Подтвердить что ты не робот

RunST и функциональный состав

Почему эта typecheck:

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

Ответ 1

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

> :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. У нас была реализация boxy, но я понял это при реализации нового typechecker. Никто этого не понимал.

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

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

Ответ 2

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

Ответ 3

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

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

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