我正在使用 OCaml 编译器进行练习，我正在做一个小任务，我们必须实现教堂数字，定义为：
zz = pair c0 c0; ss = λp. pair ( snd p) ( plus c1 (snd p)); prd = λm. fst (m ss zz );
并计算我想要实施的 ss 加：
plus = λm. λn. λs. λz. m s (n s z)
所以我的问题是，如何实现函数加，比如 n 次 succ 0？
我试过
了，plus = lambda m. lambda n. lambda s. lambda z. m s (n s z);
但在编译器中不正确。
我注意到我在 OCaml 编译器中工作，并将我的所有函数都写在 func.f 文件中而不是 .ml 文件中
https://www.cis.upenn.edu/~bcpierce/tapl/代码来自那里，fulluntyped 文件夹
与lambda在 lambda 演算中不同，您可以使用funOCaml 对 Church 数字进行编码。您将数字定义为接受一元函数（以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;;
然后你可以three通过像这样调用它来获得 OCaml 整数表示：
# three int_succ 0;;
- : int = 3
它有效地依次调用int_succ0、最里面的结果（即 1）等，直到你得到 3。
但是你可以在他们的教会代表中操纵这些数字，如下所示。例如，要计算任意流失数 n 的后继 Church 数：
# let succ n = fun s z -> (s (n s z));;
我们必须返回一个 Church 编号，结果是两个参数的函数，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)表示对 number 进行的计算，在应用iny时用作基值。如果将and 0 用于and ，您可以看到它将从 0 增加 编码 的次数，然后从该值增加 编码 的次数。x(x s (y s z))int_succsz(y s z)yx
例如：
# 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>
注意类型是弱的，你不需要太担心，但这意味着一旦你用给定的sand调用了 5 z，你将不能重用five不同的类型。
# five int_succ 0;;
- : int = 5
现在，该类型已完全为人所知：
# five;;
- : (int -> int) -> int -> int = <fun>