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

问题描述

如果我有以下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简化的形式编译，为什么eta - 减少的形式似乎在顶层（Utop）工作，但不是编译时？

哦，CCVector的文档是此处。 '_a部分可以是'RO'或'RW'，具体取决于它是只读的还是可变的。

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

限制的目的是一起解决let-polymorphism和副作用。例如，在以下定义中：

  let r = ref无
  

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

  let（）= 
 r：=大概1; （*使用r作为int选项ref *）
 match！r with 
 |一些s  - > print_string s（*这次，使用r作为不同的类型，字符串选项ref *）
 |无 - > （）
  

是错误的类型检查为有效，但它崩溃，因为引用单元 r 用于这两种不兼容的类型。为了解决这个问题，许多研究都是在80年代完成的，而多元主义的价值就是其中之一。它限制多态只能让定义形式为非扩展性的绑定。 Eta扩展形式是非扩展的，因此，您的eta扩展版本的 myFun 具有多态类型，但不会为eta减少一个。 （更准确地说，OCaml使用了这个值多态的宽松版本，但故事基本上是一样的）。

当let绑定的定义是扩展的时，没有因此引入了多态性，因此类型变量不会被广义化。这些类型在顶层打印为'_ a ，它们的直观含义是：它们必须稍后被实例化为一些具体类型：

 ＃let r = ref None（* expansive *）
 val r：'_a option ref = {contents = None}（* no polymorphism is allowed *） 
（*类型检查器不拒绝这个，
希望'_a稍后被实例化。*）
  

我们可以在定义之后修正类型'_ a >

 ＃r：=有些1 ;; （*固定'_a到int *）
  - ：unit =（）
＃r ;; 
  - ：int option ref = {contents = Some 1}（*现在'_a与int *统一）
  

一旦修正，您将无法更改类型，从而防止上面的崩溃。

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

 （* test.ml *）
 let r = ref None（* r：'_a option ref * ）
（* test.ml.的结尾）由于非泛化类型变量，输入失败。*）
  

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

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

您可以阅读其他答案：

• http://caml.inria.fr/ pub / old_caml_site / FAQ / FAQ_EXPERT-eng.html＃variables_de_types_faibles


• a和_l之间的差别


• 或者通过类似value restriction ml进行搜索

If I have the following OCaml function:

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

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:

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

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

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

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?

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.

解决方案

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

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 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 -> ()

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

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.)

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. *)

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.

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. *)

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

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
• What is the difference between 'a and '_l?
• or search by like "value restriction ml"

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