A library that implements dependent (heterogeneous) maps

Dmap is an OCaml library that implements dependent (heterogeneous)
immutable maps. The type of keys is indexed by the type of the
associated values, so that the maps can contain data whose types may
depend on the values of keys. It is adapted from the implementation
code for maps that is used by the OCaml standard

For instance:

module IntBool = struct
  (* The type for the keys of our maps. The index ['a] denotes the type
     of the values that will be associated to the keys. In the case of the
     [Int] constructor, the map will expect data of type [string]. In the
     case of the [Bool] constructor, the map will expect values of type [char].
  type 'a t = Int : int -> string t | Bool : bool -> char t

  (* Total order on values of type [_ t]. *)
  let compare (type a1 a2) (v1 : a1 t) (v2 : a2 t) : (a1, a2) cmp =
    match (v1, v2) with
    | Int n1, Int n2 -> if n1 = n2 then Eq else if n1 < n2 then Lt else Gt
    | Bool b1, Bool b2 ->
        if b1 = b2 then Eq else if (not b1) || b2 then Lt else Gt
    | Bool _, Int _ -> Lt
    | Int _, Bool _ -> Gt

(* We create a module of maps whose keys have type [IntBool.t] *)
module IntBoolMap = Dmap.Make(IntBool)

(* Definition of a map of type [IntBoolMap.t]. *)
let m = IntBoolMap.(empty |> add (Int 42) "hello" |> add (Bool true) 'A')

(* Some queries on the map [m] *)
let () =
  assert (IntBoolMap.find_opt (Int 42) m = Some "hello");
  assert (IntBoolMap.find_opt (Bool true) m = Some 'A');
  assert (IntBoolMap.find_opt (Bool false) m = None)

This creates a new module IntBoolMap, with a new type
IntBoolMap.t of maps from IntBool.t to string or char.
As specified by the GADT[^1] definition of IntBool.t, the values
associated to the keys of the form Int n have type string, and
the values associated to the keys of the form Bool b have type

You can install Dmap using opam by running opam install dmap,

Alternatively, you can download, build and install the development
version by running the following commands:

git clone
cd dmap
opam pin add .

[^1]: Generalized Algebraic Data Type

16 May 2022
>= "4.12"
>= "2.9"
Reverse Dependencies