runST и состав функции - PullRequest
Новая
       22

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

53 голосов
/ 27 февраля 2012

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

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 ]

48 голосов
/ 27 февраля 2012

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

> :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) - это новая синтаксическая форма с очевидным правилом набора текста, и все в порядке.

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

такого правила не существует.
34 голосов
/ 27 февраля 2012

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

3 голосов
/ 27 февраля 2012

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

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

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

...