Module GmapSource

Heterogenous maps over a GADT.

The motivation for this library originated in the area of parsing binary network protocols, which often contain options and extensions in the form of tag, length, value encodings: the set of tags and corresponding values is specified in some Internet standard, and later extended by using a global registry. Examples are IP options, TCP options, DNS resource records, TLS hello extensions, X.509v3 extensions, ... These extension mechanisms usually include the invariant that each tag may only be present once.

A more naive approach is to use a variant type of all known tag-value combinations and storing these in an association list while parsing, but verifying the uniqueness invariant takes quadratic (O(n^2)) time, and retrieving a specific option is only doable in linear O(n) time. Additionally, packing and unpacking is required with the variant type solution.

In gmap, GADTs are used to provide key-dependent value types: each GADT constructor carries their value type. The underlying storage mechanism uses OCaml's stdlib Map type: Lookup takes O(log n) time. The above mentioned uniqueness invariant can be preserved while constructing the gmap if for insertion into the map only S.update and S.add_unless_bound are used (S.add replaces the existing binding if present).

A small example:

type _ key =
  | I : int key
  | S : string key

module K = struct
  type 'a t = 'a key

  let compare : type a b. a t -> b t -> (a, b) Gmap.Order.t = fun t t' ->
    let open Gmap.Order in
    match t, t' with
    | I, I -> Eq | I, _ -> Lt | _, I -> Gt
    | S, S -> Eq
end

module GM = Gmap.Make(K)

Using GM is done as follows:

match GM.find I (GM.singleton I 10) with
| Some x -> x * x
| None -> 0

0.3.0 - homepage