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

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

1 голос
/ 03 октября 2019

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

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

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

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

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

Полиморфизм ранга-1 (prenex)

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

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

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

В непредсказуемой системе замещаемый тип может быть любым типом, в том числе типом, который сам по себе полиморфен;Таким образом, добавление может применяться к парам списков с элементами любого типа - даже к спискам полиморфных функций, таких как добавление. Полиморфизм в языке 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.

Спасибо.

1 Ответ

3 голосов
/ 03 октября 2019

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

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

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

Полиморфизм высшего ранга всегда непредсказуем;расширение RankNTypes разрешает невидимый полиморфизм только для конструктора (->), т. е. для типа a -> b, a или b может быть создан экземпляр с типом, содержащим forall s,Мы обычно ссылаемся на такие типы как более высокий ранг только тогда, когда 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)
...