如果我具有以下OCaml函数:
let myFun = CCVector.map ((+) 1);;
它在Utop中运行良好,Merlin并未将其标记为编译错误。但是,当我尝试编译它时,出现以下错误:
错误:此表达式的类型(int,'_a)CCVector.t->(int,'_b)CCVector.t包含无法归纳的类型变量
如果我对它进行eta-expand编译,则编译良好:
let myFun foo = CCVector.map ((+) 1) foo;;
因此,我想知道为什么它不能以eta简化的形式进行编译,以及为什么eta简化的格式似乎可以在顶级(Utop)中工作,但在编译时却不能使用?
哦,这里是CCVector的文档。'_a部分可以是`RO或`RW,取决于它是只读的还是可变的。
您在这里得到的是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扩展形式不可扩展,因此您的eta扩展版本myFun
具有多态类型,但不适用于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
。这有点糟糕,但被认为可以接受。
您还可以阅读其他答案:
本文收集自互联网,转载请注明来源。
如有侵权,请联系[email protected] 删除。
我来说两句