为什么 OCaml 有时需要 eta 扩展? [英] Why does OCaml sometimes require eta expansion?

问题描述

如果我有以下 OCaml 函数:

If I have the following OCaml function:

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

它在 Utop 中运行良好，并且 Merlin 不会将其标记为编译错误.但是，当我尝试编译它时，出现以下错误:

It works fine in Utop, and Merlin doesn't mark it as a compilation error. When I try to compile it, however, I get the following error:

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

Error: The type of this expression, (int, '_a) CCVector.t -> (int, '_b) CCVector.t, contains type variables that cannot be generalized

如果我对它进行 eta-expand，那么它编译得很好:

If I eta-expand it however then it compiles fine:

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

所以我想知道为什么它不以 eta-reduced 形式编译，以及为什么 eta-reduced 形式似乎在顶层 (Utop) 中工作但在编译时不起作用?

So I was wondering why it doesn't compile in eta-reduced form, and also why the eta-reduced form seems to work in the toplevel (Utop) but not when compiling?

哦，CCVector 的文档在这里.'_a 部分可以是`RO 或`RW，具体取决于它是只读的还是可变的.

Oh, and the documentation for CCVector is here. The '_a part can be either `RO or `RW, depending whether it is read-only or mutable.

推荐答案

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

What you got here is the value polymorphism restriction of ML language family.

限制的目的是将 let 多态性和副作用一起解决.例如，在以下定义中:

The aim of the restriction is to settle down let-polymorphism and side effects together. For example, in the following definition:

let r = ref None

r 不能有多态类型 'a option ref.否则:

r cannot have a polymorphic type 'a option ref. Otherwise:

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用于这两种不兼容的类型.

is wrongly type-checked as valid, but it crashes, since the reference cell r is used for these two incompatible types.

为了解决这个问题，80年代做了很多研究，价值多态就是其中之一.它将多态性限制为仅允许定义形式为非扩展性"的绑定.Eta 扩展形式是非扩展的，因此 myFun 的 eta 扩展版本具有多态类型，但不是 eta 缩减的类型.(更准确地说，OCaml 使用了这种值多态的宽松版本，但故事基本相同.)

To fix this issue many researches were done in 80's, and the value polymoprhism is one of them. It restricts polymorphism only to let bindings whose definition form is "non-expansive". Eta expanded form is non expansive therefore your eta expanded version of myFun has a polymorphic type, but not for eta reduced one. (More precisely speaking, OCaml uses a relaxed version of this value polymorphism, but the story is basically the same.)

当 let 绑定的定义扩展时，没有引入多态性，因此类型变量是非通用的.这些类型在顶层打印为'_a，它们的直观含义是:以后必须将它们实例化为某种具体类型:

When the definition of let binding is expansive there is no polymorphism introduced therefore the type variables are left non-generalized. These types are printed as '_a in the toplevel, and their intuitive meaning is: they must be instantiated to some concrete type later:

# 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:

We can fix the type '_a after the definition:

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

一旦修复，您将无法更改类型，从而防止上述崩溃.

Once fixed, you cannot change the type, which prevents the crash above.

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

This typing delay is permitted until the end of the typing of the compilation unit. The toplevel is a unit which never ends and therefore you can have values with '_a type variables anywhere of the session. But in the separated compilation, '_a variables must be instantiated to some type without type variables till the end of ml file:

(* 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 函数与编译器发生的情况.

This is what is happening with your myFun function with the compiler.

AFAIK，多态性和副作用的问题没有完美的解决方案.和其他解决方案一样，值多态限制也有它自己的缺点:如果你想要一个多态值，你必须在非扩展中定义:你必须 eta-expand myFun.这有点糟糕，但被认为是可以接受的.

AFAIK, there is no perfect solution to the problem of polymorphism and side effects. Like other solutions, the value polymorphism restriction has its own drawback: if you want to have a polymorphic value, you must make the definition in non-expansive: you must eta-expand myFun. This is a bit lousy but is considered acceptable.

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

You can read some other answers:

• http://caml.inria.fr/pub/old_caml_site/FAQ/FAQ_EXPERT-eng.html#variables_de_types_faibles
• 'a 和 '_l 有什么区别?
• 或按值限制毫升"之类的方式搜索

这篇关于为什么 OCaml 有时需要 eta 扩展?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！