Спецификация `State #` - PullRequest
Новая
       24

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

0 голосов
/ 31 августа 2018

Однако документация для STT гласит:

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

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

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

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

1 Ответ

0 голосов
/ 31 августа 2018

Вам на самом деле не нужно понимать, как реализовано 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.

...