How to iterate or repeat untyped function n times?

Question

I'm practicing with OCaml compiler and I'm doing a small assignment where we have to implement Church numerals defined as:

zz = pair c0 c0; ss = λp. pair ( snd p) ( plus c1 (snd p)); prd = λm. fst (m ss zz );

and to calculate the ss i wanna implement plus:

plus = λm. λn. λs. λz. m s (n s z)

so my question is, how to implement funtion plus, like n times succ 0?

I've tried like plus = lambda m. lambda n. lambda s. lambda z. m s (n s z); but it is not correct in the compiler.

I've notice that I work in the OCaml compiler and write all my functions in the func.f file not in the .ml file

https://www.cis.upenn.edu/~bcpierce/tapl/ code is from there, fulluntyped folder

Answer 1

Instead of lambda as in lambda calculus, you use fun to encode Church numerals in OCaml. You define numerals as functions that takes a unary function (named s for "successor") and base value (z for "zero"). For example, three is:

# let three = fun s z -> (s (s (s z)));;
val three : ('a -> 'a) -> 'a -> 'a = <fun>

If you want to translate this representation to an OCaml integer, you define:

# let int_succ x = x + 1;;

Then you can have the OCaml integer representation of three by calling it like so:

# three int_succ 0;;
- : int = 3

It effectively calls int_succ successively on 0, on the innermost result (ie. 1), etc. until you get 3.

But you can manipulate those numbers in their Church representation as follows. For example, to compute the successor Church number of an arbitrary Churn number n:

# let succ n = fun s z -> (s (n s z));;

We have to return a Church number, the result is a function of two parameters, s and z. It also takes a single input, a church number n. The result is calling s on (n s z), namely the successor of number n. For example:

# (succ three) int_succ 0;;
- : int = 4

Likewise, we can define add:

# let add x y = (fun s z -> (x s (y s z)));;
val add : ('a -> 'b -> 'c) -> ('a -> 'd -> 'b) -> 'a -> 'd -> 'c = <fun>

Here, the function takes two numbers. The expression (y s z) represents the computation made on number y, and it is used as the base value when applying x in (x s (y s z)). If you use int_succ and 0 for s and z, you can see that (y s z) will increment from 0 as many times as encoded by y, then increment from that value as many times as encoded by x.

For example:

# let two = fun s z -> (s (s z)) ;;
val two : ('a -> 'a) -> 'a -> 'a = <fun>

Then:

# let five = add two three;;
val five : ('_weak4 -> '_weak4) -> '_weak4 -> '_weak4 = <fun>

Notice that the types are weak, you don't need to worry too much about it but that means that once you call five with a given s and z, you won't be able to reuse five with different types.

# five int_succ 0;;
- : int = 5

And now, the type is fully known:

# five;;
- : (int -> int) -> int -> int = <fun>