package gmap
Library
Module
Module type
Parameter
Class
Class type
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
module Order : sig ... end
Ordering.
module type KEY = sig ... end
Key.