函数式编程中的部分应用和柯里化

Question

已经好几个小时了，我无法理解 OCaml 中的这个示例。

我不知道该怎么想，所以我会尝试给出我的思考过程。

问题是：对于每个定义或表达式，给出类型和值（包括）

这是整个代码（顶层）：

let rec church_of_int n = 
    if n = 0 then fun f x -> x
    else fun f x -> church_of_int (n-1) f (f x);;

let three f x = church_of_int 3 f x;;

three (fun x -> x + 1) 0;;

three three (fun x -> x + 1) 0;;

1) 第一个区块

let rec church_of_int n = 
  if n = 0 then fun f x -> x
  else fun f x -> church_of_int (n-1) f (f x);;

这是一个由于 int 运算符“-”n-1 而采用 int 的函数，并返回一个带有两个参数 'a 和 'b 的函数。由于fun f x -> x，返回的函数返回相同类型的'b。

因此类型是：

int -> ('a -> 'b) -> 'b = <fun>

但是顶层说：

val church_of_int : int -> ('a -> 'a) -> 'a -> 'a = <fun>

我不明白...

2) 第二块

let three f x = church_of_int 3 f x;;

对于第二个块，三接受一个函数和一个 int 并将其应用于 Church_of_int 的返回函数。

因此，类型为：

('a -> 'b) -> int -> 'b = <fun>

顶层说：

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

3) 第三块

three (fun x -> x + 1) 0;;

在这里，我们将一个函数和一个 int 应用于三个。

我们需要计算

church_of_int 3 (fun x -> x + 1) 0

church_of_int 3 = fun f x -> church_of_int 2 f (f x)

church_of_int 2 = fun f x -> church_of_int 1 f (f x)

church_of_int 1 = fun f x -> church_of_int 0 f (f x)

church_of_int 0 = fun f x -> x

那么

church_of_int 1 = fun f x -> ((fun f x -> x) f (f x)) = fun f x -> f x

church_of_int 2 = fun f x -> ((fun f x -> f x) f f(x)) = fun f x -> f (f x)

church_of_int 3 = fun f x -> ((fun f x -> f (f x)) f f(x)) = fun f x -> f (f (f x))

因此，

church_of_int 3 (fun x -> x + 1) 0 = 3

Toplevel 确认这是正确的。

4) 第四块

three three (fun x -> x + 1) 0;;

这里变得非常混乱。一方面，我们知道three (fun x -> x + 1) 0 = 3

然后

三3是偏应用

另一方面，顶层返回 27。

你能帮我改正我的错误和我的思维过程以获得正确的类型和结果吗？

Answer 1

这是一个函数，由于 int 运算符 "-" n-1 而采用 int 并返回一个带有两个参数 'a 和 'b 的函数。由于fun f x -> x，返回的函数返回相同类型的'b。 因此类型是：

int -> ('a -> 'b) -> 'b = <fun>

让我们仔细看看定义，

let rec church_of_int n = 
 if n = 0 then fun f x -> x
 else fun f x -> church_of_int (n-1) f (f x)

从if 表达式的第一个分支我们确实可以推断出返回类型是一个接受两个参数并返回最后一个参数的函数，即

int -> ('a -> 'b -> 'b)

我们可以重写（使用 -> 类型运算符 as 的右关联性），

int -> 'a -> 'b -> 'b

请注意，您的思路是如何偏离正确路径的 - 因为您表示一个函数，该函数接受两个参数并将第二个参数返回为 ('a -> 'b) -> 'b。你把括号放错了，实际上你的类型代表了一个接受单个参数的函数，它本身就是一个接受任何参数并返回类型为'b的值的函数。

但是让我们回到我们的定义。我们只使用了来自if 表达式的一个分支的信息，因此我们错过了一些可用信息。从else分支church_of_int (n-1) f (f x)我们可以看到第一个参数（我们用'a赋予的类型）是一个函数本身，因为应用程序(f x)，所以我们可以将'a细化为函数类型。我们看到它被应用到x，我们知道它的类型是'b，而且应用的结果被传递给第二个参数，我们从第一个分支推断为'b，所以我们知道f 的类型是 'b -> 'b。现在我们将'a 替换为('b -> 'b) 并得到，

int -> ('b -> 'b) -> 'b -> 'b

这相当于 OCaml 顶层推断的类型的模变量名称。

那么这种类型是什么意思，或者更具体地说，church_of_int n 表达式定义了什么？此函数将n 乘以传递的函数f 应用于传递的参数x。参数的类型无关紧要，因为我们从不使用它，我们只是将f 应用于它n 次。

有了这些知识，我们可以轻松消化let three f x = church_of_int 3 f x。它将f 应用于x 三次。所以类型是('a -> 'a) -> 'a -> 'a（我们仍然等待f和x被传递）。

如果我们将fun x -> x + 1 作为函数传递，0 作为初始值传递，那么three (fun x -> x + 1) 0 是该函数对0 的三重应用。让我们将fun x -> x + 1 命名为succ，所以three succ 0 是succ (succ (succ 0)))，即零的第三个后继，即三。

现在是最难的部分，让我们试着理解three three (fun x -> x + 1) 0 表达式。首先，我们把它改写成three three succ 0。

您可能遇到的第一个问题是为什么three 能够接受两个以上的参数？由于three 的类型为('a -> 'a) -> 'a -> 'a，第二个参数'a 本身可能是一个函数。我们知道succ 的类型为int -> int，所以我们将'a 替换为(int -> int)，

((int -> int) -> (int -> int)) -> (int -> int) -> (int -> int)

让我们删除一些括号，

((int -> int) -> int -> int) -> (int -> int) -> int -> int

这给了我们一个接受三个参数的函数，

• 函数three，类型为((int -> int) -> int -> int)，
• 函数succ 类型为(int -> int)
• 初始参数0 类型为int

而three three succ 将three 应用于succ 三次。所以让我们展开它，

three three succ
===========================
three (three (three succ))

我们已经知道three succ 将3 添加到传递的参数中，所以它是x + 3，我们将其命名为plus3 并重写，

three three succ
===========================
three (three (three succ))
=================== (three succ => plus3)
three (three plus3)

如果我们将plus3重复三遍，即x + 3 + 3 + 3，这与x + 9相同，所以我们可以重写为，

three three succ
=========================== 
three (three (three succ))
=================== (three succ => plus3)
three (three plus3)
=================== (three plus3 => plus9)
three plus9

现在，最后一步，重复x + 9 + 9 + 9 是x+27，所以我们可以进行最后的重写，

three three succ
=========================== 
three (three (three succ))
=================== (three succ => plus3)
three (three plus3)
=================== (three plus3 => plus9)
three plus9
=========== (three plus9 => plus27)
plus27

所以最后three three succ x 创建了一个在语义上等价于fun x -> x + 27 的函数，而three three succ 0 给了我们27。

Answer 2

第一部分

让我们考虑一下：

let rec church_of_int n =
    if n = 0 then fun f x -> x
    else fun f x -> church_of_int (n-1) f (f x)

我们可以在这里推断出什么类型？

显然，您已经确定 n 必须是 int，因为它同时被减去并与另一个 int 进行比较。

int -> ... -> ... -> ...

举个例子，如果我们调用church_of_int 3，那会是什么样子？它返回一个函数，该函数接受一个函数，该函数接受一个函数f 和一个值x，我们将其表示为类型'a。所以f 接受'a 类型的值并将其转换为...

好吧，f x 的结果传递给 church_of_int 需要 a 类型的值，所以 f 的类型必须是 'a -> 'a。

既然我们知道了f和x的推断类型，我们就可以完成church_of_int的类型签名了。

int -> ('a -> 'a) -> 'a -> 'a

第二块

关于：

let three f x = church_of_int 3 f x

这可能只是以下使用部分应用程序。

let three = church_of_int 3

在这种情况下，类型签名 ('a -> 'a) -> 'a -> 'a 不应该令人惊讶。

第三块

three (fun x -> x + 1) 0

让我们考虑一下这是如何计算的，(fun x -> x + 1) 被替换为加法运算符 ((+) 1) 的部分应用。

church_of_int 3 ((+) 1) 0

3 不等于 0，所以我们返回 fun f x -> church_of_int (n-1) f (f x)，我们将其应用于 (3 - 1)、((+) 1) 和 ((+) 1) 0。

所以现在我们调用了：

church_of_int 2 ((+) 1) 1

评估这个，我们得到：

church_of_int 1 ((+) 1) 2

因为1 不是0：

church_of_int 0 ((+) 1) 3

不过，现在n 是 0，所以我们得到了一个函数，其中f 永远不会应用于任何东西，所以没关系。我们只返回x，即3。

第四部分

再次考虑three的定义。

let three = church_of_int 3

类型是：

('a -> 'a) -> 'a -> 'a

three 的第一个参数是将'a 类型的值映射到另一个相同类型的值的函数。让我们稍微重写一下那个类型签名。

('a -> 'a) -> ('a -> 'a)

如果我们部分应用three three，我们会得到一个具有以下类型的函数，它看起来很像three 的类型。

('_a -> '_a) -> '_a -> '_a

将three 应用到three 的效果是得到另一个函数，该函数接受一个新函数，该函数接受一个函数和一个初始值。我们可以无休止地应用它。如果我们这样看，也许语法更有意义：

let f = ((+) 1 in
((three three) f) 0

我们可以通过定义更多的函数来看到这种“求幂”。

─( 10:02:30 )─< command 42 >----
utop #
let two f x = church_of_int 2 f x
let three f x = church_of_int 3 f x
let four f x = church_of_int 4 f x;;
val two : ('a -> 'a) -> 'a -> 'a = <fun>
val three : ('a -> 'a) -> 'a -> 'a = <fun>
val four : ('a -> 'a) -> 'a -> 'a = <fun>
─( 10:02:39 )─< command 43 >----
utop #
let inc x = x + 1;;
val inc : int -> int = <fun>
─( 10:03:05 )─< command 44 >----
utop # two two inc 0;;
- : int = 4
─( 10:03:13 )─< command 45 >----
utop # two four inc 0;;
- : int = 16
─( 10:03:21 )─< command 46 >----
utop # two two two inc 0;;
- : int = 16
─( 10:03:30 )─< command 47 >----
utop # two two four inc 0;;
- : int = 256