ST-подобная инкапсуляция

Question

Я пытаюсь использовать систему типов, чтобы гарантировать, что X никогда не может быть извлечен из монады М. Я ожидаю, что она будет работать аналогично runST, где невозможно смешивать среды из разных потоков.

data X s = X Int
type M s = State Int

newX :: M s (X s)
newX = X <$> get

eval :: (forall s. M s a) -> a
eval x = evalState x 0

Однако следующий код не вызывает ошибку типа:

ghci> x = eval newX
ghci> :t x
x :: X s

Почему аналогичный код в монаде ST выдает ошибку, а мой - нет? Насколько я понимаю, s в M s a должен стать связанным, делая s в X s переменной свободного типа и, таким образом, вызывая ошибку в контролере типов.

Answer 1

Чтобы применить абстракцию типа, вы должны использовать data или newtype, а не type.

Неиспользуемый параметр в синониме type не действует вообще:

type M s = State Int

Итак, это эквивалентно:

newX :: M s (X s)
newX :: State Int (X s)

eval :: (forall s. M s a) -> a
eval :: State Int a -> a

eval на самом деле не более высокого ранга.