在SML中等价于编码rank-2多态性

Question

runST是Haskell函数，通过类型静态约束可用资源的寿命。为此，它使用了rank-2多态性。标准ML更简单的类型系统只提供rank-1多态性。

标准ML是否仍然可以使用类型来约束资源的寿命，从而实现类似的结果？

这个页面和这个页面演示了一些重构代码的方法，只需要更简单的类型就可以。如果我理解正确，核心是将表达式包装起来，以便在上下文中替换为可能的观察结果，这些结果是有限的。这种技术是普适的吗？它或者类似的编码方式能否与像runST这样的东西（显然不是完全相同的签名）一起使用，以防止价值类型逃离被观察到的包装表达式？如果可以，如何实现？

我想象的情境是这样的：

magicRunSTLikeThing (fn resource =>
    (* do things with resource *)
    (* return a value that most definitely doesn't contain resource *)
)

...其中，magic...提供了一种资源，用户提供的代码无法以任何方式共享。显然，像这样的简单界面只有一个库函数是不可能的，但也许通过各种包装、手动内联和提取等方法可以实现...

我看过这篇文章，但如果我理解正确（很可能不是这样），这并不能防止所有对资源的引用被共享，只能确保其中一个引用必须被“关闭”。

基本上，我想在SML中实现安全类型的显式（不是推断式的MLKit风格）区域。

- Alex Celeste

Answer 1

经过一番思考，我认为这是可能的 - 或者至少足够接近以便工作 - 尽管它看起来并不太美观。（我可能完全走了错路，请有知识的人发表评论。）

使用SML的生成数据类型和函数器，可以创建抽象幻影类型，这些类型在给定的词汇块之外无法被引用（我认为这是可能的）：

datatype ('s, 'a) Res = ResC of 's

signature BLOCK = sig
  type t
  val f:('s, t) Res -> t
end

signature REGION = sig
  type t
  val run:unit -> t
end

functor Region(B:BLOCK) :> REGION where type t = B.t = struct
  type t = B.t
  datatype phan = Phan
  fun run () = let
    val ret = (print "opening region\n"; B.f(ResC Phan))
  in print "closing region\n" ; ret end
end

structure T = Region(struct
  type t = int
  fun f resource = ( (* this function forms the body of the "region" *)
    6
  )
end)

;print (Int.toString(T.run()))

这可以防止程序简单地返回resource或声明外部可变变量并将其分配给它，从而解决了大部分问题。但是，在“region”块内创建的函数仍然可以封闭它，并在其所需关闭点之后保留它；这样的函数可能会被导出，并再次使用悬空资源引用，导致问题。

我们可以像模仿ST一样，通过强制该区域使用以虚类型为键的monad，防止闭包能够对resource执行任何有用的操作：

signature RMONAD = sig
  type ('s, 'a, 'r) m
  val ret: ('s * 'r) -> 'a -> ('s, 'a, 'r) m
  val bnd: ('s, 'a, 'r) m * ('a * 'r -> ('s, 'b, 'r) m) -> ('s, 'b, 'r) m
  val get: 's -> ('s, 'a, 'r) m -> 'a * 'r
end

structure RMonad :> RMONAD = struct
  type ('s, 'a, 'r) m = 's -> 's * 'a * 'r
  fun ret (k, r) x = fn _ => (k, x, r)
  fun bnd (m, f) = fn k => let
    val (_, v, r) = m k
  in f (v, r) k end
  fun get k m = let val (_, v, r) = m k in (v, r) end
end

signature MBLOCK = sig
  type t
  val f:(t -> ('s, t, 'r) RMonad.m)  (* return *)
         * ('r -> ('s, string, 'r) RMonad.m) (* operations on r *)
        -> ('s, t, 'r) RMonad.m
end

signature MREGION = sig
  type t
  val run:unit -> t
end

functor MRegion(B:MBLOCK) :> MREGION where type t = B.t = struct
  type t = B.t
  datatype phan = Phan
  fun run () = let
    val (ret, res) = RMonad.get Phan (B.f(RMonad.ret(Phan, "RESOURCE"),
                                     (fn r => RMonad.ret(Phan, "RESOURCE") r)))
  in
    print("closing " ^ res ^ "\n") ; ret
  end
end

structure T = MRegion(struct
  type t = int
  fun f (return, toString) = let
    val >>= = RMonad.bnd
    infix >>=
  in
    return 6 >>= (fn(x, r) =>
      toString r >>= (fn(s, r) => (
        print ("received " ^ s ^ "\n");
        return (x + 1)
    )))
  end
end)

;T.run()

这很混乱，但它展示了我的基本想法。

资源发挥 STRef 的作用；如果它上面提供的所有操作都返回一个单调值而不是直接工作，那么它将建立一个延迟操作链，只有通过返回到 run 才能执行。这样可以抵消闭包保留代码块外部的 r 副本的能力，因为它们实际上永远不能执行操作链，无法返回到 run，因此无法以任何方式访问它。

两次调用 T.run 将重复使用相同的“key”类型，这意味着这不等同于嵌套的 forall，但如果没有办法在两个独立的调用之间共享 r，那就没有区别；而且确实没有-如果它不能被返回、不能在外部分配，并且任何闭包都无法运行处理它的代码。至少我是这么认为的。

- Alex Celeste