Design: More expressive type quantities

[ReedOei]

Currently for type quantities, we have empty, any, one, and nonempty.

One simple extension that may be useful is to add every (which used to be in the lanugage) back. One particular use case for this is in filters, where it can be used to assert that the predicate is true for every value in the source. For example,

[ x,y,z] --[ every such that P(_) ]-> Dst

will only succeed when P(x), P(y), and P(z) are all true.

Another possible extension is to replace type quantities with a "bounds" system, so types look something like xs : (>=n, <=m) multiset nat, meaning that n <= size x <= m, where . This gives significantly more expressive power (e.g., empty becomes (>=0, <=0), nonempty becomes (>=1, <=infinity)), but it's unclear what this is actually useful for.