Тип Rank-1 требует расширения Rank2Types

вики-страница Haskell на Rank-N-Types сообщает, что этот тип

forall a . a -> (forall b . b -> a)

имеет ранг 1. Я верю в этот факт, и он кажется мне вполне понятным (имея в виду то, что я уже знаю о том, как определить ранг функции). Однако, когда я пытаюсь написать следующий код:

{-# LANGUAGE ExplicitForAll #-}

foo :: forall a . a -> (forall b . b -> a)
foo = undefined

он не компилируется (ghc 8.0.1), что приводит к следующей ошибке:

• Illegal polymorphic type: forall b. b -> a
  Perhaps you intended to use RankNTypes or Rank2Types
• In the type signature:
    foo :: forall a. a -> (forall b. b -> a)

Вот мне интересно: действительно ли тип foo имеет Ранг-2? Или у GHC просто нет какого-то умного механизма для определения истинного ранга функции? Иногда в образовательных целях я хочу иметь некоторую команду ghci, например rank, для проверки истинных рангов типов функций...

ghci> :rank foo
foo :: forall a . a -> (forall b . b -> a)  -- Rank 1

types functional-programming haskell higher-rank-types forall
person Shersh    schedule 18.12.2016    source источник
comment
В Haskell 98 forall не является зарезервированным символом. Чтобы использовать его в качестве явного квантификатора, требуется одно из этих двух языковых расширений, даже если типы, которые вы хотите написать, имеют ранг 1. Типы ранга 1 обычно имеют эквивалентную форму, в которой квантификаторы можно оставить неявными, отсюда и эта проблема: ожидание что вы включаете явный forall только в том случае, если хотите подняться выше ранга 1, где он вам действительно нужен.   -  person pigworker    schedule 18.12.2016
comment
@pigworker Я не использую Haskell 98, я использую Haskell 2010. И я включил конкретное расширение ghc -XExplicitForAll. Я просто ожидал, что это расширение будет работать как что-то вроде гипотетического -XRank1Types, где все forall должны быть подняты, если это возможно. Судя по всему, в последнем руководстве пользователя ghc ничего не говорится о таком поведении: количественная оценка для всех" rel="nofollow noreferrer">downloads.haskell.org/~ghc/latest/docs/html/users_guide/   -  person Shersh    schedule 18.12.2016
comment
Язык Haskell 2010 почти идентичен Haskell 98. Новый стандарт включает больше библиотечных функций и стандартизирует объявления пустых данных и средства защиты шаблонов. Если и есть какие-то другие расширения языка, то они очень маленькие.   -  person dfeuer    schedule 19.12.2016

Ответы (1)


arrow_upward
3
arrow_downward

Причина такого поведения задокументирована в модуле TcValidity typechecker. .

Note [Higher rank types]
~~~~~~~~~~~~~~~~~~~~~~~~
Technically
            Int -> forall a. a->a
is still a rank-1 type, but it's not Haskell 98 (Trac #5957).  So the
validity checker allow a forall after an arrow only if we allow it
before — that is, with Rank2Types or RankNTypes

Я не очень хорошо разбираюсь в языках, но мне кажется, что спецификация Haskell 98 не позволяет использовать квантификаторы после любых стрелок, несмотря на то, что это более строгое требование, чем ранг 1. Поскольку Haskell 2010 лишь слегка обновил спецификацию, я считаю, что это применимо и к 2010 году.

Я полагаю (но не уверен), что GHC кодирует это с помощью let r1 = LimitedRank True r0 в функции checkValidType, которая указывает, что forall могут появляться в начале объявления типа, но последующие аргументы функции должны иметь нулевой ранг, что исключает forall b. b -> a в вашем тип.

стандартный отказ от ответственности: я не эксперт, все, что у меня было, это поиск на github

person hao    schedule 18.12.2016
comment
AFAIK forall справа от -> перемещаются в верхнюю часть области видимости. Они могут отображаться в аннотациях типов вводящим в заблуждение образом. Фактический тип foo — forall a b. a -> b -> a. - person András Kovács; 18.12.2016