Haskell: карта runST

Ответ 1

Каждый раз, когда вы запускаете трансформатор состояния с runST, он работает в каком-то локальном состоянии, которое отделено от всех других трансформаторов состояния. runST создает новый тип состояния и вызывает его аргумент с этим типом. Так, например, если вы выполните

let x = runST (return ())
    y = runST (return ())
in (x, y)

то первый return () и второй return () будут иметь разные типы: ST s1 () и ST s2 () для некоторых неизвестных типов s1 и s2, которые создаются runST.

Вы пытаетесь вызвать runST с аргументом, который имеет тип состояния s. Это не тип состояния, который создает runST, а также другой тип, который вы можете выбрать. Для вызова runST необходимо передать аргумент, который может иметь любой тип состояния. Вот пример:

r1 :: forall s. ST s ()
r1 = return ()

Поскольку r1 является полиморфным, его состояние может иметь любой тип, включая любой тип, выбранный runST. Вы можете сопоставить runST список полиморфных r1 (с -XImpredicativeTypes):

map runST ([r1, r1] :: [forall t. ST t ()])

Однако вы не можете сопоставить runST над списком неполиморфных r1 s.

map runST ([r1, r1] :: forall t. [ST t ()]) -- Not polymorphic enough

Тип forall t. [ST t ()] говорит, что все элементы списка имеют тип состояния t. Но они должны иметь независимые типы состояний, потому что на каждом из них вызывается runST. Это означает, что это сообщение об ошибке.

Если это нормально для всех элементов списка, вы можете вызвать runST один раз, как показано ниже. Явная подпись типа не требуется.

runST (sequence ([r1, r1] :: forall t. [ST t ()]))

Ответ 2

Ваш name недостаточно полиморфный. Ваше выражение

name :: [ST s (Int, [Int])]

означает "список возвращаемых результатов вычисления состояния (Int, [Int]), которые имеют точно такое же s '. Но посмотрите на тип runST:

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

Этот тип означает "функция, которая принимает вычисление с учетом состояния, где s может быть любым, что вы когда-либо могли бы себе представить". Эти типы вычислений - это не одно и то же. И наконец:

map runST :: [forall s. ST s a] -> [a]

Вы видите, ваш список должен содержать больше полиморфных значений, чем сейчас. Тип s может быть различным в каждом элементе списка, он может быть не того же типа, что и в name. Измените подпись типа name, и все должно быть в порядке. Это может потребовать включения некоторых расширений, но GHC должен быть в состоянии сообщить вам, какие из них.

Ответ 3

Я попытаюсь объяснить аргументы типа runST:

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

И почему это не так просто:

alternativeRunST :: ST s a -> a

Обратите внимание, что этот alternativeRunST работал бы для вашей программы.

alternativeRunST также позволил бы нам утечка переменных из монады ST:

leakyVar :: STRef s Int
leakyVar = alternativeRunST (newSTRef 0)

evilFunction :: Int -> Int
evilFunction x =
  alternativeRunST $ do
    val <- readSTRef leakyVar
    writeSTRef leakyVar (val+1)
    return (val + x)

Тогда вы можете пойти в ghci и сделать:

>>> map evilFunction [7,7,7]
[7,8,9]

evilFunction не является ссылочно прозрачным!

Btw, попробовав себе здесь "плохую ST" структуру, необходимую для запуска кода выше:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
import Control.Monad
import Data.IORef
import System.IO.Unsafe
newtype ST s a = ST { unST :: IO a } deriving Monad
newtype STRef s a = STRef { unSTRef :: IORef a }
alternativeRunST :: ST s a -> a
alternativeRunST = unsafePerformIO . unST
newSTRef :: a -> ST s (STRef s a)
newSTRef = ST . liftM STRef . newIORef
readSTRef :: STRef s a -> ST s a
readSTRef = ST . readIORef . unSTRef
writeSTRef :: STRef s a -> a -> ST s ()
writeSTRef ref = ST . writeIORef (unSTRef ref)

Реальный runST не позволяет нам строить такие "злые" функции. Как это делается? Это довольно сложно, см. Ниже:

Попытка запуска:

>>> runST (newSTRef "Hi")
error:
    Couldn't match type `a' with `STRef s [Char]'
...

>>> :t runST
runST :: (forall s. ST s a) -> a
>>> :t newSTRef "Hi"
newSTRef "Hi" :: ST s (STRef s [Char])

newSTRef "Hi" не соответствует (forall s. ST s a). Как можно увидеть, используя еще более простой пример, где GHC дает нам довольно приятную ошибку:

dontEvenRunST :: (forall s. ST s a) -> Int
dontEvenRunST = const 0

>>> dontEvenRunST (newSTRef "Hi")
<interactive>:14:1:
    Couldn't match type `a0' with `STRef s [Char]'
      because type variable `s' would escape its scope

Заметим, что мы также можем написать

dontEvenRunST :: forall a. (forall s. ST s a) -> Int

И это эквивалентно исключению forall a., как мы это делали раньше.

Обратите внимание, что область a больше, чем область s, но в случае newSTRef "Hi" ее значение должно зависеть от s. Система типов не позволяет этого.