existential quantifier in OCaml

exists.ml

(* an abstract signature for instantiations of the existential quantifier *)
module type EXISTS =
sig
  (* the predicate *)
  type 'a phi

  (* the existential type *)
  type t

  (* the introduction rule *)
  val pack : 'a phi -> t

  (* we use a record to wrap this polymorphic function, working
   * around a limitation of OCaml *)
  type 'b cont = { run : 'a. 'a phi -> 'b }

  (* eliminate an existential by providing a polymorphic function
   * and an existential package *)
  val spread : 'b cont -> t -> 'b
end

(* Two implementations of the existential quantifier! *)

(* POSITIVE ENCODING *)
module Exists (Phi : sig type 'a t end) : EXISTS with type 'a phi = 'a Phi.t =
struct
  type 'a phi = 'a Phi.t
  type 'b cont = { run : 'a. 'a Phi.t -> 'b}

  (* We use OCaml's new support for generalized algebraic datatypes to define an
   * inductive type whose _constructor_ quantifies over types. *)
  type t = Pack : 'a Phi.t -> t

  let pack x =
    Pack x

  let spread k (Pack x) =
    k.run x
end

(* NEGATIVE ENCODING *)
module Exists2 (Phi : sig type 'a t end) : EXISTS with type 'a phi = 'a Phi.t =
struct
  type 'a phi = 'a Phi.t
  type 'b cont = { run : 'a. 'a Phi.t -> 'b}

  (* we use the universal property to define the existential quantifier
   * impredicatively. *)
  type t = { unpack : 'y. 'y cont -> 'y }

  let pack x =
    { unpack = fun k -> k.run x }

  let spread f pkg =
    pkg.unpack f
end

(* Below follows an example, [Exists a. List(a)] *)
module L = Exists2(struct type 'a t = 'a list end)

module type EXAMPLE =
sig
  val example : L.t
  val length : L.t -> int
end

module Example : EXAMPLE =
struct
  let example =
    L.pack ["hello"; "world!"]

  let length =
    L.spread { L.run = List.length }

  let _ =
    Printf.printf
      "Length: %i"
      (length example)
end