`State#` 的规范

Specification of `State#`

然而,documentation for STT 表示:

This monad transformer should not be used with monads that can contain multiple answers, like the list monad. The reason is that the state token will be duplicated across the different answers and this causes Bad Things to happen (such as loss of referential transparency). Safe monads include the monads State, Reader, Writer, Maybe and combinations of their corresponding monad transformers.

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

我发现(至少在 GHC 中),STT 最终是使用像 MuteVar#State#realWorld# 等神奇的构造来实现的。有没有有关这些对象行为方式的准确文档?

这与密切相关。

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

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

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

我相信还有进一步的保证,虽然这有点难以推理:

如果在最终的答案列表(即由 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)

我们可以推断,当需要第一个值时,左侧分支中的 write/read/read/write 操作已被执行。 (在这种情况下,我认为中间分支的写入和读取也已执行,如下所述,但我有点不确定。)

当求第二个值时,我们知道左边分支的所有动作都按顺序执行了,中间分支的所有动作都按顺序执行了,但是不知道相对的这些分支之间的顺序。它们可能已完全按顺序执行(给出答案 3),或者它们可能已经交错,因此左分支上的最终写入介于右分支上的两次读取之间(给出答案 1 + 2*3 = 7.