Хаскелл не хочет набирать полиморфизм высокого ранга

Question

Я не понимаю, почему эта программа не печатается:

type Test a = forall z. (a -> z) -> z

cons :: a -> Test a
cons = \a -> \p -> p a

type Identity = forall x. x -> x

t :: Identity
t = \x -> x

c :: Test Identity
c = cons (t :: Identity)

main :: IO ()
main = do{
  print "test"
}

Я использую опцию -XRankNTypes с GHC.

У меня есть следующая ошибка:

Couldn't match type `x0 -> x0' with `forall x. x -> x'
Expected type: Identity
  Actual type: x0 -> x0
In the first argument of `cons', namely `(t :: Identity)'
In the expression: cons (t :: Identity)
In an equation for `c': c = cons (t :: Identity)

Может ли кто-нибудь помочь мне?

Answer 1

Вывод с RankNTypes это сложно. Попробуйте аннотировать функцию вместо аргумента.

c :: Test Identity
c = (cons :: Identity -> Test Identity) t

Почему это так, требует углубления в тонкости алгоритма вывода типов. Вот некоторая интуиция за этим.

Интуитивно, всякий раз, когда полиморфное значение x :: forall a. F(a) используется переменная типа a никогда не создается автоматически для полиморфного типа. Скорее, a заменяется неизвестной новой переменной a0 (ранжирование по мономорфным типам). Эта переменная затем используется для создания уравнений типа, которые затем решаются с использованием объединения позже.

Пример:

id id :: ??

Давайте назовем два случая как id0 а также id1, Мы получаем

id0 id1 :: ?? 
id0 :: forall a. a->a
id1 :: forall a. a->a

Создайте свежие переменные

id0 :: a0 -> a0
id1 :: a1 -> a1

Унифицируйте тип аргумента: a0 ~ (a1 -> a1),

id0 :: (a1 -> a1) -> (a1 -> a1)
id1 :: a1 -> a1

Применять.

id0 id1 :: a1 -> a1

Re-обобщать.

id0 id1 :: forall a. a->a

Обратите внимание, что в этом конкретном случае мы могли бы получить тот же конечный результат, объединяя a0 ~ (forall a. a->a) вместо этого и избегая генерировать свежий неизвестный a1, Это, однако, не то, что происходит в алгоритме вывода.

Мы можем достичь последнего экземпляра, если прибегнем к ручному вводу:

(id :: (forall a. a->a) -> (forall a. a->a)) id

Однако есть некоторые исключения из вышеприведенного обсуждения. Основным из них являются типы ранга 2 (и ранга N). Когда GHC знает, что функция имеет более высокий рейтинг, ее аргумент обрабатывается по-другому: forallпеременные, встречающиеся в своем типе, не заменяются неизвестными. Скорее, foralls хранятся так, чтобы впоследствии их можно было сопоставить с типом, ожидаемым функцией.

Я рекомендую прочитать руководство пользователя GHC, которое немного объясняет, что происходит. Если вы хотите получить все подробности, вам нужно обратиться к документам, описывающим действительные правила набора текста. (На самом деле, прежде чем читать их, я изучу некоторые основы в некоторых более простых системах, например, в базовых принципах Хиндли-Милнера)