(********************** ml source ***********************)

(* Church Numerals *)

val zero = fn f => fn x => x;
val next = fn n => fn f => fn x => (f ((n f) x));
val add = fn m => fn n => fn f => fn x => ((((m next) n) f) x);
val mult = fn f => fn g => fn x => (f (g x));
val power = fn f => fn g => (f g);

(* Church Numerals *)
val one = (next zero);
val two = (next one);

val inc = fn n => n+1;
val sq = fn n:int => n*n ;

(* More Church Numerals *)
val four = (add one (add one (add one (add one zero))));
val three = ((add one) two);
val five = ((add three) two);
val six = ((mult three) two);
val nine = ((power two) three);
val ten = ((mult two) five);

(* A test to show what a Church Numeral does *)

((zero inc) 0);
((five inc) 0);
((ten inc) 0);

val first = fn x => fn y => x;
val second = fn x => fn y => y;
val third = fn x => fn y => fn z => z;

val iszero = fn n => ((n third) first);
(* Predicate, is a Church Numeral zero? *)

val T = fn x => fn y => x ;
val F = fn x => fn y => y ;
val af = fn x => F;
val zp = fn n => ((n af) T);  (* zp is a zero predicate *)
(* note that while zp is a nice zero test in Lambda-calc,
   which is untyped... when we simulate it is ML (which is typed)
   we get some restrictions... namely, that when we want to
   zero test any number greater than one, we get back a form
   of the FALSE function that requires both arguments to be
   of the same type...

   i.e. (zp two) will have type signature 'a -> 'a -> 'a
        where as F has signature 'a -> 'b -> 'b

   (zp two) still takes two arguments and returns the second,
   as does F, but (zp two) forces a restriction on what arguments
   it is willing to work on
*)

val pair = fn x => fn y => fn f => ((f x) y);

val prefn = fn f => fn p => ((pair (f (p first))) (p first));
val pred = fn n => fn f => fn x => (((n (prefn f))(pair x x)) second);
(* predecessor function *)

val eight = (pred nine);