This implementation of implicit finite sequences is used as a building block in the definition of the type enum, which follows.

An enumeration of type 'a enum can be loosely thought of as a set of values of type 'a, equipped with a notion of size. More precisely, it is a function of a size s to a subset of inhabitants of size s, presented as a sequence.

We expose the fact that enumerations are functions, instead of making enum an abstract type, because this allows the user to make recursive definitions. It is up to the user to ensure that recursion is well-founded; as a rule of thumb, every recursive call must appear under pay. It is also up to the user to take precautions so that these functions have constant time complexity (beyond the cost of an initialization phase). This is typically achieved by using a memoizing fixed point combinator instead of an ordinary recursive definition.

empty is the empty enumeration.

zero is a synonym for empty.

The enumeration just x contains just the element x, with size zero. just x is equivalent to finite [x].

The enumeration enum x contains the elements in the sequence xs, with size zero.

The enumeration pay e contains the same elements as e, with a size that is increased by one with respect to e.

sum e1 e2 is the union of the enumerations e1 and e2. It is up to the user to ensure that the sets e1 and e2 are disjoint.

(++) is a synonym for sum.

exists xs e is the union of all enumerations of the form e x, where x is drawn from the list xs. (This is an indexed sum.) It is up to the user to ensure that the sets e1 and e2 are disjoint.

product e1 e2 is the Cartesian product of the enumerations e1 and e2.

( ** ) is a synonym for product.

balanced_product e1 e2 is a subset of the Cartesian product product e1 e2 where the sizes of the left-hand and right-hand pair components must differ by at most one.

( *-* ) is a synonym for balanced_product.

map phi e is the image of the enumeration e through the function phi. It is up to the user to ensure that phi is injective.

The enumeration finite xs contains the elements in the list xs, with size zero.

bool is equivalent to finite [false; true].

If elem is an enumeration of the type 'a, then list elem is an enumeration of the type 'a list. It is worth noting that every call to list elem produces a fresh memoizing function, so (if possible) one should avoid applying list twice to the same argument; that would be a waste of time and space.

Suppose we wish to enumerate lists of elements, where the validity of an element depends on which elements have appeared earlier in the list. For instance, we might wish to enumerate lists of instructions, where the set of permitted instructions at some point depends on the environment at this point, and each instruction produces an updated environment. If fix is a suitable fixed point combinator and if the function elem describes how elements depend on environments and how elements affect environments, then dlist fix elem is such an enumeration. Each list node is considered to have size 1. Because the function elem produces a list (as opposed to an enumeration), an element does not have a size.

The fixed point combinator fix is typically of the form curried fix, where fix is a fixed point combinator for keys of type 'env * int. Memoization takes place at keys that are pairs of an environment and a size.

The function elem receives an environment and must return a list of pairs of an element and an updated environment.

sample m e i j k is a sequence of at most m elements of every size comprised between i (included) and j (excluded) extracted out of the enumeration e, prepended in front of the existing sequence k. At every size, if there are at most m elements of this size, then all elements of this size are produced; otherwise, a random sample of m elements of this size is produced.