runST и состав функций

Почему эта проверка типов:

runST $ return $ True

Пока следующего нет:

runST . return $ True

GHCI жалуется:

Couldn't match expected type `forall s. ST s c0'
            with actual type `m0 a0'
Expected type: a0 -> forall s. ST s c0
  Actual type: a0 -> m0 a0
In the second argument of `(.)', namely `return'
In the expression: runST . return
Источник

3 ответа

Решение

Короткий ответ: вывод типов не всегда работает с типами более высокого ранга. В этом случае он не может определить тип (.), но он проверяет тип, если мы добавим явную аннотацию типа:

> :m + Control.Monad.ST
> :set -XRankNTypes
> :t (((.) :: ((forall s0. ST s0 a) -> a) -> (a -> forall s1. ST s1 a) -> a -> a) runST return) $ True
(((.) :: ((forall s0. ST s0 a) -> a) -> (a -> forall s1. ST s1 a) -> a -> a) runST return) $ True :: Bool

Та же проблема возникает и с вашим первым примером, если мы заменим ($) с нашей собственной версией:

> let app f x = f x
> :t runST `app` (return `app` True)
<interactive>:1:14:
    Couldn't match expected type `forall s. ST s t0'
                with actual type `m0 t10'
    Expected type: t10 -> forall s. ST s t0
      Actual type: t10 -> m0 t10
    In the first argument of `app', namely `return'
    In the second argument of `app', namely `(return `app` True)'

Опять же, это можно решить, добавив аннотации типов:

> :t (app :: ((forall s0. ST s0 a) -> a) -> (forall s1. ST s1 a) -> a) runST (return `app` True)
(app :: ((forall s0. ST s0 a) -> a) -> (forall s1. ST s1 a) -> a) runST (return `app` True) :: Bool

Здесь происходит то, что в GHC 7 есть специальное правило печати, которое применяется только к стандарту. ($) оператор. Саймон Пейтон-Джонс объясняет это поведение в ответе на список рассылки пользователей GHC:

Это мотивирующий пример для вывода типа, который может иметь дело с непредсказуемыми типами. Рассмотрим тип ($):

($) :: forall p q. (p -> q) -> p -> q

В примере нам нужно создать экземпляр p с (forall s. ST s a)и вот что означает непредсказуемый полиморфизм: создание экземпляра переменной типа с полиморфным типом.

К сожалению, я не знаю ни одной системы разумной сложности, которая могла бы проверять [это] без посторонней помощи. Существует множество сложных систем, и я был соавтором по крайней мере двух работ, но все они слишком сложны, чтобы жить в GHC. У нас была реализация коробочных типов, но я снял ее при реализации нового средства проверки типов. Никто не понял этого.

Однако люди так часто пишут

runST $ do ...

что в GHC 7 я реализовал специальное правило печатания, только для инфиксного использования ($), Просто подумай о (f $ x) как новая синтаксическая форма, с очевидным правилом печати, и все готово.

Ваш второй пример терпит неудачу, потому что нет такого правила для (.),

Источник

runST $ do { ... } шаблон настолько распространен, и тот факт, что он обычно не проверяет тип, настолько раздражает, что GHC включает некоторые ST-специфическая проверка типов хаков, чтобы она работала. Эти хаки, вероятно, стреляют здесь для ($) версия, но не (.) версия.

Источник

Сообщения немного сбивают с толку (я так чувствую). Позвольте мне переписать ваш код:

runST (return True)   -- return True is ST s Bool
(runST . return) True  -- cannot work

Другой способ выразить это в том, что мономорфный m0 a0 (результат возврата, если он получит a0) не может быть унифицирован с (forall s.ST s a).

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