4

作为消磨时间，我正在尝试解决我在大学学习的课程（涉及 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
4

2 回答 2

3

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

这里真正的问题是您的附加术语：

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

这很有趣：为什么第一个 arg 被键入为'a Church Church？

答案如下：这里，教堂整数是一个值，它采用可以浏览空间的移动函数（'a -> 'a ）和属于该空间的起点（'a ）。

在这里，如果我们指定参数a 的类型为'a Church，那么'a表示我们可以移动的空间。由于succ （ a的移动函数）在教堂上运行，而不是'a here is it self an 'a Church，因此使参数a为'a Church Church。

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

一种解决方案是以不同的方式编写 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

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

希望很清楚。

于 2017-04-16T08:47:39.960 回答
2

如果您查看三种类型，您会得到：

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

这只是工作中的价值限制。值限制在这里得到了很好的解释：https ://realworldocaml.org/v1/en/html/imperative-programming-1.html#side-effects-and-weak-polymorphism

为了解决这个问题，在这种情况下，您可以简单地对函数进行 eta 扩展：

let three x = int_to_church 3 x ;;
val three : ('a -> 'a) -> 'a -> 'a = <fun>
于 2017-04-15T14:02:35.993 回答