(* Existential encodings using Caml's universal types. See [1] for
 * implementation details, [2] for the theory. Credits to Daniel Bunzli and
 * Jean-Christophe Filliatre.
 *
 * [1] http://sardes.inrialpes.fr/~aschmitt/cwn/2004.01.13.html
 * [2] TAPL, Chapter 24
 *)

module type POLY_TYPE = sig type 'a t end

module type EXIST_FUNCTOR =
  functor (P : POLY_TYPE) ->
    sig
      type 'a user = { f : 'b. 'b P.t -> 'a }
      type t
      val pack : 'a P.t -> t
      val use : 'a user -> t -> 'a
    end

module Make(P : POLY_TYPE) =
  struct
    type 'a user = { f : 'b. 'b P.t -> 'a }
    type t = { g : 'a. 'a user -> 'a }
    let pack impl = { g = fun user -> user.f impl }
    let use f p = p.g f
  end