package dmap

Dependent (or heterogeneous) association tables over ordered types.

This module implements applicative association tables, also known as finite maps or dictionaries, given a total ordering function over the keys. The particularity is that the types of the values recorded in the tables may vary, depending on the keys, hence the name heterogeneous (or dependent) maps.

All operations over maps are purely applicative (no side-effects). The implementation uses balanced binary trees, and therefore searching and insertion take time logarithmic in the size of the map.

For instance:

module IntBool = struct
  type 'a t = Int : int -> string t | Bool : bool -> char 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

module IntBoolMap = Dmap.Make(IntBool)

let m = IntBoolMap.(empty |> add (Int 42) "hello" |> add (Bool true) 'A')

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.