为什么Ocaml中的“ref None”值受限制？

Posted 2021-04-07

值限制规则表明，只有当表达式的右侧在语法上是一个值时，才会发生泛化。

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

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

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

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

答案

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

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

另一答案

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