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

type 'n cardinal

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.

type (_, _) eq =
  1. | Refl : ('a, 'a) eq

The equality type.

val equal : 'n cardinal -> 'm cardinal -> ('n, 'm) eq option

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.

val assert_equal : 'n cardinal -> 'm cardinal -> ('n, 'm) eq

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.

  • raises Invalid_argument

    if the cardinals are not equal.

type 'n index = private int

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.

module Const (X : sig ... end) : CARDINAL

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)

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

module Empty : CARDINAL

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

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.

type ('l, 'r) either =
  1. | L of 'l
  2. | R of 'r

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.

module Sum (L : CARDINAL) (R : CARDINAL) : SUM with type l := L.n and type r := R.n

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.

val sum : 'l cardinal -> 'r cardinal -> (module SUM with type l = 'l and type r = 'r)

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

module Index : sig ... end

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

type ('n, 'a) vector

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.

module Vector : sig ... end

The submodule Vector allows safely manipulating indices into a vector.