OCaml 的类型系统会阻止它对教会数字建模吗？

Question

作为消遣，我正在尝试解决我在大学学习的课程（与 Lambda 微积分和各种编程概念有关）中出现的各种问题。因此，我正在尝试在 OCaml 中实现教会数字和相关运算符（也作为 OCaml 中的练习）。

这是目前的代码：

let church_to_int n =
    n (fun x -> x + 1) 0;;

let succ n s z =
    s (n s z)

let zero = fun s z -> z

let int_to_church i =
    let rec compounder i cont =
        match i with
        | 0 -> cont zero
        | _ -> compounder (i - 1) (fun res -> cont (succ res))
    in
    compounder i (fun x -> x)

let add a b = (b succ) a

let mul a b = (b (add a)) zero

所以，它似乎可以工作，但后来就崩溃了。让我们考虑这些定义：

let three = int_to_church 3
let four = int_to_church 4
church_to_int (add three four) // evaluates to 7
church_to_int (add four three) // throws type error - see later

我知道抛出的错误与定义 Church 数字时的类型多态性有关（请参阅 SO question），然后在调用一次闭包后解决。但是，我似乎不明白为什么在这种情况下会抛出类型不一致错误：

let three = int_to_church 3
let four = int_to_church 4
church_to_int (mul three four) // throws type error - see later

有什么想法吗？

具体错误：

1.

Error: This expression has type (int -> int) -> int -> int                                                 but an expression was expected of type                                                                ((('a -> 'b) -> 'c -> 'a) -> ('a -> 'b) -> 'c -> 'b) ->                                    
         ((((int -> int) -> int -> int) -> (int -> int) -> int -> int) ->
          ((int -> int) -> int -> int) -> (int -> int) -> int -> int) ->
         'd
       Type int is not compatible with type ('a -> 'b) -> 'c -> 'a

2.

Error: This expression has type                                                                              ((((('a -> 'b) -> 'c -> 'a) -> ('a -> 'b) -> 'c -> 'b) ->                                             (('d -> 'd) -> 'd -> 'd) -> 'e) ->                                                       
          ((('a -> 'b) -> 'c -> 'a) -> ('a -> 'b) -> 'c -> 'b) ->
          (('d -> 'd) -> 'd -> 'd) -> 'e) ->
         (((('a -> 'b) -> 'c -> 'a) -> ('a -> 'b) -> 'c -> 'b) ->
          (('d -> 'd) -> 'd -> 'd) -> 'e) ->
         ((('a -> 'b) -> 'c -> 'a) -> ('a -> 'b) -> 'c -> 'b) ->
         (('d -> 'd) -> 'd -> 'd) -> 'e
       but an expression was expected of type
         ((((('a -> 'b) -> 'c -> 'a) -> ('a -> 'b) -> 'c -> 'b) ->
           (('d -> 'd) -> 'd -> 'd) -> 'e) ->
          'e) ->
         ('f -> 'g -> 'g) -> 'h
       The type variable 'e occurs inside
       ((('a -> 'b) -> 'c -> 'a) -> ('a -> 'b) -> 'c -> 'b) ->
       (('d -> 'd) -> 'd -> 'd) -> 'e

Answer 1

如果你看一下三的类型，你会得到：

val three : ('_a -> '_a) -> '_a -> '_a = <fun>

这简直就是价值限制在起作用。这里很好地解释了值限制：https://realworldocaml.org/v1/en/html/imperative-programming-1.html#side-effects-and-weak-polymorphism

为了解决这个问题，在这种情况下你可以简单地eta-expand函数：

let three x = int_to_church 3 x ;;
val three : ('a -> 'a) -> 'a -> 'a = <fun>

Answer 2

好吧，我对 lambda 演算有点生疏，但在与一些聪明的老人讨论了几次之后，我得出了这个答案：是的，那样写，OCaml 的类型系统不允许写教会数字。

真正的问题在于你的加法项：

let add a b = b succ a

具有以下类型

(((('a -> 'b) -> 'c -> 'a) -> ('a -> 'b) -> 'c -> 'b) -> 'd -> 'e) -> 'd -> 'e

add 的参数类型不同。这有点可悲，因为我们天真地期望加法是可交换的。您可以在编写时轻松验证这一点：

let double a = add a a //produces type error - the type variable occurs ...

此错误意味着您正在尝试将一种类型与“更大”的类型统一，即包含它（例如：将 'a 与 'a -> 'a 统一). OCaml 不允许这样做（除非您设置了允许循环类型的 -rectypes 选项）。为了更好地理解发生了什么，让我们添加类型注释来帮助打字者（为了清楚起见，我将稍微更改一下您的符号）：

type 'a church = ('a -> 'a) -> 'a -> 'a
let zero : 'a church = fun f x -> x
let succ n : 'a church = fun f x -> f (n f x)

现在让我们回到 add 术语并稍微注释一下，看看打字员要说什么：

let add (a:'a church) b = a succ b // we only annotate "a" to let the typer infer the rest

这会产生一个非常奇怪的类型：

'a church church -> 'a church -> 'a church

这变得有趣了：为什么第一个参数输入为 'a church church？

答案如下：在这里，教堂整数是一个采用 moving 函数的值（'a -> 'a)可以浏览一个space，以及一个属于那个space的起点('a)。

这里，如果我们指定参数a的类型是'a church，那么'a 代表我们可以移动的 space。由于 succ，a 的 moving 功能在教堂上运行，比 'a 这里本身就是一个'a church，因此参数a an 'a church教堂.

这根本不是我们一开始想要的类型...但这证明了为什么类型系统不允许您的值 three 和 four 作为 add.

的第一个和第二个参数

一个解决方案是用不同的方式编写 add ：

let add a b f x = a f (b f x)

这里，a和b都具有相同的移动功能，因此是同一个类型，但是你不再欣赏偏应用的漂亮文字了...

另一种让您保持这种优美写作的解决方案是使用通用类型，它允许更大种类的多态性：

type nat = {f:'a.('a -> 'a) -> 'a -> 'a}
// this means “for all types ‘a”

let zero : nat = {
  f=fun f x -> x
}

let succ n : nat = {
  f= fun f x -> f (n.f f x)
}

let add (a:nat) (b:nat) = a.f succ b

let double a = add a a //types well

let nat_to_int n =
  n.f (fun x -> x + 1) 0;;

let nat_four = succ (succ (succ (succ zero)))

let eight_i = double nat_four |> nat_to_int //returns 8

但是这个解决方案比你最初的解决方案有点冗长。

希望清楚。

OCaml 的类型系统会阻止它对教会数字建模吗？

Does OCaml's type system prevent it from modeling Church numerals?

ocaml

lambda-calculus

church-encoding