package dmap

Dmap

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

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
end

(* 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 char.

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 https://gitlab.inria.fr/bmontagu/dmap.git
cd dmap
opam pin add .

[^1]: Generalized Algebraic Data Type