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就是这样做的。然而，这里有一个问题:您必须确保引用永远不会"转义"monad。Psuedocode:

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

run的存在让我们回到开始的地方:

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)，它可以没有一个rununio或类似的
• ST单子使用一个技巧与排名2类型，以确保引用是不可用的，一旦单子退出，允许本地可变状态，同时保持声音。

对于第二种情况，你可以这样写:

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)。