Как итерировать или повторять нетипизированную функцию n раз?

Вместо lambda, как в лямбда-исчислении, вы используете fun для кодирования чисел Черча в OCaml. Вы определяете числа как функции, которые принимают унарную функцию (с именем s для преемника) и базовое значение (z для нуля). Например, три это:

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

Если вы хотите преобразовать это представление в целое число OCaml, вы определяете:

# let int_succ x = x + 1;;

Затем вы можете получить целочисленное представление OCaml three, вызвав его следующим образом:

# three int_succ 0;;
- : int = 3

Он эффективно вызывает int_succ последовательно для 0, самого внутреннего результата (т.е. 1) и т. д., пока вы не получите 3.

Но вы можете манипулировать этими числами в их церковном представлении следующим образом. Например, чтобы вычислить номер Черча-преемника произвольного номера оттока n:

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

Мы должны вернуть число Черча, результат является функцией двух параметров, s и z. Он также принимает один вход, номер церкви n. В результате звонит s (n s z), а именно наследнику номера n. Например:

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

Точно так же мы можем определить 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>

Здесь функция принимает два числа. Выражение (y s z) представляет собой вычисление, выполненное для числа y, и используется в качестве базового значения при применении x к (x s (y s z)). Если вы используете int_succ и 0 для s и z, вы можете видеть, что (y s z) будет увеличиваться от 0 столько раз, сколько раз закодировано y, а затем увеличиваться от этого значения столько раз, сколько раз закодировано x.

Например:

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

Потом:

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

Обратите внимание, что типы слабы, вам не нужно слишком беспокоиться об этом, но это означает, что как только вы вызовете Five с заданными s и z, вы не сможете повторно использовать five с различные виды.

# five int_succ 0;;
- : int = 5

И вот, тип полностью известен:

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