Спецификация `State#`

Question

Тем не менее, документация для STT говорит:

Этот преобразователь монад не следует использовать с монадами, которые могут содержать несколько ответов, например, монадой списка. Причина в том, что токен состояния будет дублироваться в разных ответах, что приведет к возникновению плохих вещей (таких как потеря ссылочной прозрачности). К безопасным монадам относятся монады State, Reader, Writer, Maybe и комбинации соответствующих им монадных трансформаторов.

Я хотел бы быть в состоянии судить для себя, является ли определенное использование STT Монада в безопасности. В частности, я хочу понять взаимодействие с монадой List. я знаю это STT sloc (ListT (ST sglob)) a небезопасно, но как насчет STT sloc []?

Я понял, что (по крайней мере, в GHC), STT в конечном итоге реализуется с помощью магических конструкций, таких как MuteVar#, State#, realWorld# и т.д. Есть ли точная документация о том, как ведут себя эти объекты?

Это тесно связано с моим более ранним вопросом.

Answer 1

Вам не нужно понимать, как State# реализовано. Вам просто нужно думать об этом как о токене, который передается через поток вычислений для обеспечения определенного порядка выполнения ST действия, которые иначе могли бы быть оптимизированы.

В STT s [] Монада, вы можете думать о действиях со списком, как о создании дерева возможных вычислений с окончательными ответами на листьях. В каждой точке ветвления 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

выдает разные ответы в GHC 8.4.3 при компиляции с -O0 (ответ [3,3,3]) против -O2 (ответ [3,7,15]).

В его (простом) дереве вычислений:

    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,