Module Pickles_types.Hlist

Basic primitives for inductive rules. In particular, heterogeneous lists (H1, H2, ...) whose length and element types are known at compile-time.

To get started, read some basic usage examples in Hlist0.H1, H1 and H1.Map.

Implementation principle

In a normal value-level computation analogy:

In the rest of this documentation, we will use the terms "type values", "type functions" and "higher-order type functions" w.r.t this analogy. Where possible, we will give for each symbol its equivalent translation at the value-level.

The basic concept of this implementation of heterogeneous lists is inspired from Haskell's Hlist library: https://okmij.org/ftp/Haskell/HList-ext.pdf

Supporting transformers

The following modules and functors are support tools used to manipulate types that are then fed to the heterogeneous lists defined below (see Heterogeneous lists).

Arity transformers

The following higher-order functions artificially increase the number of arguments of a function (or value), by creating a function that ignores extra parameters.

module E01 (T : Poly_types.T0) : sig ... end

Map arity 0 to 1: let e01 t = fun _ -> t

module E02 (T : Poly_types.T0) : sig ... end

Map arity 0 to 2: let e02 t = fun _ _ -> t

module E03 (T : Poly_types.T0) : sig ... end

Map arity 0 to 3: let e02 t = fun _ _ _ -> t

module E04 (T : Poly_types.T0) : sig ... end

Map arity 0 to 4: let e02 t = fun _ _ _ _ -> t

module E06 (T : Poly_types.T0) : sig ... end

Map arity 0 to 6: let e06 t = fun _ _ _ _ _ _ -> t

module E13 (T : Poly_types.T1) : sig ... end

Map arity 1 to 3: let e13 t = fun a _ _ -> t a

module E23 (T : Poly_types.T2) : sig ... end

Map arity 2 to 3: let e23 t = fun a b _ -> t a b

Tuple transformers

The following higher-order functions take multiple functions F, G, ... and return a function which applies all of its arguments to F, G, ... and packs the result in a tuple.

module Tuple2 (F : Poly_types.T3) (G : Poly_types.T3) : sig ... end

Tuple of 2 function applications: let tuple2 f g = fun a b c -> (f a b c, g a b c)

module Tuple3 (F : Poly_types.T3) (G : Poly_types.T3) (H : Poly_types.T3) : sig ... end

Tuple of 3 function applications: let tuple3 f g h = fun a b c -> (f a b c, g a b c, h a b c)

module Tuple4 (F : Poly_types.T3) (G : Poly_types.T3) (H : Poly_types.T3) (I : Poly_types.T3) : sig ... end

Tuple of 4 function applications: let tuple4 f g h i = fun a b c -> (f a b c, g a b c, ..., i a b c)

module Tuple5 (F : Poly_types.T3) (G : Poly_types.T3) (H : Poly_types.T3) (I : Poly_types.T3) (J : Poly_types.T3) : sig ... end

Tuple of 5 function applications: let tuple4 f g h i = fun a b c -> (f a b c, g a b c, ..., j a b c)

Argument selectors

The following Functions just return one of their arguments.

module Arg1 : sig ... end

Always return first argument: let fst a _ = a

module Arg2 : sig ... end

Always return second argument: let snd _ b = b

Application transformers

The following higher-order functions composes function applications in specific ways.

module Apply2 (F : Poly_types.T2) (X : Poly_types.T1) (Y : Poly_types.T1) : sig ... end

Compose one binary function F and two unary functions X and Y into a binary function that applies X (resp. Y) to its first (resp. second) argument before passing both to F: let apply2 f x y = fun a b -> f (x a) (y b)

module Dup (F : Poly_types.T2) : sig ... end

Transforms a binary function into an unary one by duplicating its argument. let dup f = fun x -> f x x

module Length = Hlist0.Length

Reification of list length with Peano integers, see Hlist0.Length.

Heterogeneous lists

Over one type parameter

The following modules are named as with the following scheme:

module H1 : sig ... end

Operations on heterogeneous lists whose content type varies over a single type parameter. Read Hlist0.H1 first.

module Id = Hlist0.Id

Identity type function, see Hlist0.Id.

module HlistId = Hlist0.HlistId

Simplest heterogeneous list, see Hlist0.HlistId.

Over two type parameters

module H2 : sig ... end

Operations on heterogeneous lists whose content type varies over a two type parameters.

module H2_1 : sig ... end

Data type of heterogeneous lists whose content type varies over two type parameters, but also varies homogeneously over one other type parameter. It supports operations similar to H1. See also Hlist0.H1_1.

Over three type parameters

module H3 : sig ... end

Operations on heterogeneous lists whose content type varies over a tree type parameters.

module H3_1 (A : sig ... end) : sig ... end

Data type of heterogeneous lists whose content type varies over three type parameters, but also varies homogeneously over one other type parameters. It supports no operations. See Hlist0.H1_1.

module H3_2 : sig ... end

Data type of heterogeneous lists whose content type varies over three type parameters, but also varies homogeneously over two other type parameters. It supports no operations. See Hlist0.H1_1.

module H3_3 : sig ... end

Data type of heterogeneous lists whose content type varies over three type parameters, but also varies homogeneously over three other type parameters. It supports no operations. See Hlist0.H1_1.

module H3_4 : sig ... end

Data type of heterogeneous lists whose content type varies over three type parameters, but also varies homogeneously over four other type parameters. It supports no operations. See Hlist0.H1_1.

Over four type parameters

module H4 : sig ... end

Operations on heterogeneous lists whose content type varies over a four type parameters.

module H6 : sig ... end

Operations on heterogeneous lists whose content type varies over a four type parameters.

module H4_2 : sig ... end

Data type of heterogeneous lists whose content type varies over four type parameters, but also varies homogeneously over two other type parameters. It supports no operations. See Hlist0.H1_1.

module H4_4 : sig ... end

Data type of heterogeneous lists whose content type varies over four type parameters, but also varies homogeneously over four other type parameters. It supports no operations. See Hlist0.H1_1.

module H4_6 : sig ... end

Data type of heterogeneous lists whose content type varies over four type parameters, but also varies homogeneously over six other type parameters. It supports no operations. See Hlist0.H1_1.

module H6_2 : sig ... end

Data type of heterogeneous lists whose content type varies over six type parameters, but also varies homogeneously over two other type parameters. It supports no operations. See Hlist0.H1_1.

module H6_4 : sig ... end

Data type of heterogeneous lists whose content type varies over six type parameters, but also varies homogeneously over four other type parameters. It supports no operations. See Hlist0.H1_1.

Maximum functions for natural integer lists

Utilities to compute the maximum of heterogeneous lists containing natural integers whose type represent their value (hence the need for heterogeneous lists).

module type Max_s = sig ... end

Type of modules returned by max and max_exn. Contains the maximum value n and the list of its predecessors p.

type 'ns max = (module Max_s with type ns = 'ns)

Type of the maximum for heterogeneous lists containing types 'ns.

val max : ('n * 'ns) H1.T(Nat).t -> ('n * 'ns) max

Find the maximum of a non-empty (ensured by the type system) list of naturals.

val max_exn : 'ns H1.T(Nat).t -> 'ns max

Find the maximum of a list of naturals, raising an exception if it is empty.

module Maxes : sig ... end

Build the (heterogeneous) list of maximums from a vector of vectors of integers. See Vector.

Misc. operations

module Map_1_specific (A : Poly_types.T2) (B : Poly_types.T2) (C : sig ... end) : sig ... end

Build a function which transforms a Hlist0.H1_1 list into another Hlist0.H1_1 which has the same varying type parameter but a different homogeneous type parameter.

module Lengths : sig ... end

Handles the conversion from a list of Length to its equivalent list of natural integers.