9

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

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 的杂散定义会影响启发式。

4

4 回答 4

9

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

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

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

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

于 2013-03-22T03:17:27.403 回答
5

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

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

几个月前，我们在 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是一种幻象区域变量，保证当它保持多态时，引用代码中变量的作用域是正确的。由于在引用表达式是通过组合其他引用表达式（通常不是值）来构建引用表达式的情况下，这依赖于多态性，因此如果没有放宽的值限制，它基本上根本无法工作（这是他关于类型的优秀但技术文档中的一个旁注推理）。

于 2013-03-22T07:32:10.667 回答
2

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

回顾

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

被赋予多态类型 (think ∀ α. 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如果 -expression 的主体和所有绑定变量都是值，则它就是一个值。

在附录中给出的两个示例中，主体都是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 Generalizationgeneralize，generalize_expansive这可能是一个好的开始。

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

于 2015-02-11T10:19:03.757 回答
1

虽然我对这个理论不是很熟悉，但我已经问过一个关于它的问题。
加什向我提供了一个简明的解释。该示例只是 OCaml 地图模块的一部分。一探究竟！
也许他能给你一个更好的答案。@加什

于 2013-03-22T03:17:20.557 回答