`Fix.Indexing`

This module offers **a safe API for manipulating indices into fixed-size arrays**.

It provides support for constructing finite sets at the type level and for encoding the inhabitants of these sets as runtime integers. These runtime integers are statically branded with the name of the set that they inhabit, so two inhabitants of two distinct sets cannot be inadvertently confused.

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.

`val cardinal : 'n cardinal -> int`

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.

`val is_fixed : 'n cardinal -> bool`

`is_fixed n`

determines whether the cardinal `n`

is (or has been) fixed.

The equality type.

`equal n m`

tests whether the cardinals `n`

and `m`

are equal, and if so, produces a type-level equality between the types `'n`

and `'m`

. If the cardinals `n`

or `m`

are not yet fixed, then, as a side effect of this call, they become fixed.

`assert_equal n m`

checks that the cardinals `n`

and `m`

are equal, and produces a type-level equality between the types `'n`

and `'m`

. If the cardinals `n`

or `m`

are not yet fixed, then, as a side effect of this call, they become fixed.

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.

`module type CARDINAL = sig ... end`

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.

`val const : int -> (module CARDINAL)`

`module Gensym () : sig ... end`

`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.

`module type SUM = sig ... end`

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`

.

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`

.