ML 中的单子和值限制

Question

ML 中的 值限制 可防止在可能破坏类型安全的上下文中进行类型泛化。核心问题似乎是由序列突变和多态类型的组合引起的，例如在这个 OCaml 代码中：

let x = ref [];;  (* value restriction prevents generalization here *)

x := 1::!x;;      (* type unification with int *)
x := true::!x;;   (* error *)

如果没有值限制，最后一行将进行类型检查而不会出错，因为 x 的多态类型将与 bool 统一。为了防止这种情况，x 的类型必须保持单态。

我的问题如下：是否可以通过使用 monad 来表达操作序列来消除值限制？

作为函数参数，通过monad的bind操作引入的变量在整个序列中保持单态，因此在泛化时似乎没有引入特殊情况就达到了与值限制相同的效果。

这行得通吗？如果不行，为什么？

Answer 1

是的，这基本上是可行的，Haskell 就是这样做的。然而，有一个障碍：你必须确保引用永远不会 "escapes" monad。伪代码：

module MutMonad : sig
  (* This is all sound: *)
  type 'a t
  type 'a ref

  val mkref : 'a -> ('a ref) t
  val read_ref : 'a ref -> 'a t
  val write_ref : 'a -> 'a ref -> unit t

  (* This breaks soundness: *)
  val run : 'a t -> 'a
end

运行的存在让我们回到起点：

let x = run (mkref []) in (* x is of type ('a list) ref *)
run (read_ref x >>= fun list -> write_ref (1::list) x);
run (read_ref x >>= fun list -> write_ref (true::list) x)

Haskell 通过两种方式解决这个问题：

因为 main 已经是单子类型 (IO)，它可以没有运行IO 或类似的。
ST monad 使用 rank 2 类型的技巧来确保引用在 monad 退出后不可用，允许局部可变状态同时保持正常。

对于第二种情况，你有类似的东西：

module MutMonad : sig
  (* The types now take an extra type parameter 's,
     which is a phantom type. Otherwise, the first
     bit is the same: *)
  type 'a 's t
  type 'a 's ref

  val mkref : 'a -> ('a 's ref) 's t
  val read_ref : 'a 's ref -> 'a 's t
  val write_ref : 'a -> 'a 's ref -> unit 's t

  (* This bit is the key. *)
  val run : (forall 's. 'a 's t) -> 'a
end

类型级别的 forall 's. ... 类似于 fun x -> ...。 's 是本地绑定变量，因此运行的参数不能假设关于 's 的任何内容。特别是，这不会类型检查：

let old_ref = run (mkref 3) in
run (read_ref old_ref)

因为运行的参数不能假定它们传递给 's 的相同类型。

这需要 ocaml 中不存在的类型系统功能，并且需要 Haskell 中的语言扩展 (Rank2Types)。

ML 中的单子和值限制

Monads and value restriction in ML

monads

ml

value-restriction