Как работает монада ST?

Я понимаю, что монада ST похожа на младшего брата IO, который, в свою очередь, является государственной монадой с добавленной магией RealWorld. Я могу представить состояние, и я могу представить, что RealWorld каким-то образом помещается в IO, но каждый раз, когда я пишу подпись типа ST, s монады ST меня смущает.

Возьмите, например, ST s (STArray s a b). Как работает s? Это просто используется для создания некоторой зависимости искусственных данных между вычислениями, не имея возможности ссылаться как состояния в государственной монаде (из-за forall)?

Я просто выбрасываю идеи и очень ценю кого-то более знающего, чем я, чтобы объяснить это мне.

Ответ 1

s хранит объекты внутри монады ST от утечки вне монады ST.

-- This is an error... but let pretend for a moment...
let a = runST $ newSTRef (15 :: Int)
    b = runST $ writeSTRef a 20
    c = runST $ readSTRef a
in b `seq` c

Хорошо, это ошибка типа (это хорошо, мы не хотим, чтобы STRef просачивался за пределы исходных вычислений!). Это ошибка типа из-за дополнительного s. Помните, что runST имеет подпись:

runST :: (forall s . ST s a) -> a

Это означает, что в s на выполненном вами вычислении не должно быть ограничений. Поэтому, когда вы пытаетесь оценить a:

a = runST (newSTRef (15 :: Int) :: forall s. ST s (STRef s Int))

Результат будет иметь тип STRef s Int, что неверно, так как s "экранировался" вне forall в runST. Переменные типа всегда должны появляться внутри forall, а Haskell допускает неявные forall кванторы везде. Просто не существует правила, позволяющего значительно осмыслить возвращаемый тип a.

Еще один пример с forall: Чтобы четко показать, почему вы не можете позволить вещам избежать forall, вот более простой пример:

f :: (forall a. [a] -> b) -> Bool -> b
f g flag =
  if flag
  then g "abcd"
  else g [1,2]

> :t f length
f length :: Bool -> Int

> :t f id
-- error --

Конечно, f id - ошибка, так как она вернет либо список Char, либо список Int в зависимости от того, является ли логическое значение true или false. Это просто неправильно, как в примере с ST.

С другой стороны,, если у вас не было параметра типа s, тогда все будет набирать проверку просто отлично, хотя код явно довольно фиктивный.

Как работает ST: Реализация, монада ST на самом деле такая же, как монада IO, но с немного другим интерфейсом. Когда вы используете монаду ST, вы фактически получаете unsafePerformIO или эквивалент за кулисами. Причина, по которой вы можете сделать это безопасно, - это сигнатура типа всех ST связанных функций, особенно часть с forall.

Ответ 2

s - это просто хак, который заставляет систему типа останавливать вас на том, что вы делаете небезопасно. Он не "ничего" делает во время выполнения; он просто заставляет проверку типов отклонять программы, которые делают сомнительные вещи. (Это так называемый тип phantom, вещь, которая существует только в головке проверки типа и не влияет ни на что во время выполнения.)