函数式语言类型推断混淆

Question

假设我在 ocaml 中有这段代码：

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

函数类型是有道理的，因为我们可以看到在rhs中，b是一个以a为参数的函数，所以b的类型是('a ->'b)，所以这也意味着结果是 'b 类型，而 a 的类型是 '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>

你的第二个问题是：

Also, If I were to write let func a b c = a b c without any sugar would it be 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）和 returns 它 returns（a 'd)

类型的值