Skip to content

Instantly share code, notes, and snippets.

(* Encoding termination of a Turing machine into a GADT *)
type s0 and s1 and s2 and s3 and s4 and fin
type c0 and c1 and c2 and c3 and blank
type left and right
type endt
type ('st_in, 'head_in, 'st_out, 'head_out, 'lr) transition =
| Tr1 : (s0, 'a, s1, 'a, left) transition
@garrigue
garrigue / logic.ml
Created June 18, 2015 04:49
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