(* Scott numerals in OCaml: second attempt. *)

(* This encodes Scott naturals in OCaml using records, in what I think
   is essentially an isorecursive formulation. *)

type nat = {f: 'r.(nat -> 'r) -> 'r -> 'r}

let zero = {f = fun s z -> z}
let succ n = {f = fun s z -> s n}
let rec prec n = n.f (fun p -> p) zero 

let rec to_int: nat -> int =  fun k -> k.f (fun i -> (to_int i)+1) 0 

let rec from_int: int -> nat = fun k -> if k=0 then zero else succ (from_int (k-1))

let one = succ zero

let two = succ one

let five = succ(succ(succ(succ(succ zero))))
 
let six = succ five

let rec add k l = k.f (fun p -> succ(add p l)) l 

let rec mul k l = k.f (fun p -> add (mul p l) l) zero

let _ =  add five (mul six (succ six))


(* This is much better than the first attempt.  We get

  type nat = { f : 'r. (nat -> 'r) -> 'r -> 'r; }
  val zero : nat = {f = <fun>}
  val succ : nat -> nat = <fun>
  val prec : nat -> nat = <fun>
  val to_int : nat -> int = <fun>
  val from_int : int -> nat = <fun>
  val one : nat = {f = <fun>}
  val two : nat = {f = <fun>}
  val five : nat = {f = <fun>}
  val six : nat = {f = <fun>}
  val add : nat -> nat -> nat = <fun>
  val mul : nat -> nat -> nat = <fun>
  - : nat = {f = <fun>}
  
Everything has a sensible type, with no polymorphic
values in sight.  We can do sensible calculations with
no typing problems.  Unfortunately RAML doesn't support
records, so it can't handle this.

*)