`State#` 的规范

Posted 2023-02-16

【中文标题】`State#` 的规范

【英文标题】：Specification of `State#`

【发布时间】：2018-08-31 13:42:46

【问题描述】：

但是，documentation for STT 说：

这个 monad 转换器不应该与可以包含多个答案的 monad 一起使用，比如 list monad。原因是状态令牌将在不同的答案中重复，这会导致坏事发生（例如失去参考透明度）。安全单子包括单子 State、Reader、Writer、Maybe 及其对应的单子转换器的组合。

我希望能够自己判断STT monad 的某种使用是否安全。特别是，我想了解与 List monad 的交互。我知道STT sloc (ListT (ST sglob)) a 是unsafe，但是STT sloc [] 呢？

我发现（至少在 GHC 中），STT 最终是使用 MuteVar#、State#、realWorld# 等神奇结构实现的。是否有任何关于这些对象如何表现的准确文档？

这与earlier question of mine密切相关。

【问题讨论】：

我想你可以在不了解State#的情况下判断STT的某种使用是否安全。具体来说：State# 是否使用了affinely？然后就安全了。否则，不安全。您无需了解State# 的内部实现细节即可做出此决定。

然而realWorld# :: State# RealWorld 肯定不会被仿射使用：每次有人调用runST 时都会使用它。 （我不打算仿射使用State#，并且想了解如果我不这样做会发生什么。）

@dremodaris 你会分叉一堆平行宇宙。

这正是我想要的！他们每个人都会有自己的状态副本，还是他们会共同破坏一个共同的状态？为了清楚起见，我打算使用STT s [] monad。

@dremodaris 他们将共同破坏一个共同的状态。 ST 的重点是使用类型系统来保证使用可变状态的计算是自包含的，因此从周围上下文的角度来看，它可以被视为纯粹的。把它想象成“类型安全，受限IO”，仅此而已。 “状态令牌”不包括任何实际状态，它只是IO 和ST 用于确保排序的内部实现细节。正如文档所述，您不能安全地使用STT s []。如果你想能够分叉状态，你需要使用StateT。

【参考方案1】：

您真的不需要了解State# 是如何实现的。您只需将其视为通过计算线程传递的令牌，以确保 ST 操作的特定执行顺序，否则这些操作可能会被优化掉。

在STT s [] monad 中，您可以将列表操作视为生成可能的计算树，最终答案位于叶子节点。在每个分支点，State# 标记被拆分。所以，粗略地说：

在从根到叶的特定路径中，单个State# 令牌贯穿整个路径，因此当需要答案时，所有 ST 操作将按顺序执行 对于两条路径，它们共有的部分树中的 ST 操作（在拆分之前）是安全的，并且以您期望的方式在两条路径之间正确“共享” 两条路径拆分后，两个独立分支中动作的相对顺序未指定

我相信还有一个进一步的保证，尽管这有点难以推理：

如果在最终的答案列表（即由runSTT 生成的列表）中，您强制索引k 处的单个答案 - 或者，实际上，我认为如果您只是强制证明的列表构造函数在索引k 处有一个答案 - 然后将执行树的深度优先遍历中直到该答案的所有操作。问题是树中的其他操作也可能已执行。

例如，下面的程序：

-# OPTIONS_GHC -Wall #-

import Control.Monad.Trans
import Control.Monad.ST.Trans

type M s = STT s []

foo :: STRef s Int -> M s Int
foo r = do
  _ <- lift [1::Int,2,3]
  writeSTRef r 1
  n1 <- readSTRef r
  n2 <- readSTRef r
  let f = n1 + n2*2
  writeSTRef r f
  return f

main :: IO ()
main = print $ runSTT $ foo =<< newSTRef 9999

使用-O0（答案是[3,3,3]）与-O2（答案是[3,7,15]）编译时，在GHC 8.4.3 下会产生不同的答案。

在其（简单）计算树中：

    root
   /  |  \
  1   2   3          _ <- lift [1,2,3]
 /    |    \
wr    wr    wr       writeSTRef r 1
|     |     |
rd    rd    rd       n1 <- readSTRef r
|     |     |
rd    rd    rd       n2 <- readSTRef r
|     |     |
wr    wr    wr       writeSTRef r (n1 + n2*2)
|     |     |
f     f     f        return (n1 + n2*2)

我们可以推断，当请求第一个值时，左分支中的写/读/读/写动作已经执行。 （在这种情况下，我认为中间分支上的写入和读取也已执行，如下所述，但我有点不确定。）

求第二个值的时候，我们知道左分支的所有动作都已经按顺序执行了，中间分支的所有动作都按顺序执行了，但是我们不知道它们之间的相对顺序那些树枝。它们可能已经完全按顺序执行（给出答案3），或者它们可能已经交错，以便左分支上的最终写入落在右分支上的两个读取之间（给出答案1 + 2*3 = 7。