gadt_alist.ml

module Eq = struct
  type (_,_) t = Refl : ('a,'a) t
end

module type EqAssoc = sig
  type 'a key
  type 'a value
  val equal : 'a key -> 'b key -> ('a, 'b) Eq.t option
end

module Alist (T : EqAssoc) : sig
  type t
  val nil : t
  val cons : 'a T.key -> 'a T.value -> t -> t
  val find : 'a T.key -> t -> 'a T.value option
end = struct
  type t =
    | Nil : t
    | Cons : 'a T.key * 'a T.value * t -> t
  let cast : type a b . (a, b) Eq.t -> a T.value -> b T.value = fun Eq.Refl x -> x
  let nil = Nil
  let cons k v tail = Cons (k, v, tail)
  let rec find : type a . a T.key -> t -> a T.value option =
    fun key -> function
    | Nil -> None
    | Cons (k, v, tail) ->
      match T.equal k key with
      | None -> find key tail
      | Some equality -> Some (cast equality v)
end