package fix

If n is a type-level name for a finite set, then a value of type n cardinal is a runtime integer that represents the cardinal of the set n.

In the following, the functor Gensym allows creating open-ended sets, which can grow over time. If n is such a set, then a value of type n cardinal can be thought of as the as-yet-undetermined cardinal of the set.

If n is the cardinal of the set n, then cardinal n returns the cardinal of this set, as a concrete integer.

In the following, the functor Gensym allows creating open-ended sets, which can grow over time. If n is such a set, then calling cardinal n has the side-effect of freezing this set, thereby fixing its cardinal: thereafter, calling fresh becomes forbidden, so no new elements can be added.

If n is a type-level name for a finite set, then a value i of type n index is an integer value that is guaranteed to inhabit the set n.

If n has type n cardinal, then 0 <= i < cardinal n must hold.

The main reason why elements of a finite set are called "indices" is that their main purpose is to serve as indices in fixed-size vectors. See the submodule Vector below.

A new type-level set is created by an application of the functors Const, Gensym, and Sum below. Each functor application creates a fresh type name n. More precisely, each functor application returns a module whose signature is CARDINAL: it contains both a fresh abstract type n and a value n of type n cardinal that represents the cardinal of the newly-created set.

Const(struct let cardinal = c end) creates a fresh type-level name for a set whose cardinal is c. c must be nonnegative.

The function const is a value-level analogue of the functor Const.

Empty contains a type-level name for the empty set.

Gensym() creates an open-ended type-level set, whose cardinality is not known a priori. As long as the cardinal of the set has not been observed by invoking cardinal, new elements can be added to the set by invoking fresh.

The type ('l, 'r) either represents the disjoint sum of the types 'l and 'r. It is isomorphic to the type either found in Stdlib.Either in OCaml 4.12.0.

The signature SUM extends CARDINAL with an explicit isomorphism between the set n and the disjoint sum l + r. The functions inj_l and inj_r convert an index into l or an index into r into an index into n. Conversely, the function prj converts an index into r into either an index into l or an index into r.

Sum(L)(R) creates a new type-level set, which is the disjoint sums of the sets L and R. The functor application Sum(L)(R) involves a call to cardinal L.n, thereby fixing the cardinal of the set L, if it was an open-ended set. The cardinal of the set R is not fixed: if R is an open-ended set, then the new set is open-ended as well, and it is still permitted to add new elements to R by calling R.fresh(). Fixing the cardinal of the new set fixes the cardinal of R.

The function sum is a value-level analogue of the functor Sum.

The submodule Index allows safely manipulating indices into a finite set.

A vector of type (n, a) vector is a (fixed-size) array whose indices lie in the type-level set n and whose elements have type a.

The submodule Vector allows safely manipulating indices into a vector.