Module DmapSource

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