Jones和Launchbury在他们的论文 "Lazy Functional State Threads"中描述了ST monad.为了确保可变参数不能在它们创建的上下文(或"线程")之外使用,它们使用特殊类型,包括更高级别的类型.这有四个重要的例子:
newVar :: ? s a. a -> ST s (MutVar s a) readVar :: ? s a. MutVar s a -> ST s a writeVar :: ? s a. MutVar s a -> a -> ST s () runST :: ? a. (? s. ST s a) -> a
为了理解这种结构背后的想法,我阅读了论文的前两部分.以下解释似乎是核心:
现在,我们真正想说的是,
newST应该只应用于一个状态转换器,它newVar用于创建在该线程中使用的任何引用.换句话说,runST不应该对初始状态下已分配的内容做出任何假设.也就是说,runST不管它给出的初始状态如何都应该工作.所以类型runST应该是:runST :: ? a. (? s. ST s a) -> a
解释很好,但我想知道它如何映射到所需类型的最终定义.我的问题是我不知道如何解释类型变量s.如第1节所述,状态本质上是从变量到值的映射.但什么是州的类型s？州的类型s与另一种州有何不同t？对我来说有两种可能性:
(1)类型s可以看作是变量映射的具体类型,如列表,数组和序列可以看作是顺序集合的具体类型.(我故意避免使用"class"和"implementation"这两个词,因为对类型没有类限制s.)
(2)类型s可以看作具体值,即具体状态,即变量的具体映射.
解释(2)很好地映射了Jones'和Launchbury对其类型的解释runST.全量化表示实际状态的独立性(由状态类型完全描述).然而,这种解释的缺陷是类型writeVar.因为它明确地修改了状态,所以它应该是类型的? s a. MutVar s a -> a -> ST t ().所以这种解释必定是错误的.
然而,解释(1)并不是更好,因为它没有映射到Jones'和Launchbury的解释.该类型? s a. ST s a -> a的runST就可以了.重要的是,不应该对s赋予函数的状态(类型)的具体值有任何假设.因此,全量化不应该超过状态类型,而应该(而不是)超过状态的具体值.类型系统必须表明有状态操作的结果与状态runST无关(但不独立于其类型).
因此,我的两种解释都是错误的.我真的试着理解这种类型结构的一切.有人可以向我解释一下吗？
PS.我已经阅读了帖子[ ST monad是如何工作的？但它没有帮助我.当我用我的手做统一算法时,我看到,机制是有效的,它是如何工作的(通过使用范围的限制),但我真的想要了解它 - 而不仅仅是看它是否有效.
解释很好,但我想知道它如何映射到所需类型的最终定义.
好吧,让我们回到方式到什么我们正在试图做的,以及如何它不同于我们已经可以做到.
功能状态线程我们已经可以做功能状态.这是通过State smonad 来完成的,其中State s x :: *函数类型与函数类型是同构的s -> (x, s):函数s作为输入并返回一对包含xmonad的某个类型值以及新类型的类型s.通过一些弱类型,我们甚至可以使用a Data.Map.Strict(Map)来处理这些值.例如,基本的JavaScript弱类型系统在历史上足以支持大多数通用计算,它看起来像(省略函数,结果也是对象,并且具有类似词法闭包的模型):
data JSVariable = Undefined | Number Double | Str String | Boolean Bool | Null |
Object (Map String JSVariable)
有了这些,我们可以使用State (Map String JSVariable)monad来存储一个函数名称空间,通过它可以引用变量,将它们初始化为值,并在状态线程中对它们进行操作.然后我们有一个类型的功能
runState :: State s x -> s -> (x, s)
我们可以填写并截断得到:
fst . flip runState Map.empty :: State (Map a b) x -> x
更一般地说,我们可能会立即将其概括Map为一个Monoid或多个东西.
ST不同？首先,ST想要改变底层数据结构 - 上面没有改变 Map,但创建了一个新的 Map,它被传递给下一个线程.因此,例如,如果我们写相同的论文,let v = runST (newVar True) in runST (readVar v)我们上面没有歧义,因为无论你如何切片,你从等价物中获得的数据结构newVar True只是状态的冻结快照,而不是完整的可变状态本身!State smonad中没有可变状态.
为了维护一个独特的命名空间状态(而不是某种全局状态)的外观,我们保留了ST smonad 的概念,但现在我们不会让你直接访问它s.这意味着它s被称为幻象类型:它不代表任何你能抓住的具体内容,你将获得的唯一价值s是undefined :: s,即便如此,只有你有意识地选择制作它.
因为我们永远不会给你一个类型的价值,s所以没有任何意义,你有任何与它有关的功能; 对于你来说,它总是一个由底层管道填充的类型变量.(我们不要深入了解管道的功能.)
其次,ST因此比上述弱型系统具有更大范围的类型安全性!我们现在可以让每个newVar :: x -> ST s (MutVar s x)返回这种类型的封装引用MutVar s x.这个引用包含一个指向它所处的状态的指针,所以它在任何其他上下文中都没有意义 - 它也有自己独特的类型x,因此它可以保存任何类型,并且可以严格地进行类型检查.
因此,我们已经开始与一般的想法,我们要达到什么样的:我们希望能够定义类型的线ST s x,其中s在一般留下作为一个类型变量,但是x是一个值,我们感兴趣的是计算,然后最终我们应该能够将它们插入一个看起来像这样的函数:
runST' :: ? s a. (ST s a) -> a
这个想法"闻起来很正确",因为它(a)类似于State smonad中类似的东西,并且(b)你应该能够ST s a为它做一个空白状态,然后运行计算以返回纯粹的功能a.
但是......有一个问题.问题是,在本文的这一点上,我们有几个函数,比如newVar :: x -> ST s (MutVar s x)将内部线程状态类型复制s到这个monad的"输出"空间.即使我们没有得到类型 的值,s我们仍然得到类型变量 s,你会记得它是某种可变状态块的某种通用命名空间.其他函数readVar :: MutVar s x -> ST s x将允许您创建依赖于此特定可变状态的其他状态线程.
所以这是关键词:具体.newVar :: x -> ST s (MutVar s x)包含非特定或一般 的类型s,它适用于任何s.但是,如果你runST (newVar True)得到MutVar s Bool一些特定的 s,计算中使用的那个.我们希望确保runST只采用一般 s而非特定的.
换句话说,newVar有类型x -> forall s. ST s (MutVar s x)(请参阅forall强制变量仍然是空闲的？)虽然readVar有类型MutVar s x -> ST s x(没有forall- 本身,或者具有MutVar来自另一个计算的特定s,它具有特定的类型).在s被特殊到一般只有转变,若对所有readVar我们还包括newVar生成传递给对象readVar,以获取forall s,保持术语一般!
因此,论文的基本问题是:我们如何重新定义ST以确保状态不具体？必须出现这样的情况,即出来的东西readVar 不能被喂食,runST但是什么出来,newVar True甚至出来的东西都newVar True >>= readVar可以在喂食时进行类型检查runST.
他们的回答是,我们添加了Haskell的语法,说"这个类型变量必须仍然是一个自由类型变量!" 这是通过写作完成的runST :: forall x. (forall s. ST s x) -> x.请注意,forall s.现在包含在函数参数中,表示"嘿,此参数必须是此表达式中的常规自由类型参数".
这会阻止类型检查的并行线程垃圾,从而使整个系统正确.
我会避免解释s任何具体的东西.它基本上只是一个"唯一标识符",它确保两个不同ST计算中的状态不会混淆.特别是,因为参数runST是一个(rank-2)多态行为,你可以以某种方式走私出这个monadic动作的任何状态引用必然是一个存在类型,而且对于一个不受约束的存在主义基本上没什么可以做的.因此,不可能例如在状态monad中引用不再存在的值.
如果您希望将s具体内容视为具体内容,请将其视为可以分配,修改和删除有状态值的世界类型.
该设置中的类型说明:
newVar :: ? s a. a -> ST s (MutVar s a):在任何世界上s,我都可以将类型的值a抛到地面,因此它可以通过MutVar引用进行修改(当然,仅在同一个世界中 - 尽管这个世界的状态因此而改变,但它的类型/身份不).
readVar :: ? s a. MutVar s a -> ST s a:如果可变引用和我一样存在于同一个世界中,我可以查看该对象并给出一个副本作为monadic结果.
writeVar :: ? s a. MutVar s a -> a -> ST s ():如果可变参考与我一样生活在同一个世界中,我就能够破坏坐在那里的物体并用其他东西代替它.
runST :: ? a. (? s. ST s a) -> a:给定一个适用于任何世界的动作,我能够选择一些没人知道的隐藏星球.然后,该行动可以将各种变异的暴行应用于景观并仅将结果带回来.因为没有人知道这个星球,我们仍然拥有一个宇宙,对于所有人都能看到的宇宙,它没有受到损害并且纯粹是功能性的,但你确实得到了破坏性计算的结果.
京公网安备 11010802040832号 | 京ICP备19059560号-6 