规则`State＃`

Question

然而，documentation for STT说：

此monad转换器不应与包含多个答案的monad一起使用，例如list monad。原因是状态令牌将在不同的答案中重复，这会导致坏事发生（例如失去参照透明度）。安全monad包括monads State，Reader，Writer，Maybe和他们相应的monad变换器的组合。

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

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

这与earlier question of mine密切相关。

Answer 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。