Есть ли доказательство того, что runST действительно чист?

Монада ST, изначально разработанная Launchbury и Peyton Jones, позволяет программистам на Haskell писать императивный код (с изменяемыми переменными, массивами и т. Д.), Получая при этом чистый интерфейс с этим кодом.

Конкретнее, полиморфный тип функции точки входа

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

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

Было ли это когда-либо строго (или даже формально) доказано?

Источник

2 ответа

Решение

Так уж сложилось, что Амин Тимани и соавт. недавно опубликовал статью на POPL2018 именно об этой теме. Вы можете найти бумагу здесь. Полное раскрытие: я еще не нашел время, чтобы прочитать его полностью:).

Источник

Вот формализация Агды Андреа Веццози, которая доказывает, что 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,

Источник
Другие вопросы по тегам