Почему ограничение класса в синониме типа требует RankNTypes

Question

Это хорошо компилируется:

type List a = [a]

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

type List2 a = Num a => [a]

После включения этого расширения оно прекрасно компилируется. Почему это расширение требуется для компиляции кода?

Изменить: зачем мне ограничение в первую очередь?

Я проверял этот тип объектива (type RefF a b = Functor f => (b -> f b) -> (a -> f a)) из этого поста и выяснил, что это на самом деле нужно RankNTypes из-за Functor ограничение.

Answer 1

Это не стандарт

В котором ответ на вопрос

Простой ответ состоит в том, что стандартный Haskell не допускает объявления синонимов квалифицированных типов, то есть синонимов типов, включающих =>, Согласно отчету 2010 года, синтаксис для объявления синонима типа:

type simpletype = тип

где type, если вы посмотрите вниз на Раздел 4.1.2, не может содержать контекст.

Кстати, наличие переменной типа a в контексте не имеет значения. Без расширений GHC отклоняет

type IrrelevantConstraint a = Num Int => [a]

или, в этом отношении,

type QualifiedT = Num Int => String

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

List2 a      === forall a.   Num a => [a]        -- Okay
List2 a -> b === forall a b. (Num a => [a]) -> b -- Not okay
a -> List2 b === forall a b. a -> Num b => [b]   -- Not okay

И так далее для Maybe (List2 a) и т.д. В каждом случае дело не в том, что это тип более высокого ранга в обычном смысле. Я добавил явную нотацию, которая, конечно, также не является стандартной, чтобы подчеркнуть этот факт.

Скорее проблема в том, что каждый тип неадекватно квалифицирован, потому что => появляется внутри типа. Опять же, если вы посмотрите на разделы отчета 2010 о сигнатурах и декларациях типов выражений, вы увидите, что => это не строго говоря часть типа, а скорее синтаксически отличная вещь, например:

exp → exp :: [ контекст => ] тип

поскольку List2 Недействителен Haskell2010, для его работы необходимо какое-то расширение языка. Это специально не задокументировано, что RankNTypes разрешает объявления синонимов квалифицированных типов, но, как вы заметили, это имеет такой эффект. Зачем?

В документах GHC есть подсказка RankNTypes:

-XRankNTypes опция также требуется для любого типа с полем или контекстом справа от стрелки (например, f :: Int -> forall a. a->a, или же g :: Int -> Ord a => a -> a). Такие типы технически имеют ранг 1, но явно не Haskell-98, и дополнительный флаг, похоже, не стоит беспокоиться.

g пример связан с нашим List2 проблема: нет forall там, но есть контекст справа от стрелки, который является третьим примером, который я привел выше. Как это происходит, RankNTypes позволяет второй пример тоже.

Боковое путешествие по шаблону Haskell

В котором взят обходной путь, мистер Форалл обнаружен в неожиданном месте, и разрабатываются ранги и контексты

Я не знаю, обязательно ли представление Template Haskell объявления связано с внутренним представлением или операцией проверки типов. Но мы находим что-то немного необычное: forall где мы не ожидаем, и без переменных типа:

> import Language.Haskell.TH
> :set -XTemplateHaskell
> runQ [d|type List2 a = Num a => [a]|]
[TySynD List2_2
        [PlainTV a_3]
        (ForallT []
                 [ClassP GHC.Num.Num [VarT a_3]]
                 (AppT ListT (VarT a_3)))]

-- simpler example:
> runQ [d|type T = Num Int => Int|]
[TySynD T_0
        []
        (ForallT []
                 [ClassP GHC.Num.Num [ConT GHC.Types.Int]]
                 (ConT GHC.Types.Int))]

Примечательная вещь здесь, по-видимому, ложная ForallT, В шаблоне Haskell это имеет смысл, потому что ForallT единственный конструктор Type с Cxt поле, то есть это может содержать контекст. Если типограф проверяет аналогично forall и контексты ограничения, имело бы смысл, что RankNTypes повлияло на его поведение. Но так ли это?

Как реализовано в GHC

В котором обнаружено почему RankNTypes позволяет List2

Точная ошибка, которую мы получаем:

Illegal polymorphic or qualified type: Num a => [a]
Perhaps you intended to use RankNTypes or Rank2Types
In the type declaration for `List2'

Поиск по источнику GHC показывает, что эта ошибка генерируется в TcValidity.hs, Точка входа, с которой мы имеем дело, это checkValidType,

Мы можем проверить, что компилятор действительно входит туда, скомпилировав -ddump-tc-trace; последний отладочный вывод перед сообщением об ошибке:

Starting validity check [Type constructor `List2']
checkValidType Num a => [a] :: *

Продолжая в checkValidType мы видим, что отсутствуют RankNTypes RHS синонима типа должен иметь ранг 0. (К сожалению, выходные данные отладки не указывают значение ctxt здесь, но это по-видимому TySynCtxt.)

Примечание чуть выше checkValidType определить ранги в этом контексте следующим образом:

    basic ::= tyvar | T basic ... basic

    r2  ::= forall tvs. cxt => r2a
    r2a ::= r1 -> r2a | basic
    r1  ::= forall tvs. cxt => r0
    r0  ::= r0 -> r0 | basic

Этот комментарий совпадает с экспериментом Template Haskell, то есть тип ранга 0 не может включать => и любой тип, включающий => должен включать в себя forall и, следовательно, иметь ранг 1 или 2, даже если в forall, В терминологии, изложенной в TcType, контексты появляются только в сигма-типах.

Другими словами, как реализовано, проверка типов отклоняет RHS List2 потому что он интерпретирует RHS как ранг 1 из-за его квалификации класса.

Ветвь, которая приводит к нашему сообщению об ошибке, начинается здесь. Если я правильно понимаю, theta представляет контекст ограничения. Ядро первой линии do блок forAllAllowed rank, который делает то, на что это похоже. Напомним, что RHS синонима типа ограничен рангом 0; так как ввод не разрешен, мы получаем ошибку.

Это объясняет почему RankNTypes отменяет это ограничение. Если мы проследим, где параметр rank приходит через rank0 в checkValidType а затем через несколько предыдущих строк, мы находим, что RankNTypes флаг в основном перекрывает rank0 ограничение. (Сравните ситуацию с объявлениями по умолчанию.) И поскольку дополнительный контекст был обработан как ошибка ранга, RankNTypes разрешает это.