It is my pleasure to announce the release of 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 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
thanks for your release announcement. Did you look into other similar libraries, and have a perspective how they are different from dmap? What comes to my mind are hmap and gmap. Are there other design goals, or different performance tradeoffs/guarantees?
thanks for asking. Here are the differences with hmap and gmap, as far as I understand. Please correct me if I misunderstood some parts.
hmap only supports keys with no contents. In particular, no total ordering of keys is required. Instead, you can dynamically create new keys, with the type index that you want. It is fully type-safe (no assert false, no Obj.magic, etc). It does not support (but maybe it could) a polymorphic map function (this requires second-order polymorphism). It reuses the standard library’s Map implementation by calling Map.Make.
gmap supports keys with contents, and expects a total ordering function that returns a GADT to witness type equality, exactly as I did in dmap. It supports a polymorphic map function (using second-order polymorphism). It reuses the standard library’s Map implementation by calling Map.Make. The implementation records the keys twice: as keys, and as part of the associated data, so that type equality witnesses can be exploited. This results in extra calls to the comparison functions on keys (see the code of get for an example). The extra calls and the double recording of keys might have an impact in terms of cost, that I cannot quantify. I should be measured. The code is almost type-safe: it relies on the invariant the key is the same as the key part that is recorded as data for that that binding. The impossible cases returned by the comparison function are given the assert false behavior.
dmap also supports a polymorphic map function. It does not store keys twice: as in the standard library’s implementation, the keys are stored only once. In comparison to gmap, the comparisons on keys are not done twice. The code is completely type-safe: no assert false is introduced to handle the impossible cases of key comparison. The implementation duplicates the one of the standard library, rather than calling Map.Make. The exported functions and their names are on par with the standard library’s Map.