函数式推理混乱

Question

假设我在ocaml中有以下代码：

# let func a b = b a;;
val func : 'a -> ('a -> 'b) -> 'b = <fun>

函数类型是有意义的，因为我们可以看到，在rhs中，b是一个以a为参数的函数，因此b的类型是('a ->'b)，这也意味着结果是'b类型和a is 'a类型。所以我们得到了val func : 'a -> ('a -> 'b) -> 'b = <fun>。

然而，我不明白的是

# let func a b c = a b c;;
val func : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c = <fun>

按照第一个问题中的逻辑，它在rhs a中是一个接受b和c的函数，而b也是一个接受c的函数。很明显，a的类型是('a->'b->'c)，b的类型是('a->'b)，c的类型就是'a。所以，我得到的函数类型是(type of a) -> (type of b) -> (type of c) -> result，并替换了上面的逻辑，我得到了('a -> 'b ->'c) -> ('a ->'b) -> 'a -> 'c，但这显然不是真正的func类型。有人能解释一下我的逻辑有什么问题吗？

而且，如果我写的let func a b c = a b c没有任何糖，会是let func = fun a -> fun b -> (fun c -> a b c)吗？谢谢

Answer 1

您在问题中说：“b也是一个接受c的函数”

这是你推理出错的地方。这并不是一个存在的约束。从表面上看，b似乎适用于c，但它不是，它只是a的第二个参数，而c是a的第三个参数。

更清楚的是，如果您将优先级显式地加上一些括号，则b永远不会应用于c：

# let func a b c = (a b) c;;
val func : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c = <fun>

如果您编写了let func a b c = ignore (b c) ; a b c;;，那么b将是一个应用于c的函数。在这种情况下，推理是适用的，您可以：

# let func a b c = ignore (b c) ; a b c;;
val func : (('a -> 'b) -> 'a -> 'c) -> ('a -> 'b) -> 'a -> 'c = <fun>

你的第二个问题是：

也是，如果我写没有糖的let func a b c = a b c，会是let func = fun a -> fun b -> (fun c -> a b c)吗？

是的，前者只是后者的一个简明表示法。括号甚至没有必要：

# let func = fun a -> fun b -> fun c -> a b c;;
val func : ('a -> 'b -> 'c) -> 'a -> 'b -> 'c = <fun>

Answer 2

您的“显然”实际上是错误的，至少就您正在考虑的b和c的类型而言是这样。如果将类型变量重命名略有不同，可能会更清楚：

# let func a b c = a b c;;
val func : ('b -> 'c -> 'd) -> 'b -> 'c -> 'd = <fun>

这是相同的，只是为类型变量的名称启动一个'b。现在它可能更清楚了：a的类型是'b -> 'c -> 'd，而b的类型是'b，而c的类型是'c。函数接受三个参数，将后两个参数(b和c)传递给第一个参数(a)，并返回它返回的内容('d类型的值)。