为什么 `ref None` 值在 Ocaml 中受到限制？答案

【问题标题】：Why is `ref None` value restricted in Ocaml?为什么 `ref None` 值在 Ocaml 中受到限制？
【发布时间】：2018-06-10 09:11:46
【问题描述】：

值限制规则说，只有当表达式的右侧在语法上是一个值时，才能进行泛化。

我不明白为什么let r = ref None 会受到价值限制？为什么ref (Some 2) 是一个值而ref None 不是？

None 是不是就像一个类型构造函数？ None 不是一个值？在我看来，None 是一个多态值。有没有多态值之类的东西？

在我看来，当与多个多态实体（例如 id id 或 ref None）进行某种交互时，就会出现值限制。

我是 OCaml 的初学者，正在自学。任何帮助表示赞赏。

【问题讨论】：

ref None 是一个值（ref (Some 2) ... 也是如此）。值限制规则是关于类型的。键入发生在编译时。值在运行时存在。
我在这里读到的mlton.org/ValueRestriction ref None 不是一个值。
我正在通过stackoverflow.com/questions/42149525/…中给出的语法值的更精确定义

标签： polymorphism ocaml

【解决方案1】：

ref None 和 ref (Some 2) 都不是用于值限制的值。它们都是函数ref的应用程序。

谈论泛化ref (Some 2) 是没有意义的，因为不可能存在多态性。

None 是一个值，但ref None 不是一个值（在用于值限制的句法意义上）。由于None 是一个可以泛化的值（所以它是多态的）：

# let my_none = None;;
val my_none : 'a option = None

# let f x = if x then Some 3 else my_none;;
val f : bool -> int option = <fun>
# let g x = if x then Some "abc" else my_none;;
val g : bool -> string option = <fun>

由于my_none 是多态的，它可以用作int option 类型的值，也可以用作string option 类型的值。

更新

OCaml 有一个“宽松”的值限制，其中一些不是语法值的东西仍然可以被泛化（多态）。

您可以在我经常引用的这篇论文中阅读有关放宽值限制的内容。（我也会定期重读它，因为随着时间的推移我往往会忘记这个论点。）

Jacques Garrigue, Relaxing the Value Restriction

【讨论】：

好吧，这是有道理的，所以这里去掉了值限制中的值概念是“句法值”的概念，我们不会将函数应用程序视为句法值，因为它们会进行一些计算。
虽然，我想知道为什么像 ref None 这样的东西不是句法值，而像 id None 这样的东西是？其中let id = fun x -> x
id None 不是句法值。这是函数id 的应用。但是，OCaml 有一个 relaxed 值限制。有一篇很棒的论文可供阅读；我会将链接添加到我的答案中。
非常感谢。非常感谢您的帮助。

【解决方案2】：

可变状态不得是多态的。 ref 案例是价值限制首先存在的原因。考虑：

let r = ref None in     (* consider this was r : 'a option ref *)
r := Some "boo";        (* then this would be well-typed *)
unSome (!r) + 1         (* and this would be well-typed as well -- BOOM! *)

unSome 是一个助手：

let unSome = function Some x -> x | None -> raise Not_found

【讨论】：