ST monad, изначально разработанный Launchbury и Peyton Jones, позволяет программистам Haskell писать императивный код (с изменяемыми переменными, массивами и т.д.), получая чистый интерфейс к этому коду.
Более конкретно, полиморфный тип функции точки входа
runST :: (forall s. ST s a) -> a
гарантирует, что все побочные эффекты вычисления ST содержатся, и полученное значение является чистым.
Было ли это когда-либо строго (или даже формально) доказано?
Так получилось, что Амин Тимани и др. недавно опубликовали статью на POPL2018 по этой теме. Здесь вы можете найти бумагу здесь. Полное раскрытие: я не нашел времени, чтобы прочитать его полностью, но сам:).
Ниже приведена форма формализация Agda от Andrea Vezzosi, которая доказывает, что runST является безопасным и итоговым для монады ST с читаемыми/записи для записи. Он опирается на постулированную параметричность, т.е. е. истина свободных теорем для задействованных определений, которая как и ожидалось, поскольку параметричность является именно тем, почему работает трюк forall s..
Однако доказательство предполагает, что мы не можем вводить значения внутри STRef s с типами, которые сами зависят от ST s. В Haskell мы можем использовать такую зависимость для получения цикла без рекурсии:
loop :: ()
loop = runST $ do
x <- newSTRef (pure ())
writeSTRef x $ do
y <- readSTRef x
y
y <- readSTRef x
y
Вероятно, эта версия ST-монады по-прежнему безопасна, просто не имеет доказанных итогов writeSTRef и readSTRef.