Specification of `State#`

Question

However, the documentation for STT says:

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.

I would like to be able to judge for myself whether a certain use of the STT monad is safe. In particular, I want to understand the interaction with the List monad. I know that STT sloc (ListT (ST sglob)) a is unsafe, but what about STT sloc []?

I figured out that (at least in GHC), STT is ultimately implemented using magical constructs like MuteVar#, State#, realWorld# etc. Is there any accurate documentation on how these objects behave?

This is closely related to an earlier question of mine.

I think you can determine whether a certain use of STT is safe without understanding State#. Specifically: is the State# used affinely? Then it is safe. Otherwise, not safe. You do not need to know the internal implementation details of State# to make this determination. — Daniel Wagner
Yet realWorld# :: State# RealWorld is certainly not used affinely: it is used every time someone invokes runST. (I do not intend to use the State# affinely, and would like to understand what happens if I don't.) — dremodaris
That's exactly what I want! Will each of them have its own copy of the state, or will they jointly be messing up a common state? To be clear, I intend to use the STT s [] monad. — dremodaris
@dremodaris They will jointly be messing up a common state. The whole point of ST is to use the type system to guarantee a computation that uses mutable state is self-contained, so it can be treated as pure from the perspective of the surrounding context. Think of it as “type-safe, restricted IO”, nothing more. The “state token” does not include any actual state, it is merely an internal implementation detail used by IO and ST to ensure ordering. You cannot safely use STT s [], as the documentation states. If you want to be able to fork the state, you need to use StateT. — Alexis King

K. A. Buhr K. A. Buhr · Accepted Answer · 2018-08-31T17:01:39

You don't really need to understand how State# is implemented. You just need to think of it as a token that's passed through a thread of computations to ensure a certain execution order of ST actions which might otherwise be optimized away.

In an STT s [] monad, you can think of the list actions as producing a tree of possible computations with the final answers at the leaves. At each branching point, the State# token is split. So, roughly speaking:

within a particular path from root to leaf, a single State# token is threaded through the whole path, so all ST actions will be executed in order when the answer is demanded
for two paths, ST actions within the portion of the tree they have in common (before splitting) are safe and properly "shared" between the two paths in the way you'd expect
after two paths split, the relative ordering of the actions in the two independent branches is unspecified

There's a further guarantee, I believe, though it's a little hard to reason about:

If, in the final list of answers (i.e., the list produced by runSTT), you force the single answer at index k -- or, actually, I think if you just force the list constructor that proves there is an answer at index k -- then all actions in a depth-first traversal of the tree up to that answer will have been performed. The catch is that other actions in the tree may have been executed as well.

As an example, the following program:

{-# 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

produces different answers under GHC 8.4.3 when compiled with -O0 (answer is [3,3,3]) versus -O2 (answer is [3,7,15]).

In its (simple) tree of computations:

    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)

we can reason that when the first value is demanded, the write/read/read/write actions in the left branch have been executed. (In this case, I think that the write and read on the middle branch have also been executed, as explained below, but I'm a little unsure.)

When the second value is demanded, we know that all the actions in the left branch have been executed in order, and all the actions in the middle branch have been executed in order, but we don't know the relative order between those branches. They may have been executed fully sequentially (giving the answer 3), or they may have been interleaved so that the final write on the left branch fell between the two reads on the right branch (giving the answer 1 + 2*3 = 7.

Specification of `State#`

1 Answers