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

Question

作为一种消遣，我正在尝试解决我在大学学习的课程（涉及 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 问题），然后在调用一次闭包后解决该错误。但是，我似乎不明白为什么在这种情况下会抛出类型不一致错误：

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 的类型系统不允许写 Church 数字。

\n

这里真正的问题是你的加法项：

\n

let add a b = b succ a\n

\n

有以下类型

\n

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

\n

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

\n

let double a = add a a (* produces type error - the type variable occurs ... *)\n

\n

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

\n

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

\n

现在让我们回到add术语并对其进行一些注释，看看打字员会说什么：

\n

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

\n

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

\n

'a church church -> 'a church -> 'a church\n

\n

这变得很有趣：为什么第一个参数被输入为'a Church Church？

\n

答案如下：这里，教堂整数是一个值，它采用类型为'a -> 'a的移动函数（mlahematics 中的自映射），可以浏览空间，以及一个起始点( 'a )属于那个空间。

\n

在这里，如果我们指定参数a 的类型为'a Church，则'a表示我们可以移动的空间。\n因为a的移动函数succ在教堂上运行，所以'a本身就是一个'a Church，从而使参数a成为 ' a Church Church。

\n

这根本不是我们一开始想要的类型......但这证明了为什么类型系统不允许您的值三和四作为add的第一个和第二个参数。

\n

一种解决方案是以不同的方式编写 add ：

\n

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

\n

在这里，a和b都具有相同的移动功能，因此具有相同的类型，但您不再享受部分应用的美丽书写......

\n

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

\n

type nat = {f:'a.('a -> 'a) -> 'a -> 'a}\n(* this means \xe2\x80\x9cfor all types \xe2\x80\x98a\xe2\x80\x9d *)\n\nlet zero : nat = {\n  f=fun f x -> x\n}\n\nlet succ n : nat = {\n  f= fun f x -> f (n.f f x)\n}\n\nlet add (a:nat) (b:nat) = a.f succ b\n\nlet double a = add a a (* Now this has a correct type *)\n\nlet nat_to_int n =\n  n.f (fun x -> x + 1) 0;;\n\nlet nat_four = succ (succ (succ (succ zero)))\n\nlet eight_i = double nat_four |> nat_to_int //returns 8\n

\n

但这个解决方案比您最初的解决方案更冗长一些。

\n

希望它是清楚的。

\n