OCaml 类型推断不会产生函数参数的预期类型

Posted 2023-02-19

【中文标题】OCaml 类型推断不会产生函数参数的预期类型

【英文标题】：OCaml type inference does not yield expected type for function arguments

【发布时间】：2022-01-15 23:24:54

【问题描述】：

这是一个家庭作业。我知道我不应该在这里问这个，但欢迎解释。 :)

我的代码是这样的：

let some_function f x = match x with 
  | (k, v) -> fun k -> f k

f 应该是一个函数，x 是一个元组列表。 我的编译器（？）说 ('a -> 'b) -> 'c * 'd -> 'a -> 'b 但应该是('a -> 'b) -> 'a * 'b -> 'a -> 'b

您无需告诉我解决方案，只需解释一下为什么是 'c * 'd 而不是 'a * 'b

【参考方案1】：

首先，当你写这个时：

let some_function f x = match x with 
  | (k, v) -> fun k -> f k

您可以直接在函数参数中进行模式匹配。

let some_function f (k, v) = 
  fun k -> f k

其次，v 从未使用过，所以让我们使用_ 来消除它。

let some_function f (k, _) = 
  fun k -> f k

这完全一样，让我们​​更容易推理。

但是，fun k -> f k 中的 k 会影响函数元组参数中的 k，因此您并没有真正使用那个。

所以我们真的有：

let some_function f (_, _) = 
  fun k -> f k

它们的具体类型未知，因此f 被推断为接受'a 类型的值并返回'b 类型的值的函数。因此f 是'a -> 'b。

你从不使用的元组？它有一个类型，但我们无法从函数的其余部分了解这些类型，因此推断的类型是'c * 'd。

我们可以进一步简化这一步骤。 fun k -> f k 相当于只写f，所以你的函数可以等价地重写：

let some_function f (_, _) = f

虽然这不允许 OCaml 推断出 f 是一个函数，所以类型签名变为：

'a -> 'b * 'c -> 'a

【讨论】：

首先：非常感谢您向我解释“有趣”（呵呵）！以前不知道那个！但它仍然不是('a -> 'b) -> 'a * 'b -> 'a -> 'b 还是还是一样？我以为我会有所作为:)

这并不适用于每次使用fun，但在这种情况下它适用。

OCaml 非常适合代数。如果您看到f(x) = g(x)，您就会知道f = g。在这种情况下，您基本上看到的是相同的东西。如果您正在使用带有参数的fun 创建一个匿名函数，并且您将一个函数应用到同一个参数而不进行修改，则该匿名函数与您正在应用的函数相同。