Skip to content

Instantly share code, notes, and snippets.

@debasishg
Forked from jonsterling/exists.ml
Created October 12, 2023 16:47
Show Gist options
  • Save debasishg/cabf63e1515ba091350dd0a458c2b425 to your computer and use it in GitHub Desktop.
Save debasishg/cabf63e1515ba091350dd0a458c2b425 to your computer and use it in GitHub Desktop.
existential quantifier in OCaml
(* 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment