为啥 OCaml 有时需要 eta 扩展？

Posted 2023-03-15

【中文标题】为啥 OCaml 有时需要 eta 扩展？

【英文标题】：Why does OCaml sometimes require eta expansion?为什么 OCaml 有时需要 eta 扩展？

【发布时间】：2014-11-03 23:36:49

【问题描述】：

如果我有以下 OCaml 函数：

let myFun = CCVector.map ((+) 1);;

它在 Utop 中运行良好，而且 Merlin 没有将其标记为编译错误。但是，当我尝试编译它时，出现以下错误：

错误：这个表达式的类型， (int, '_a) CCVector.t -> (int, '_b) CCVector.t, 包含无法泛化的类型变量

如果我对它进行 eta 扩展，那么它编译得很好：

let myFun foo = CCVector.map ((+) 1) foo;;

所以我想知道为什么它不能以 eta-reduced 形式编译，以及为什么 eta-reduced 形式似乎在顶层（Utop）中工作，但在编译时却不行？

哦，CCVector 的文档是here。 '_a 部分可以是 `RO 或 `RW，这取决于它是只读的还是可变的。

【问题讨论】：

我注意到你已经在上面添加了haskell 标签。尽管 Haskell 具有“可怕的单态性限制”，乍一看其行为与 Ocaml 的值限制模糊地相似，但这两种限制的原因非常不同。 Ocaml 使用它来驯服副作用，但 Haskell 是纯的，所以不需要它。 Haskell 的限制可以防止对值进行意外的重新评估，而且这并非绝对必要 - 对于某些类型的代码，它更烦人而不是有用，并且有一个流行的选项可以将其关闭。

它们比你第一眼看到的更相似。

【参考方案1】：

你在这里得到的是 ML 语言家族的值多态性限制。

限制的目的是解决 let 多态性和副作用。例如，在以下定义中：

let r = ref None

r 不能有多态类型'a option ref。否则：

let () =
  r := Some 1;       (* use r as int option ref *)
  match !r with
  | Some s -> print_string s  (* this time, use r as a different type, string option ref *)
  | None -> ()

被错误地类型检查为有效，但它崩溃了，因为引用单元格r 用于这两种不兼容的类型。

为了解决这个问题，80年代进行了许多研究，价值多态性就是其中之一。它将多态性限制为只允许定义形式为“非扩展”的绑定。 Eta 扩展形式是非扩展的，因此您的 myFun 的 eta 扩展版本具有多态类型，但不适用于 eta 缩减类型。 （更准确地说，OCaml 使用了这种值多态的宽松版本，但故事基本相同。）

当 let 绑定的定义是扩展的时，没有引入多态性，因此类型变量是非泛化的。这些类型在顶层打印为'_a，其直观含义是：后面必须实例化为某种具体类型：

# let r = ref None                           (* expansive *)
val r : '_a option ref = contents = None   (* no polymorphism is allowed *)
                                             (* type checker does not reject this,
                                                hoping '_a is instantiated later. *)

我们可以在定义后修复'_a的类型：

# r := Some 1;;                              (* fixing '_a to int *)
- : unit = ()
# r;;
- : int option ref = contents = Some 1     (* Now '_a is unified with int *)

一旦修复，你就不能改变类型，这样可以防止上面的崩溃。

这种输入延迟是允许的，直到编译单元的输入结束。顶层是一个永不结束的单元，因此您可以在会话的任何位置使用'_a 类型变量的值。但是在分离编译中，'_a变量必须实例化为某种没有类型变量的类型，直到ml文件结束：

(* test.ml *)
let r = ref None (* r : '_a option ref *)
(* end of test.ml. Typing fails due to the non generalizable type variable remains. *)

这就是您的 myFun 函数与编译器发生的情况。

AFAIK，多态性和副作用问题没有完美的解决方案。与其他解决方案一样，值多态性限制也有其自身的缺点：如果要具有多态值，则必须将定义设为非扩展：必须 eta-expand myFun。这有点糟糕，但被认为可以接受。

您可以阅读其他一些答案：

http://caml.inria.fr/pub/old_caml_site/FAQ/FAQ_EXPERT-eng.html#variables_de_types_faibles What is the difference between 'a and '_l? 或通过类似“值限制 ml”进行搜索