haskell - 为什么 OCaml 有时需要 eta 扩展?

标签 haskell functional-programming ocaml

如果我有以下 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,具体取决于它是只读还是可变。

最佳答案

这里得到的是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 年代进行了许多研究,值多态性就是其中之一。它限制多态性仅允许定义形式为“非扩展”的绑定(bind)。 eta 扩展形式是非扩展的,因此 myFun 的 eta 扩展版本具有多态类型,但 eta 缩减版本则不然。 (更准确地说,OCaml 使用了这种值多态性的宽松版本,但故事基本相同。)

当 let 绑定(bind)的定义是扩展的时,不会引入多态性,因此类型变量是非泛化的。这些类型在顶层打印为 '_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 *)

一旦修复,您就无法更改类型,这可以防止上述崩溃。

在编译单元的输入结束之前,允许这种输入延迟。顶层是一个永无止境的单元,因此您可以在 session 的任何位置使用 '_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 函数与编译器发生的情况。

据我所知,多态性和副作用问题没有完美的解决方案。与其他解决方案一样,值多态性限制也有其自身的缺点:如果您想要拥有多态值,则必须以非扩展方式进行定义:您必须进行 eta 扩展 myFun。这有点糟糕,但被认为是可以接受的。

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

关于haskell - 为什么 OCaml 有时需要 eta 扩展?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/25763412/

相关文章:

OCaml - GADT - bool 表达式

haskell - Haskell 中的惯用向量代数

haskell - 在 Haskell 中将整数输出到标准输出

haskell - 将高阶函数提升到 monad

scala - 传递函数返回仿函数或单子(monad)类型的困难

tcp - 通过 TCP Erlang 接收错误数据

scala - 是否有 `Optional` 的 van Laarhoven 表示

ocaml - 在 OCAML 中使用 in 关键字

windows - 使用 CMake 在 MinGW 下的 Windows 上构建 LLVM OCaml 绑定(bind)?

Haskell:模板 Haskell 和作用域