Skip to content

Instantly share code, notes, and snippets.

@garrigue
Created June 18, 2015 04:49
Show Gist options
  • Save garrigue/b4728f8f279d31c489a1 to your computer and use it in GitHub Desktop.
Save garrigue/b4728f8f279d31c489a1 to your computer and use it in GitHub Desktop.
Logic using GADTs in OCaml
(* Logic using GADTs *)
exception Axiom
type falso
type ex_falso = {ex_falso: 'p. falso -> 'p}
let ex_falso = {ex_falso = fun _ -> raise Axiom}
type 'p not = 'p -> falso
type ('a,'b) ior = Inl of 'a | Inr of 'b
(* NB: the unit -> below is essential for soundness *)
type classic = {classic: 'p. unit -> ('p, 'p not) ior}
type (_,_) eq = Refl : ('x,'x) eq
(* forall x, exists y, x = y *)
type 'a exeq = Exeq : ('x,'y) eq -> 'x exeq
type for_all_x_exists_y_eq_x_y = {faxy: 'x. 'x exeq}
let proof = {faxy = Exeq Refl}
(* Drinkers paradox: exists x, x drinks -> forall y, y drinks *)
type _ drinks
type all_drink = {all: 'y. unit -> 'y drinks}
type non_drinker = Nd : 'x drinks not -> non_drinker
type drinkers_paradox = Drinker : ('x drinks -> all_drink) -> drinkers_paradox
let proof {classic=c} =
let ef = ex_falso.ex_falso in
match c () with
| Inl (Nd nd) -> Drinker (fun d -> ef (nd d))
| Inr nnd -> Drinker (fun d ->
{all = fun () -> match c() with
| Inr nd -> ef (nnd (Nd nd))
| Inl d -> d})
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment