2

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

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

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

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

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

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

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

4

1 回答 1

1

是的，这基本上是可行的，这就是 Haskell 做事的方式。但是，有一个问题：您必须确保引用永远不会“逃脱” 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

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），它不能有一个 runIO 或类似的。
  • 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 是本地绑定变量，因此 run 的参数不能假设任何关于 's. 特别是，这不会进行类型检查：

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

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

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

于 2017-10-30T21:11:10.710 回答