(* run `ocamlc -i code.ml` to see the types *) (* modus ponens *) let apply f x = f x (* axiomatization of -> *) let const x = fun _ -> x let subst x y z = x z (y z) (* implements something like (x y){z} = x{z} y{z} where z is a substitution *) (* axiomatization of AND *) let fst (a,b) = a let snd (a,b) = b let pair a b = (a,b) (* axiomatization of true *) let tt = () (* axiomatization of false *) type void = {nope:'a .'a} let ff1 = {nope = let rec f x = f x in f ()} let ff2 = {nope = failwith ""} let explode (f:void) : 'b = f.nope (* axiomatization of OR *) type ('a,'b) or' = Left of 'a | Right of 'b let left (x:'a) = Left x let right (y:'b) = Right y let match' (f1:'a -> 'c) (f2:'b -> 'c) = function | Left v1 -> f1 v1 | Right v2 -> f2 v2 (* SKI combinators *) let s x y z = x z (y z) let k x y = x let i x = x (* A few theorems about -> and AND *) let swap (a,b) = (b,a) let curry f x y = f (x,y) let uncurry f (x,y) = f x y (* Several proofs of a theorem *) let pair1 x y = (fun z -> (snd z, fst z)) (y,x) let pair2 x y = (snd (y,x), fst (y,x)) let pair3 x y = (x,y)