Specification of `State#`

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.

Solution

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.