Какова связь между рангом полиморфизма и (не)предикативностью?

Какова связь между рангом полиморфизма и (не)предикативностью?

Может ли полиморфизм ранга 1 быть предикативным или непредикативным?

Может ли полиморфизм ранга k с k > 1 быть либо предикативным, либо непредикативным?

Мои заблуждения исходят из:

Почему https://en.wikipedia.org/wiki/Parametric_polymorphism упоминает предикативность под рангом? 1 полиморфизм? (Мне кажется, ранг-1 подразумевает предикативность)

Полиморфизм ранга-1 (предварительный)

В пренекс-полиморфной системе переменные типа не могут быть созданы с полиморфными типами.[4] Это очень похоже на то, что называется «ML-стиль» или «Let-полиморфизм» (технически Let-полиморфизм ML имеет несколько других синтаксических ограничений). Это ограничение делает очень важным различие между полиморфными и неполиморфными типами; таким образом, в предикативных системах полиморфные типы иногда называют схемами типов, чтобы отличить их от обычных (мономорфных) типов, которые иногда называют монотипами. Следствием этого является то, что все типы могут быть записаны в форме, которая помещает все квантификаторы в крайнюю (предварительную) позицию. Например, рассмотрим описанную выше функцию добавления, имеющую тип

forall a. [a] × [a] -> [a]

Чтобы применить эту функцию к паре списков, необходимо подставить тип вместо переменной a в типе функции так, чтобы тип аргументов совпадал с результирующим типом функции.

В непредикативной системе заменяемый тип может быть любым типом, включая тип, который сам является полиморфным; Таким образом, append может применяться к парам списков с элементами любого типа — даже к спискам полиморфных функций, таких как сама функция append. Полиморфизм в языке ML является предикативным.[Необходима цитата] Это связано с тем, что предикативность вместе с другими ограничениями делает систему типов достаточно простой, чтобы всегда был возможен полный вывод типов.

В качестве практического примера, OCaml (потомок или диалект ML) выполняет вывод типов и поддерживает непредикативный полиморфизм, но в некоторых случаях, когда используется непредикативный полиморфизм, вывод типа системой будет неполным, если программист не предоставит некоторые явные аннотации типов.

...

Предикативный полиморфизм

В предикативной параметрической полиморфной системе тип τ, содержащий переменную типа α, не может использоваться таким образом, чтобы α реализовывался как полиморфный тип. Теории предикативных типов включают теорию типов Мартина-Лёфа и NuPRL.

https://wiki.haskell.org/Impredicative_types:

Непредикативные типы — это продвинутая форма полиморфизма, в отличие от типов ранга N.

Стандартный Haskell допускает полиморфные типы за счет использования переменных типа, которые считаются универсально определяемыми количественно: id :: a -> a означает «для всех типов a, id может принимать аргумент и возвращать результат этого типа». Все универсальные квантификаторы («для всех») должны стоять в начале типа.

Полиморфизм более высокого ранга (например, типы ранга N) позволяет универсальным квантификаторам также появляться внутри функциональных типов. Оказывается, справа от функциональных стрелок появляться неинтересно: Int -> forall a. a -> [a] на самом деле то же самое, что и forall a. Int -> a -> [a].

Однако полиморфизм более высокого ранга также допускает квантификаторы слева от функциональных стрелок, и (forall a. [a] -> Int) -> Int действительно отличается от forall a. ([a] -> Int) -> Int.

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

Спасибо.


polymorphism parametric-polymorphism haskell programming-languages impredicativetypes
person Tim    schedule 03.10.2019    source источник
comment
Кстати, в будущем вы можете избавить себя от душевной боли (а меня — нескольких секунд усилий), явно связав вопросы, которые вы уже прочитали, которые не отвечают на ваш вопрос, и объяснив, почему они не являются ответами. (Это также официально рекомендуется, так что это не просто кислый запрос.)   -  person Daniel Wagner    schedule 03.10.2019

Ответы (1)


arrow_upward
6
arrow_downward

Может ли полиморфизм ранга 1 быть предикативным или непредикативным?

Нет, полиморфизм ранга 1 всегда является предикативным, потому что любые кванторы forall не появляются в качестве аргументов конструкторов типов, то есть кванторы являются «предварительными».

Может ли полиморфизм ранга k с k > 1 быть предикативным или непредикативным?

Полиморфизм более высокого ранга всегда непредикативен; расширение RankNTypes включает непредикативный полиморфизм только для конструктора (->), то есть, если тип a -> b, a или b может быть создан с типом, содержащим foralls. Обычно мы называем такие типы высокоранговыми только тогда, когда a содержит forall, потому что (за исключением TypeApplications) X -> forall t. Y эквивалентно forall t. X -> Y.

Общий импредикативный полиморфизм (с неработающим расширением ImpredicativeTypes) не поддерживается. Например, вы не можете написать Maybe (forall a. [a] -> [a]). По сути, это связано с тем, что сложно автоматически определить, когда обобщать, а когда конкретизировать этот квантификатор. К счастью, вы можете сделать это явным, используя оболочку newtype, чтобы «скрыть» непредикативность, или, скорее, дать понять компилятору, что вы хотите делать с квантификаторами, например:

{-# LANGUAGE RankNTypes #-}

newtype ListTransform = ListTransform { unLT :: forall a. [a] -> [a] }

f :: Maybe ListTransform -> [Int] -> [Char] -> ([Int], [Char])
f Nothing is cs = (is, cs)
f (Just (ListTransform t)) is cs = (t is, t cs)
-- or: f (Just lt) is cs = (unLT lt is, unLT lt cs)
person Jon Purdy    schedule 03.10.2019