在OCaml中,宽松的价值限制什么时候开始？

Question

有人可以简单描述放松的价值限制何时开始？我很难找到简明扼要的规则描述.那是加里格的论文:

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

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

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

因此,当你有(仅将出现的)单态变量出现在协变位置时,放宽的值限制就会启动.

(我希望我有这个权利.当然,正如octref建议的那样,@ gasche会做得更好.)

Answer 2

杰弗里提供了放松正确原因的直观解释.至于什么时候它有用,我想我们可以先重现有用的链接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是一种幻像区域变量,它保证当它保持多态时,引用代码中变量的范围是正确的.因为这依赖于在引用表达式是通过组合其他引用表达式来构建的情况下的多态性(因此通常不是值),如果没有宽松的值限制,它基本上根本不起作用(这是他在类型上的优秀技术文档中的侧面评论推理).

Answer 3

虽然我对这个理论不是很熟悉，但我还是问了一个问题。
Gasche 为我提供了简洁的解释。该示例只是 OCaml 地图模块的一部分。一探究竟！
也许他能给你更好的答案。@加斯切