Task

In the Church encoding of natural numbers, the number N is encoded by a function that applies its first argument N times to its second argument.

 Church zero always returns the identity function, regardless of its first argument. In other words, the first argument is not applied to the second argument at all.
 Church one applies its first argument f just once to its second argument x, yielding f(x)
 Church two applies its first argument f twice to its second argument x, yielding f(f(x))
 and each successive Church numeral applies its first argument one additional time to its second argument, f(f(f(x))), f(f(f(f(x)))) ... The Church numeral 4, for example, returns a quadruple composition of the function supplied as its first argument.


Arithmetic operations on natural numbers can be similarly represented as functions on Church numerals.

In your language define:

 Church Zero,
 a Church successor function (a function on a Church numeral which returns the next Church numeral in the series),
 functions for Addition, Multiplication and Exponentiation over Church numerals,
 a function to convert integers to corresponding Church numerals,
 and a function to convert Church numerals to corresponding integers.


You should:

 Derive Church numerals three and four in terms of Church zero and a Church successor function.
 use Church numeral arithmetic to obtain the the sum and the product of Church 3 and Church 4,
 similarly obtain 4^3 and 3^4 in terms of Church numerals, using a Church numeral exponentiation function,
 convert each result back to an integer, and return it or print it to the console.


(*  Using type as suggested in https://stackoverflow.com/questions/43426709/does-ocamls-type-system-prevent-it-from-modeling-church-numerals 
    This is an explicitly polymorphic type : it says that f must be of type ('a -> 'a) -> 'a -> 'a for any possible a "at same time".
*)
type church_num = { f : 'a. ('a -> 'a) -> 'a -> 'a }
 
(* Zero means apply f 0 times to x, aka return x *)
let ch_zero : church_num = { f = fun _ -> fun x -> x }
 
(* One simplifies to just returning the function *)
let ch_one : church_num = { f = fun fn -> fn }
 
(* The next numeral of a church numeral would apply f one more time *)
let ch_succ (c : church_num) : church_num = { f = fun fn x -> fn (c.f fn x) }
 
(* Adding m and n is applying f m times and then also n times *)
let ch_add  (m : church_num) (n : church_num) : church_num =
    { f = fun fn x -> n.f fn (m.f fn x) }
 
(* Multiplying is repeated addition : add n, m times *)
let ch_mul  (m : church_num) (n : church_num) : church_num =
    { f = fun fn x -> m.f (n.f fn) x }
 
(*  Exp is repeated multiplication : multiply by base, exp times.
    However, Church numeral n is in some sense the n'th power of a function f applied to x
    So exp base = apply function base to the exp'th power = base^exp.
*)
let ch_exp (base : church_num) (exp : church_num) : church_num =
    { f = fun fn x -> (exp.f base.f) fn x }
 
(* extended Church functions: *)
 
(* test function for church zero *)
let ch_is_zero (c : church_num) : church_num =
    { f = fun fn x -> c.f (fun _ -> fun _ -> fun xi -> xi) (* when argument is not ch_zero *)
                          (fun fi -> fi) (* when argument is ch_zero *) fn x }
 
(* church predecessor function; reduces function calls by one unless already church zero *)
let ch_pred (c : church_num) : church_num =
    { f = fun fn x -> c.f (fun g h -> h (g fn)) (fun _ -> x) (fun xi -> xi) }
 
(* church subtraction function; calls predecessor function second argument times on first *)
let ch_sub (m : church_num) (n : church_num) : church_num = n.f ch_pred m
 
(* church division function; counts number of times divisor can be recursively
   subtracted from dividend *)
let ch_div (dvdnd : church_num) (dvsr : church_num) : church_num =
  let rec divr n = (fun v -> v.f (fun _ -> (ch_succ (divr v)))
                                  ch_zero) (ch_sub n dvsr)
  in divr (ch_succ dvdnd)
 
(* conversion functions: *)
 
(* Convert a number to a church_num via recursion *)
let church_of_int (n : int) : church_num = 
    if n < 0 
    then raise (Invalid_argument (string_of_int n ^ " is not a natural number"))
    else 
    (* Tail-recursed helper *)
    let rec helper n acc = 
        if n = 0 
        then acc
        else helper (n-1) (ch_succ acc)
    in helper n ch_zero
 
(*  Convert a church_num to an int is rather easy! Just +1 n times. *)
let int_of_church (n : church_num) : int = n.f succ 0
 
(* Now the tasks at hand: *)
 
(* Derive Church numerals three, four, eleven, and twelve,
   in terms of Church zero and a Church successor function *)
 
let ch_three = church_of_int 3
let ch_four = ch_three |> ch_succ
let ch_eleven = church_of_int 11
let ch_twelve = ch_eleven |> ch_succ
 
(* Use Church numeral arithmetic to obtain the the sum and the product of Church 3 and Church 4 *)
let ch_7 = ch_add ch_three ch_four
let ch_12 = ch_mul ch_three ch_four
 
(* Similarly obtain 4^3 and 3^4 in terms of Church numerals, using a Church numeral exponentiation function *)
let ch_64 = ch_exp ch_four ch_three
let ch_81 = ch_exp ch_three ch_four
 
(* check that ch_is_zero works *)
let ch_1 = ch_is_zero ch_zero
let ch_0 = ch_is_zero ch_three
 
(* check church predecessor, subtraction, and division, functions work *)
let ch_2 = ch_pred ch_three
let ch_8 = ch_sub ch_eleven ch_three
let ch_3 = ch_div ch_eleven ch_three
let ch_4 = ch_div ch_twelve ch_three
 
(* Convert each result back to an integer, and return it as a string *)
let result = List.map (fun c -> string_of_int(int_of_church c)) 
                      [ ch_three; ch_four; ch_7; ch_12; ch_64; ch_81;
                        ch_eleven; ch_twelve; ch_1; ch_0; ch_2; ch_8; ch_3; ch_4 ]
             |> String.concat "; " |> Printf.sprintf "[ %s ]"
 
;;
 
print_endline result