ocaml - OCaml 的类型系统是否会阻止它对 Church 数字进行建模？

Question

作为打发时间，我正在尝试解决我在大学上的一门类(class)(关于 Lambda 微积分和各种编程概念)中提出的各种问题。因此，我正在尝试在 OCaml 中实现 Church 数字和相关运算符(也作为 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

好吧，我对 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 ...

此错误意味着您正在尝试将一种类型与“更大”的类型统一，即包含它( 例如:unifying 'a with '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)

现在让我们回到 添加 术语并对其进行一些注释，看看打字机要说什么:

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

这变得有趣了:为什么第一个 arg 被输入为“教堂教堂”？
答案如下:这里，一个教堂整数是一个值，它采用一个可以浏览空间的移动函数( 'a -> 'a )，以及一个属于该空间的起点( 'a ) .
在这里，如果我们指定参数 a 的类型为 'a Church ，那么 'a _0x104569 表示我们可以移动的空间。
由于 SUCC 的一个的移动功能，工作在教堂，比“这里是自我的”教堂，从而使参数一个的“教会教堂。
这根本不是我们一开始想要的类型……但这证明了为什么类型系统不允许您的值 三个 和 四个 作为 _60x79 的第一个和 snd 参数 add.607920
一种解决方案可以是以不同的方式编写 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

但是这个解决方案比你最初的解决方案要冗长一些。
希望很清楚。