如何理解Haskell的ST monad中的状态类型 [英] How to understand the state type in Haskell's 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 - >一个对于 runST 就没问题。重要的是，
不能有任何有关该州的具体价值（类型 s ）的假设，它被赋予
给功能。因此，全量化不应该超过国家类型，而应该超过
国家的具体价值。类型系统必须表明赋予 runST 的有状态
动作的结果与状态无关（但与其类型无关）。
因此，我的两个解释都是错误的。我真的试图理解这种类型的
结构的一切。有没有人可以向我解释？
PS。我已经阅读了线程
[ ST monad是如何工作的？但它没有帮助我。当
时，我用我的手做统一算法，我发现机制起作用，它是如何工作的（由
使用范围限制），但我真的很想理解它 - 不仅仅是看到它的工作原理。
解释很好，但我想知道它是如何映射到最终定义的
好的，让我们回到的方式，直到我们正在尝试做的事情，以及它与我们已经可以做的有什么不同。
功能状态线程
我们已经可以做功能状态。这是通过 State s monad完成的，其中 State sx :: * 与函数类型<$ c同构$ c> s - > （x，s）：以 s 作为输入的函数，返回一个包含 x 为monad，也是 s 类型的新状态。对于一些弱类型，我们甚至可以使用 Data.Map.Strict（Map）来处理这些值。例如，基本的JavaScript弱类型系统在历史上足以支持大多数通用计算，并且它看起来像（省略函数，它们也变成了对象，并且具有像词法关闭的模型）：
data JSVariable = Undefined |数字双| Str String |布尔布尔|空|
对象（Map String JSVariable）
有了这些，我们可以使用 State（Map String JSVariable） monad存储一个函数式命名空间，我们可以通过它来引用变量，将它们初始化为值并在状态线程中操作它们。然后我们有一个类型的函数：
$ b
runState :: State s x - > s - > （x，s）
我们可以填写并截断以获得：
fst。 flip runState Map.empty :: State（Map a b）x - > x
更一般的情况下，我们可以立刻将这个概括为 Map 是一个 Monoid 或其他。
ST 不同？
首先， ST 想要 mutate 一个底层的数据结构 - 上面没有改变Map，而是创建了一个传递到下一个线程的 new Map。因此，举例来说，如果我们在runST（readVar v）中编写相当于论文的 let v = runST（newVar True），我们在上面没有含糊性，因为不管你如何切片，您从等价于 newVar True 获得的数据结构只是状态的冻结时间快照，而不是完整的可变状态本身！在状态s monad中没有可变状态。
为了维护不同名称空间状态的外观（而不是某种全局状态），我们保留 ST s monad的概念，但现在我们不允许您直接访问 取值。这意味着 s 被称为幻影类型：它不代表 你只会得到类型 s 的唯一值是 undefined :: s ，即使如此，只有当你有意识地选择成功。
因为我们从不会给你一个类型 s 的值，所以你没有任何意义曾经有过用它做任何事情的功能;对你来说，它总是是一个类型变量，由潜在的管道填充。 （让我们不要深入探讨管道的作用）。
其次， ST 因此允许更大范围的类型安全性比上述弱类型系统！现在我们可以有每个 newVar :: x - > ST s（MutVar s x）返回此类型的封装引用 MutVar s x 。这个引用包含一个指向它所处状态的指针，所以它在任何其他上下文中都不会有意义 - 它也有它自己独特的类型 x ，所以它已经可以容纳任何类型，并且可以进行严格的类型检查。
现在有龙
我们已经开始使用我们想要实现的一般想法：我们希望能够定义类型 ST sx 的线程，其中 s 通常保留为一个类型变量，但是 x 是一个我们感兴趣计算的值，然后最终我们应该能够将它们插入一个如下所示的函数中：
$ b
runST'::∀s一个。 （ST s a） - > a
这个想法有味道，因为它（a）类似于 State monad，并且（b）你应该能够获取 ST sa ，为它创建一个空白状态，然后运行计算来返回一个纯函数 a 。
但是...有一个问题。问题是，在这篇论文中，我们有几个函数，比如 newVar :: x - > ST s（MutVar s x），它将内部线程状态类型 s 复制到此monad的输出空间中。即使我们没有得到 s 类型的值，我们仍然得到类型变量 s ，你会记得它是某种可变状态的通用命名空间。其他函数如 readVar :: MutVar s x - >然后，ST s x 将允许您创建其他状态线程，这些线程依赖于此特定的可变状态。
这就是关键词：特定。 newVar :: x - >的类型ST s（MutVar sx）包含一个非特定或常规 s 对于任何 s 。但是如果你 runST（newVar True），你会得到一个 MutVar s Bool s ，这是计算中使用的那个。我们希望确保 runST 只占用常规 s 的而不是特定的。
换句话说， 所以这篇论文的基本问题是：我们如何重新定义 newVar 的类型为 x - > forall s。 ST s（MutVar sx）（请参阅 forall ，它强制变量仍然空闲），而 readVar 的类型为 MutVar sx - > ST sx （no forall - 本身或者来自另一个特定的 MutVar ）计算，它有一个特定的 s ）。如果每个 readVar 我们还包含 newVar，那么，以获得 s 生成传递给 readVar 的对象的
ST 以确保状态不是特定的吗？ newVar True 甚至是出自 newVar True>> = readVar 可以在输入 runST 时检查。
他们的回答是，我们添加Haskell的语法，并说这个类型变量必须仍然是一个自由类型变量！这是通过编写 runST :: forall x来完成的。 （全部ST s x） - > X 。请注意， forall s。现在包含在函数参数中，用于表示嘿，这个参数必须是一个通用的自由类型参数这个表达式。
这阻止了类型检查中的并行线程垃圾，因此使整个系统正确。
Jones and Launchbury described in their paper "Lazy Functional State Threads" the ST monad. To ensure that mutable variables can't be used outside the context (or "thread") they have been created in, they use special types, including one of higher rank. Here four important examples:
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
In order to get the idea behind that construction I read the first two sections of the paper. The following explanation seems to be central:
Now, what we really want to say is that
newSTshould only be applied to a state transformer which usesnewVarto create any references which are used in that thread. To put it another way, the argument ofrunSTshould not make any assumptions about what has already been allocated in the initial state. That is,runSTshould work regardless of what initial state it is given. So the type ofrunSTshould be:runST :: ∀ a. (∀ s. ST s a) -> a
The explanation is fine, but I wonder how it maps to the final definition of the required type. My
problem is that I don't know how to interpret the type variable s. As stated in Section 1, a state
is essentially a mapping from variables to values. But what is a state type s? In what can a state
type s differ from another one t? For me there are two possibilities:
(1) The type s can be seen as the concrete type for a mapping of variables such as lists, arrays
and sequences can be seen as concrete types for sequential collections. (I intentionally avoid here
the words "class" and "implementation" as there is no class restriction on the type of s.)
(2) The type s can be seen as a concrete value, i.e. a concrete state, i.e. a concrete mapping of
variables.
Interpretation (2) maps nicely to Jones' and Launchbury's explanation of the type of runST. The
all-quantification expresses the independence of the actual state (which is fully described by the
state type). The flaw in this interpretation is however the type of writeVar. As it clearly
modifies the state, it should be of type ∀ s a. MutVar s a -> a -> ST t (). So this
interpretation must be false.
Interpretation (1) however is not really better because it doesn't map to Jones' and Launchbury's
explanation. The type ∀ s a. ST s a -> a for runST would be fine. The important thing is that
there mustn't be any assumption about the concrete value of the state (of type s) which is given
to the function. Hence the all-quantification shouldn't be over the state type but (instead) over
the concrete value of the state. The type system must express that the result of the stateful
action, which is given to runST, is independent of the state (but not independent of its type).
Hence both of my interpretations are false. I really tried to understand everything of this type construction. Is there someone who can explain that to me?
PS. I have already read the thread [How does the ST monad work? but it didn't help me. When I do the unification algorithm with my hand I see, that the mechanism works and how it works (by using the limits of scopes) but I really want to understand it – not just see that it works.
The explanation is fine, but I wonder how it maps to the final definition of the required type.
Okay, so let's back way up to what we're trying to do, and how it differs from what we can already do.
Functional state threading
We can already do functional state. This is done with the State s monad, where State s x :: * is isomorphic to the function type s -> (x, s): functions which take s as an input and return a pair containing both some value of type x for the monad and also a new state of type s. With some weak typing we could even just use a Data.Map.Strict(Map) to handle these values. For example the basic JavaScript weakly typed system has historically been enough to enable most general computation and it looks something like (omitting functions, which turn out to also be objects and have things like lexical closures to model):
data JSVariable = Undefined | Number Double | Str String | Boolean Bool | Null |
Object (Map String JSVariable)
With these we might use the State (Map String JSVariable) monad to store a functional namespace by which we can refer to variables, initialize them to values, and manipulate them in a state thread. And then we have a function of type
runState :: State s x -> s -> (x, s)
which we can fill in and also truncate to get:
fst . flip runState Map.empty :: State (Map a b) x -> x
More generally we might immediately be able to generalize this to make the Map be a Monoid or something.
How is ST different?
First off, ST wants to mutate an underlying data structure -- the above did not mutate the Map, but created a new Map which got passed on to the next thread. So for example if we write the equivalent of the paper's let v = runST (newVar True) in runST (readVar v) we have no ambiguity above because no matter how you slice it, the data structure that you get from the equivalent of newVar True is only a frozen-in-time snapshot of the state, not the full mutable state itself! There is no mutable state in the State s monad.
In order to maintain the facade of a distinct namespaced state (rather than some sort of global state) we keep the notion of an ST s monad, but now we do not give you direct access to that s. This means that s is something called a phantom type: it does not represent anything concrete that you can hold onto, the only value you will ever get of type s is undefined :: s, and even then, only if you consciously choose to make it.
Since we never will give you a value of type s there is no point to you ever having functions which do anything with it; for you, it will always be a type variable to be filled in by the underlying plumbing. (Let's not get into what exactly the plumbing does.)
Second, ST therefore allows a much greater range of type safety than the above weakly-typed system! We can now have each newVar :: x -> ST s (MutVar s x) return an encapsulated reference of this type MutVar s x. This reference contains a pointer to the state that it lives in, so it will never make sense in any other context -- and it also has its own distinct type x, so it can already hold any type, and it can be rigorously type-checked.
Now there be dragons
So we've started with the general idea of what we want to achieve: we want to be able to define threads of type ST s x, where s is in general left as a type variable but x is a value that we are interested in computing, and then eventually we should be able to plug them into a function which looks like:
runST' :: ∀ s a. (ST s a) -> a
This idea "smells right" because it (a) is analogous to something similar in the State s monad, and (b) you should be able to take an ST s a, cook up a blank state for it, and then run the computation to return a purely functional a.
But... there is a problem. The problem is that at this point in the paper we have several functions like newVar :: x -> ST s (MutVar s x) which copy the internal threaded state type s into the "output" space of this monad. Even though we do not get a value of type s we still get the type variable s, which as you'll recall is some sort of general namespace for some chunk of mutable state. Other functions like readVar :: MutVar s x -> ST s x will then let you create other state threads which depend on this specific mutable state.
So that's the key word: specific. The type of newVar :: x -> ST s (MutVar s x) contains a nonspecific or general s, it will work for any s. But if you runST (newVar True) you get a MutVar s Bool for some specific s, the one that was used in the computation. We want to make sure that runST only takes general s's and not specific ones.
Put another way, newVar has type x -> forall s. ST s (MutVar s x) (see the forall that forces the variable to still be free?) while readVar has type MutVar s x -> ST s x (no forall -- by itself, or with a specific MutVar from another computation, this has a specific s to it). The s only transitions from being specific to general if for every readVar we also include the newVar that generated the object passed to readVar, to get that forall s that keeps the term general!
So the paper's essential problem is: how do we redefine ST to make sure that the state is not specific? It has to be the case that what comes out of readVar cannot be fed to runST but what comes out of newVar True and even what comes out of newVar True >>= readVar can both typecheck when fed to runST.
And their answer is, we add to the syntax of Haskell, saying "this type variable must still be a free type variable!" This is done by writing runST :: forall x. (forall s. ST s x) -> x. Notice that the forall s. is now contained within the function argument to say "hey, this parameter has to be a general, free type parameter in this expression."
This blocks the parallel-thread crap from type-checking and therefore makes the whole system correct.
这篇关于如何理解Haskell的ST monad中的状态类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
