gpt4 book ai didi

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

转载 作者:行者123 更新时间:2023-12-04 12:47:41 25 4
gpt4 key购买 nike

runST是一个 Haskell 函数,它通过类型静态地限制资源的可用生命周期。为此,它使用 rank-2 多态性。标准 ML 更简单的类型系统仅提供 rank-1 多态性。

标准 ML 是否仍然可以使用类型将资源的生命周期限制为类似的最终结果?

This pagethis page演示一些将代码重组为只需要更简单类型的方法。如果我理解正确,核心是将表达式包装起来,以便将其替换为上下文中可能的观察结果,这些观察结果是有限的。这种技术通用吗?它或相关的编码是否可以与 runST 之类的东西一起使用(显然与签名不同) ,以防止观察到从包装表达式中转义的值的类型?如果是这样,怎么做?

我想象的场景是这样的:

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

...在哪里 magic...提供了用户提供的代码无法以任何方式共享的资源。显然,像这样带有单个库函数的简单接口(interface)是不可能的,但也许有不同的包装层、手动内联和提取......?

我看过 this ,但如果我理解正确(......很可能不是),那实际上并不能阻止对资源的所有引用被共享,只能确保对它的一个引用必须“关闭”。

基本上我想在 SML 中实现安全类型的显式(不是推断的 MLKit 样式)区域。

最佳答案

经过一番摸索后,我认为这是可能的——或者至少足够接近它可以工作——尽管看起来不是很漂亮。 (我可能在这里完全走错了路,有知识的人请评论。)

有可能(我认为)使用 SML 的生成数据类型和仿函数来创建不能在给定词法 block 之外引用的抽象幻像类型:

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或声明可以分配给它的外部可变变量,这可以解决大部分问题。但是它仍然可以通过在“区域” block 中创建的函数来关闭,并在其假定的关闭点之后保持这种方式;此类函数可能会被导出并再次使用悬空资源引用,从而导致问题。

我们可以模仿 ST但是,并防止闭包对 resource 做任何有用的事情通过强制该区域使用以幻像类型为键的 monad:

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的角色;如果所有提供的操作都返回一个单子(monad)值而不是直接工作,它将建立一个延迟操作链,只能通过返回到 run 来执行。 .这抵消了闭包保留 r 副本的能力。 block 之外,因为他们将永远无法真正执行操作链,无法返回 run ,因此无法以任何方式访问它。

调用 T.run两次将重复使用相同的“键”类型,这意味着这不等同于嵌套 forall ,但如果无法分享 r在两个单独的调用之间;没有 - 如果它不能被返回,不能被分配到外部,并且任何闭包都不能运行在它上面工作的代码。至少,我是这么认为的。

关于haskell - 在 SML 中编码 rank-2 多态性等价物,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/24135774/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com