package gmap

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, variant packing/unpacking is required.

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 verified by only using S.update or S.add_unless_bound (respectively S.addb_unless_bound for insertion).

A simple example:

type _ k =
  | A : int k
  | B : string k

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

  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
    | A, A -> Eq | A, _ -> Lt | _, A -> Gt
    | B, B -> Eq

  let pp : type a. Format.formatter -> a t -> a -> unit = fun ppf t v ->
    match t, v with
    | A, x -> Fmt.pf ppf "A %d" x
    | B, s -> Fmt.pf ppf "B %s" s
end

module GM = Gmap.Make(K)

Using GM is done as follows:

match GM.find A m with
| Some x -> x * x
| None -> 0

0.2.0 - homepage