如何理解 Haskell 的 ST monad 中的状态类型
How to understand the state type in Haskell's ST monad
Jones 和 Launchbury 在他们的 paper "Lazy Functional State Threads" 中描述了 ST monad。到
确保可变变量不能在它们创建的上下文（或"thread"）之外使用
在，他们使用特殊类型，包括更高级别的一种。这里有四个重要的例子：
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
为了了解该构造背后的想法，我阅读了论文的前两部分。这
以下解释似乎很重要：
Now, what we really want to say is that newST should only be applied to a state transformer which uses newVar to create any references which are used in that thread. To put it another way, the argument of runST should not make any assumptions about what has already been allocated in the initial state. That is, runST should work regardless of what initial state it is given. So the type of runST should be: runST :: ∀ a. (∀ s. ST s a) -> a
解释的很好，但我想知道它是如何映射到所需类型的最终定义的。我的
问题是我不知道如何解释类型变量s。如第 1 节所述，状态
本质上是从变量到值的映射。但是什么是状态类型s？在什么状态下可以
类型 s 与另一个类型 t 不同？对我来说有两种可能性：
(1) 类型s可以看作是变量映射的具体类型，如列表、数组
和序列可以看作是顺序集合的具体类型。 （我故意避开这里
单词 "class" 和 "implementation" 因为 s 的类型没有 class 限制。）
(2) 类型s可以看做一个具体的值，即具体的状态，即具体的映射
变量。
解释 (2) 很好地映射到 Jones 和 Launchbury 对 runST 类型的解释。这
all-quantification 表示实际状态的独立性（由
状态类型）。然而，这种解释的缺陷在于 writeVar 的类型。因为它清楚
修改状态，它应该是 ∀ s a. MutVar s a -> a -> ST t () 类型。所以这
解释一定是错误的。
然而，解释 (1) 并不是真的更好，因为它没有映射到 Jones 和 Launchbury 的
解释。 runST 的类型 ∀ s a. ST s a -> a 就可以了。重要的是
不能对给定的状态（s 类型）的具体值有任何假设
到功能。因此，全量化不应该超过状态类型，而是（相反）超过
国家的具体价值。类型系统必须表达有状态的结果
给予 runST 的动作独立于状态（但不独立于其类型）。
因此我的两种解释都是错误的。我真的试图理解这种类型的一切
建造。有人可以向我解释一下吗？
PS。我已经阅读了线程
[How does the ST monad work? 但它对我没有帮助。什么时候
我用我的手做了统一算法，我看到，该机制是有效的，它是如何工作的（通过
使用范围的限制），但我真的很想理解它——而不仅仅是看到它有效。
我会避免将 s 解释为任何具体的东西。它基本上只是一个“唯一标识符”，可确保两个不同 ST 计算中的状态不会混淆。特别是，因为 runST 的参数是一个（rank-2）多态动作，所以你可以以某种方式从这个 monadic 动作中走私出来的任何状态引用都必然是一个存在类型，基本上你无能为力不受约束的存在。所以不可能例如引用状态 monad 中实际上不再存在的值。
如果您想将 s 视为具体的东西，请将其视为 world 的类型，其中可以分配、修改和删除有状态的值。
该设置中的类型说明：
newVar :: ∀ s a. a -> ST s (MutVar s a)：在任何世界 s 上，我都可以将 a 类型的值扔到地上，这样它就可以通过 MutVar 引用（当然，仅在同一个世界中——虽然这个世界的 state 会因此改变，但它的类型/身份不会）。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：给定一个适用于任何世界的动作，我能够 select 一些无人知晓的隐藏星球。然后，该行动可能会将各种变异的暴行应用于景观，并只带来结果。因为没有人知道这个星球，所以我们仍然有一个宇宙，在每个人都可以看到的情况下，它毫发无损，纯粹是功能性的，但你确实得到了破坏性计算的结果。
The explanation is fine, but I wonder how it maps to the final definition of the required type.
好的，让我们回到方式我们正在尝试做的事情，以及它与我们已经可以做的事情有何不同。
功能状态线程
我们可以已经做到了功能状态。这是通过 State s monad 完成的，其中 State s x :: * 与函数类型 s -> (x, s) 同构：将 s 作为输入的函数和 return 一对包含monad 的 x 类型值和 s 类型的新状态。通过一些弱类型，我们甚至可以只使用 Data.Map.Strict(Map) 来处理这些值。例如，基本的 JavaScript 弱类型系统在历史上已经足以支持大多数通用计算，它看起来像（省略函数，结果也是对象，并且具有诸如词法闭包之类的模型）：
data JSVariable = Undefined | Number Double | Str String | Boolean Bool | Null |
Object (Map String JSVariable)
有了这些，我们可以使用 State (Map String JSVariable) monad 来存储函数名称space，通过它我们可以引用变量，将它们初始化为值，并在状态线程中操作它们。然后我们有一个函数类型
runState :: State s x -> s -> (x, s)
我们可以填写，也可以t运行得到：
fst . flip runState Map.empty :: State (Map a b) x -> x
更一般地说，我们可能会立即概括这一点，使 Map 成为 Monoid 或其他东西。
ST 有何不同？
首先，ST想要改变一个底层数据结构——上面没有改变地图，但是创建了一个 new 映射，它被传递到下一个线程。因此，例如，如果我们写相当于论文的 let v = runST (newVar True) in runST (readVar v) 我们上面没有歧义，因为无论你如何切片，你从相当于 newVar True 得到的数据结构只是一个 frozen-in-time 状态快照，而不是完整的可变状态本身！ State s monad 中没有可变状态。
为了维护一个独特的名称spaced 状态（而不是某种全局状态）的外观，我们保留了 ST s monad 的概念，但现在我们 不让您直接访问那个s。这意味着 s 是一种叫做 幻影类型 的东西：它不代表 任何东西 你可以坚持的具体事物，唯一的价值你将永远得到类型 s 是 undefined :: s，即使那样，只有你有意识地选择去做它。
因为我们永远不会给你一个 s 类型的值，所以你没有必要使用它做任何事情的函数；对你来说，它将总是 是一个由底层管道填充的类型变量。 （让我们不要深入了解管道的具体作用。）
其次，ST 因此允许比上述 weakly-typed 系统更大范围的类型安全！我们现在可以让每个 newVar :: x -> ST s (MutVar s x) return 都有一个这种类型 MutVar s x 的封装引用。这个引用包含一个指向它所在状态的指针，所以它在任何其他上下文中都没有意义——它也有自己独特的类型 x，所以它已经可以容纳任何类型，并且它可以严格 type-checked.
现在有龙了
所以我们从 我们想要实现的总体想法 开始：我们希望能够定义 ST s x 类型的线程，其中 s 通常保留为类型变量，但 x 是我们有兴趣计算的值，然后最终我们应该能够将它们插入一个函数，如下所示：
runST' :: ∀ s a. (ST s a) -> a
这个想法 "smells right" 因为它 (a) 类似于 State s monad 中的类似东西，并且 (b) 你应该能够采用 ST s a，做饭它的空白状态，然后 运行 计算到 return 一个纯函数 a.
但是...有一个问题。问题是，在本文的这一点上，我们有几个函数，如 newVar :: x -> ST s (MutVar s x)，它们将内部线程状态类型 s 复制到此 monad 的 "output" space 中。即使我们没有得到 类型 s 的值，我们仍然得到 类型变量 s，就像你我会记得是一些可变状态块的通用名称space。 readVar :: MutVar s x -> ST s x 等其他函数将允许您创建依赖于此特定可变状态的其他状态线程。
这就是关键词：具体。 newVar :: x -> ST s (MutVar s x) 的类型包含 nonspecific 或 general s，它将适用于任何 s。但是如果你 runST (newVar True) 你会得到一个 MutVar s Bool 对于一些 specific s，在计算中使用的那个。我们要确保 runST 只接受 general s 而不是 specific。
换句话说，newVar 的类型为 x -> forall s. ST s (MutVar s x)（请参阅强制变量仍然可用的 forall？）而 readVar 的类型为 MutVar s x -> ST s x（没有 forall -- 本身，或来自另一个计算的特定 MutVar，它有一个特定的 s）。如果对于每个 readVar 我们还包括生成传递给 readVar 的对象的 newVar，则 s 仅从特定过渡到一般，以获得 forall s这使术语保持通用！
所以这篇论文的本质问题是：我们如何重新定义ST以确保状态不是特定的？必须是这样的来自 readVar 不能 被馈送到 runST 但来自 newVar True 甚至来自 newVar True >>= readVar 的东西都可以进行类型检查当喂给 runST.
他们的回答是，我们添加到Haskell的语法中，说"this type variable must still be a free type variable!"这是通过写runST :: forall x. (forall s. ST s x) -> x来完成的。请注意 forall s. 现在包含在函数参数 中 表示 "hey, this parameter has to be a general, free type parameter in this expression."
这阻止了来自 type-checking 的 parallel-thread 废话，因此使整个系统正确。
Jones 和 Launchbury 在他们的 paper "Lazy Functional State Threads" 中描述了 ST monad。到 确保可变变量不能在它们创建的上下文（或"thread"）之外使用 在，他们使用特殊类型，包括更高级别的一种。这里有四个重要的例子：
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
为了了解该构造背后的想法，我阅读了论文的前两部分。这 以下解释似乎很重要：
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
解释的很好，但我想知道它是如何映射到所需类型的最终定义的。我的
问题是我不知道如何解释类型变量s。如第 1 节所述，状态
本质上是从变量到值的映射。但是什么是状态类型s？在什么状态下可以
类型 s 与另一个类型 t 不同？对我来说有两种可能性：
(1) 类型s可以看作是变量映射的具体类型，如列表、数组
和序列可以看作是顺序集合的具体类型。 （我故意避开这里
单词 "class" 和 "implementation" 因为 s 的类型没有 class 限制。）
(2) 类型s可以看做一个具体的值，即具体的状态，即具体的映射
变量。
解释 (2) 很好地映射到 Jones 和 Launchbury 对 runST 类型的解释。这
all-quantification 表示实际状态的独立性（由
状态类型）。然而，这种解释的缺陷在于 writeVar 的类型。因为它清楚
修改状态，它应该是 ∀ s a. MutVar s a -> a -> ST t () 类型。所以这
解释一定是错误的。
然而，解释 (1) 并不是真的更好，因为它没有映射到 Jones 和 Launchbury 的
解释。 runST 的类型 ∀ s a. ST s a -> a 就可以了。重要的是
不能对给定的状态（s 类型）的具体值有任何假设
到功能。因此，全量化不应该超过状态类型，而是（相反）超过
国家的具体价值。类型系统必须表达有状态的结果
给予 runST 的动作独立于状态（但不独立于其类型）。
因此我的两种解释都是错误的。我真的试图理解这种类型的一切 建造。有人可以向我解释一下吗？
PS。我已经阅读了线程 [How does the ST monad work? 但它对我没有帮助。什么时候 我用我的手做了统一算法，我看到，该机制是有效的，它是如何工作的（通过 使用范围的限制），但我真的很想理解它——而不仅仅是看到它有效。
我会避免将 s 解释为任何具体的东西。它基本上只是一个“唯一标识符”，可确保两个不同 ST 计算中的状态不会混淆。特别是，因为 runST 的参数是一个（rank-2）多态动作，所以你可以以某种方式从这个 monadic 动作中走私出来的任何状态引用都必然是一个存在类型，基本上你无能为力不受约束的存在。所以不可能例如引用状态 monad 中实际上不再存在的值。
如果您想将 s 视为具体的东西，请将其视为 world 的类型，其中可以分配、修改和删除有状态的值。
该设置中的类型说明：
newVar :: ∀ s a. a -> ST s (MutVar s a)：在任何世界s上，我都可以将a类型的值扔到地上，这样它就可以通过MutVar引用（当然，仅在同一个世界中——虽然这个世界的 state 会因此改变，但它的类型/身份不会）。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：给定一个适用于任何世界的动作，我能够 select 一些无人知晓的隐藏星球。然后，该行动可能会将各种变异的暴行应用于景观，并只带来结果。因为没有人知道这个星球，所以我们仍然有一个宇宙，在每个人都可以看到的情况下，它毫发无损，纯粹是功能性的，但你确实得到了破坏性计算的结果。
The explanation is fine, but I wonder how it maps to the final definition of the required type.
好的，让我们回到方式我们正在尝试做的事情，以及它与我们已经可以做的事情有何不同。
功能状态线程
我们可以已经做到了功能状态。这是通过 State s monad 完成的，其中 State s x :: * 与函数类型 s -> (x, s) 同构：将 s 作为输入的函数和 return 一对包含monad 的 x 类型值和 s 类型的新状态。通过一些弱类型，我们甚至可以只使用 Data.Map.Strict(Map) 来处理这些值。例如，基本的 JavaScript 弱类型系统在历史上已经足以支持大多数通用计算，它看起来像（省略函数，结果也是对象，并且具有诸如词法闭包之类的模型）：
data JSVariable = Undefined | Number Double | Str String | Boolean Bool | Null |
Object (Map String JSVariable)
有了这些，我们可以使用 State (Map String JSVariable) monad 来存储函数名称space，通过它我们可以引用变量，将它们初始化为值，并在状态线程中操作它们。然后我们有一个函数类型
runState :: State s x -> s -> (x, s)
我们可以填写，也可以t运行得到：
fst . flip runState Map.empty :: State (Map a b) x -> x
更一般地说，我们可能会立即概括这一点，使 Map 成为 Monoid 或其他东西。
ST 有何不同？
首先，ST想要改变一个底层数据结构——上面没有改变地图，但是创建了一个 new 映射，它被传递到下一个线程。因此，例如，如果我们写相当于论文的 let v = runST (newVar True) in runST (readVar v) 我们上面没有歧义，因为无论你如何切片，你从相当于 newVar True 得到的数据结构只是一个 frozen-in-time 状态快照，而不是完整的可变状态本身！ State s monad 中没有可变状态。
为了维护一个独特的名称spaced 状态（而不是某种全局状态）的外观，我们保留了 ST s monad 的概念，但现在我们 不让您直接访问那个s。这意味着 s 是一种叫做 幻影类型 的东西：它不代表 任何东西 你可以坚持的具体事物，唯一的价值你将永远得到类型 s 是 undefined :: s，即使那样，只有你有意识地选择去做它。
因为我们永远不会给你一个 s 类型的值，所以你没有必要使用它做任何事情的函数；对你来说，它将总是 是一个由底层管道填充的类型变量。 （让我们不要深入了解管道的具体作用。）
其次，ST 因此允许比上述 weakly-typed 系统更大范围的类型安全！我们现在可以让每个 newVar :: x -> ST s (MutVar s x) return 都有一个这种类型 MutVar s x 的封装引用。这个引用包含一个指向它所在状态的指针，所以它在任何其他上下文中都没有意义——它也有自己独特的类型 x，所以它已经可以容纳任何类型，并且它可以严格 type-checked.
现在有龙了
所以我们从 我们想要实现的总体想法 开始：我们希望能够定义 ST s x 类型的线程，其中 s 通常保留为类型变量，但 x 是我们有兴趣计算的值，然后最终我们应该能够将它们插入一个函数，如下所示：
runST' :: ∀ s a. (ST s a) -> a
这个想法 "smells right" 因为它 (a) 类似于 State s monad 中的类似东西，并且 (b) 你应该能够采用 ST s a，做饭它的空白状态，然后 运行 计算到 return 一个纯函数 a.
但是...有一个问题。问题是，在本文的这一点上，我们有几个函数，如 newVar :: x -> ST s (MutVar s x)，它们将内部线程状态类型 s 复制到此 monad 的 "output" space 中。即使我们没有得到 类型 s 的值，我们仍然得到 类型变量 s，就像你我会记得是一些可变状态块的通用名称space。 readVar :: MutVar s x -> ST s x 等其他函数将允许您创建依赖于此特定可变状态的其他状态线程。
这就是关键词：具体。 newVar :: x -> ST s (MutVar s x) 的类型包含 nonspecific 或 general s，它将适用于任何 s。但是如果你 runST (newVar True) 你会得到一个 MutVar s Bool 对于一些 specific s，在计算中使用的那个。我们要确保 runST 只接受 general s 而不是 specific。
换句话说，newVar 的类型为 x -> forall s. ST s (MutVar s x)（请参阅强制变量仍然可用的 forall？）而 readVar 的类型为 MutVar s x -> ST s x（没有 forall -- 本身，或来自另一个计算的特定 MutVar，它有一个特定的 s）。如果对于每个 readVar 我们还包括生成传递给 readVar 的对象的 newVar，则 s 仅从特定过渡到一般，以获得 forall s这使术语保持通用！
所以这篇论文的本质问题是：我们如何重新定义ST以确保状态不是特定的？必须是这样的来自 readVar 不能 被馈送到 runST 但来自 newVar True 甚至来自 newVar True >>= readVar 的东西都可以进行类型检查当喂给 runST.
他们的回答是，我们添加到Haskell的语法中，说"this type variable must still be a free type variable!"这是通过写runST :: forall x. (forall s. ST s x) -> x来完成的。请注意 forall s. 现在包含在函数参数 中 表示 "hey, this parameter has to be a general, free type parameter in this expression."
这阻止了来自 type-checking 的 parallel-thread 废话，因此使整个系统正确。