Параметрический полиморфизм

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

Например, функция, appendкоторая объединяет два списка, может быть сконструирована так, чтобы она не заботилась о типе элементов: она может добавлять списки целых чисел, списки действительных чисел, списки строк и т. Д. Пусть переменная типа a обозначает тип элементов в списках. Затем appendможно набрать

forall a. [a] × [a] -gt; [a]

где [a]обозначает тип списков с элементами типа a. Мы говорим, что тип appendявляется параметризирован для всех значений. (Обратите внимание, что, поскольку существует только одна переменная типа, функция не может применяться только к любой паре списков: пара, а также список результатов должны состоять из элементов одного и того же типа) Для каждого места, где применяется, значение определяется для a. append

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

• 1 История
• 2 Высший полиморфизм
  • 2.1 Полиморфизм ранга 1 (преднекс)
  • 2.2 Rank- к полиморфизм
  • 2.3 Полиморфизм ранга- n ("высшего ранга")
• 3 Предикативность и отрицательность
  • 3.1 Предикативный полиморфизм
  • 3.2 Импредикативный полиморфизм
• 4 Ограниченный параметрический полиморфизм
• 5 См. Также
• 6 Примечания
• 7 ссылки

Параметрический полиморфизм впервые был введен в языки программирования в ML в 1975 году. Сегодня он существует в стандартном ML, OCaml, F #, Ada, Haskell, Mercury, Visual Prolog, Scala, Julia, Python, TypeScript, C ++ и других. Java, C #, Visual Basic.NET и Delphi представили «универсальные шаблоны» для параметрического полиморфизма. Некоторые реализации полиморфизма типов внешне похожи на параметрический полиморфизм, но при этом вводят специальные аспекты. Одним из примеров является специализация шаблонов C ++.

Наиболее общая форма полиморфизма - это « импредикативный полиморфизм более высокого ранга ». Два популярного ограничения этой формы ограниченный ранга полиморфизм (например, ранг 1 или предваренная полиморфизм) и предикативный полиморфизм. Вместе эти ограничения дают «предикативный предикативный полиморфизм», который, по сути, является формой полиморфизма, обнаруженного в ML и ранних версиях Haskell.

Полиморфизм ранга-1 (пренекс)

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

forall a. [a] × [a] -gt; [a]

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

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

Rank- к полиморфизм

Для некоторого фиксированного значения k полиморфизм ранга k - это система, в которой квантор может не появляться слева от k или более стрелок (когда тип нарисован как дерево).

Вывод типа для полиморфизма ранга 2 разрешим, но реконструкция для ранга 3 и выше - нет.

Полиморфизм ранга- n ("высшего ранга")

Полиморфизм ранга n - это полиморфизм, в котором кванторы могут появляться слева от произвольного количества стрелок.

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

В предикативной параметрической полиморфной системе тип, содержащий переменную типа, не может использоваться таким образом, чтобы он создавался для полиморфного типа. Теории предикативного типа включают теорию типа Мартина-Лёфа и NuPRL. ${\ Displaystyle \ тау}$${\ displaystyle \ alpha}$${\ displaystyle \ alpha}$

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

Импредикативный полиморфизм (также называемый полиморфизмом первого класса) - самая мощная форма параметрического полиморфизма. Определение называется непредикативным, если оно ссылается на себя; в теории типов это позволяет создать экземпляр переменной в типе с любым типом, включая полиморфные типы, такие как он сам. Примером этого является Система F с переменной типа X в типе, где X может даже ссылаться на сам T.${\ Displaystyle \ тау}$${\ Displaystyle \ тау}$ ${\ displaystyle T = \ forall XX \ to X}$

В теории типов, наиболее часто изучал непредикативный типизированный λ-исчисления основаны на тех из лямбда - кубы, особенно System F.

В 1985 году Лука Карделли и Питер Вегнер осознали преимущества разрешения ограничений на параметры типа. Многие операции требуют некоторого знания типов данных, но в остальном могут работать параметрически. Например, чтобы проверить, включен ли элемент в список, нам нужно сравнить элементы на предмет равенства. В стандартном ML параметры типа формы '' a ограничены, чтобы была доступна операция равенства, поэтому функция будет иметь тип '' a × '' a list → bool и '' a может быть только типом с определенным равенство. В Haskell ограничение достигается за счет того, что типы принадлежат классу типов ; таким образом, та же функция имеет тип в Haskell. В большинстве объектно-ориентированных языков программирования, поддерживающих параметрический полиморфизм, параметры могут быть ограничены, чтобы быть подтипами данного типа (см. Полиморфизм подтипов и статью о универсальном программировании ). ${\ displaystyle {\ scriptstyle Eq \, \ alpha \, \ Rightarrow \ alpha \, \ rightarrow \ left [\ alpha \ right] \ rightarrow Bool}}$

• Параметричность
• Полиморфная рекурсия
• Типовой класс # Высший полиморфизм

• Стрейчи, Кристофер (1967), « Фундаментальные концепции языков программирования (конспекты лекций)», Копенгаген: Международная летняя школа компьютерного программирования. Переиздано в: Strachey, Christopher (2000). Вычисление высшего порядка и символическое вычисление. 13: 11–49. DOI : 10,1023 / А: 1010000313106. Отсутствует или пусто |title=( справка )
• Хиндли, Дж Роджер (1969), «Основной тип схемы объекта в комбинаторной логики», Труды Американского математического общества, 146: 29-60, DOI : 10,2307 / 1995158, JSTOR   1995158, МР   0253905.
• Жирар, Жан-Ив (1971). "Une Extension de l'Interpretation de l'Interpretation of Gödel à l'Analyse, et son Application à l'Élimination des Coupures dans l'Analyse et la Théorie des Types". Труды Второго скандинавского логического симпозиума (на французском языке). Амстердам. С. 63–92. DOI : 10.1016 / S0049-237X (08) 70843-7.
• Жирар, Жан-Ив (1972), Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur (докторская диссертация) (на французском языке), Université Paris 7.
• Рейнольдс, Джон К. (1974), «К теории структуры типов», Colloque Sur la Programmation, Lecture Notes in Computer Science, Paris, 19: 408–425, doi : 10.1007 / 3-540-06859-7_148, ISBN   978-3-540-06859-4.
• Милнер, Робин (1978). "Теория полиморфизма типов в программировании" (PDF). Журнал компьютерных и системных наук. 17 (3): 348–375. DOI : 10.1016 / 0022-0000 (78) 90014-4.
• Карделли, Лука ; Вегнер, Питер (декабрь 1985 г.). «Понимание типов, абстракции данных и полиморфизма» (PDF). ACM Computing Surveys. 17 (4): 471–523. CiteSeerX   10.1.1.117.695. DOI : 10.1145 / 6041.6042. ISSN   0360-0300.
• Пирс, Бенджамин С. (2002). Типы и языки программирования. MIT Press. ISBN   978-0-262-16209-8.