OCaml 什么时候开始放宽值限制？

Question

有人可以简要说明何时开始放宽价值限制吗？我很难找到对规则的简洁明了的描述。这是 Garrigue 的论文：

http://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf

但它有点密集。有人知道更简洁的来源吗？

附录

下面添加了一些很好的解释，但我无法找到以下行为的解释：

# let _x = 3 in (fun () -> ref None);;
- : unit -> 'a option ref = <fun>
# let _x = ref 3 in (fun () -> ref None);;
- : unit -> '_a option ref = <fun>

任何人都可以澄清以上内容吗？为什么封闭 let 的 RHS 中的 ref 的杂散定义会影响启发式。

Answer 1

我不是类型理论家，但这是我对 Garrigue 解释的解释。你有一个值 V。从通常的值限制下分配给 V（在 OCaml 中）的类型开始。类型中会有一些（可能是 0 个）单态类型变量。对于仅出现在类型中的协变位置（函数箭头右侧）的每个此类变量，您可以将其替换为完全多态的类型变量。

论证如下。由于您的单态变量是一个变量，您可以想象用任何单一类型替换它。所以你选择了一个无人居住的类型 U。现在因为它只处于协变位置，所以 U 可以反过来被任何超类型替换。但是每种类型都是无人居住类型的超类型，因此可以安全地替换为完全多态的变量。

因此，当您拥有（可能是）仅出现在协变位置的单态变量时，宽松的值限制就会生效。

（我希望我有这个权利。当然@gasche 会做得更好，正如 octref 所建议的那样。）

Answer 2

Jeffrey 直观地解释了为什么放松是正确的。至于什么时候有用，我想我们可以先重现答案 octref 有帮助地链接到：

您可以放心地忽略这些细微之处，直到有一天您遇到了一个抽象类型的问题，该类型不像您希望的那样具有多态性，然后您应该记住，签名中的协方差注释可能会有所帮助。

几个月前我们讨论过这个on reddit/ocaml：

考虑以下代码示例：

module type S = sig
  type 'a collection
  val empty : unit -> 'a collection
end

module C : S = struct
  type 'a collection =
    | Nil
    | Cons of 'a * 'a collection
  let empty () = Nil
end

let test = C.empty ()

test 的类型是 '_a C.collection，而不是您期望的 'a C.collection。它不是多态类型（'_a 是一个尚未完全确定的单态推理变量），在大多数情况下你不会对它感到满意。

这是因为C.empty ()不是一个值，所以它的类型不是泛化的（~变成了多态的）。要从放宽的值限制中受益，您必须标记抽象类型 'a collection 协变：

module type S = sig
  type +'a collection
  val empty : unit -> 'a collection
end

当然，这只是因为模块C 被签名S 密封：module C : S = ...。如果模块C 没有给出明确的签名，那么类型系统会推断出最普​​遍的方差（这里是协方差），而人们不会注意到这一点。

针对抽象接口进行编程通常很有用（在定义函子、执行幻像类型规则或编写模块化程序时），所以这种情况肯定会发生，然后了解放宽的值限制很有用。

这是您需要了解它以获得更多多态性的示例，因为您设置了抽象边界（具有抽象类型的模块签名）并且它不会自动工作，您必须明确说明抽象类型是协变的。

在大多数情况下，当您操作多态数据结构时，它会在您没有注意到的情况下发生。 [] @ [] 只有多态类型 'a list 多亏了放松。

一个具体但更高级的示例是 Oleg 的 Ber-MetaOCaml，它使用类型 ('cl, 'ty) code 来表示分段构建的引用表达式。 'ty 表示引用代码的结果类型，'cl 是一种幻象区域变量，它保证当它保持多态时，引用代码中变量的作用域是正确的。由于在引用表达式是通过组合其他引用表达式（因此通常不是值）构建的情况下，这依赖于多态性，因此如果没有放宽的值限制，它基本上根本无法工作（这是他出色但技术性 document 中的一个旁白关于类型推断）。

Answer 3

为什么附录中给出的两个示例的输入方式不同的问题让我困惑了几天。这是我通过深入研究 OCaml 编译器的代码发现的（免责声明：我既不是 OCaml 专家，也不是 ML 类型系统专家）。

回顾

# let _x = 3 in (fun () -> ref None);;        (*  (1)  *)
- : unit -> 'a option ref = <fun>

被赋予多态类型（想想∀ α. unit → α option ref）而

# let _x = ref 3 in (fun () -> ref None);;    (*  (2)  *)
- : unit -> '_a option ref = <fun>

被赋予单态类型（想想unit → α option ref，即类型变量α没有被普遍量化）。

直觉

出于类型检查的目的，OCaml 编译器认为示例 (2) 和

之间没有区别

# let r = ref None in (fun () -> r);;         (*  (3)  *)
- : unit -> '_a option ref = <fun>

因为它不会查看let 的主体以查看是否实际使用了绑定变量（正如人们所期望的那样）。但是 (3) 显然 必须 被赋予单态类型，否则多态类型的参考单元可能会逃逸，从而可能导致不健全的行为，如内存损坏。

扩展性

要理解为什么 (1) 和 (2) 是这样输入的，让我们看看 OCaml 编译器实际上是如何检查 let 表达式是否是一个值（即“非扩展”）（参见is_nonexpansive):

let rec is_nonexpansive exp =
  match exp.exp_desc with
    (* ... *)
  | Texp_let(rec_flag, pat_exp_list, body) ->
      List.for_all (fun vb -> is_nonexpansive vb.vb_expr) pat_exp_list &&
      is_nonexpansive body
  | (* ... *)

所以let-表达式是一个值，如果它的主体和所有绑定的变量都是值。

在附录中给出的两个示例中，主体都是fun () -> ref None，它是一个函数，因此是一个值。两段代码的区别在于3 是一个值，而ref 3 不是。因此 OCaml 认为第一个 let 是一个值，而不是第二个。

打字

再次查看 OCaml 编译器的代码，我们可以看到表达式是否被认为是可扩展的，这决定了 let-表达式的类型如何被泛化（参见 type_expression）：

(* Typing of toplevel expressions *)

let type_expression env sexp =
  (* ... *)
  let exp = type_exp env sexp in
  (* ... *)
  if is_nonexpansive exp then generalize exp.exp_type
  else generalize_expansive env exp.exp_type;
  (* ... *)

由于let _x = 3 in (fun () -> ref None) 是非扩展的，它使用generalize 进行类型化，从而赋予它多态类型。另一方面，let _x = ref 3 in (fun () -> ref None) 是通过 generalize_expansive 输入的，因此是单态类型。

就我所知。如果您想深入挖掘，阅读 Oleg Kiselyov 的 Efficient and Insightful Generalization 以及 generalize 和 generalize_expansive 可能是一个好的开始。

非常感谢剑桥 OCaml Labs 的 Leo White 鼓励我开始挖掘！

Answer 4

虽然我对这个理论不是很熟悉，但我已经问过一个关于它的问题。
gasche 为我提供了a concise explanation。该示例只是 OCaml 的地图模块的一部分。看看吧！
也许他能给你一个更好的答案。 @加什