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

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

Параметрический полиморфизм можно противопоставить специальному полиморфизму . Параметрически полиморфные определения единообразны : они ведут себя одинаково независимо от типа, в котором они созданы. Напротив, в специальных полиморфных определениях каждому типу дается отдельное определение. Таким образом, специальный полиморфизм обычно может поддерживать только ограниченное количество таких различных типов, поскольку для каждого типа должна быть предусмотрена отдельная реализация.

Основное определение

Можно писать функции, не зависящие от типов своих аргументов. Например, тождественная функция ${\mathsf {id}}(x)=x$ просто возвращает свой аргумент без изменений. Это естественным образом приводит к появлению семейства потенциальных типов, таких как ${\mathsf {Int}}\to {\mathsf {Int}}$, ${\mathsf {Bool}}\to {\mathsf {Bool}}$, ${\mathsf {String}}\to {\mathsf {String}}$, и так далее. Параметрический полиморфизм позволяет ${\mathsf {id}}$ получить один, наиболее общий тип, путем введения универсальной переменной типа :

${\mathsf {id}}:\forall \alpha .\alpha \to \alpha$

Затем полиморфное определение можно реализовать , заменив любой конкретный тип на любой конкретный тип. $\alpha$, что дает полное семейство потенциальных типов.

Функция идентичности является особенно крайним примером, но многие другие функции также выигрывают от параметрического полиморфизма. Например, ${\mathsf {append}}$ функция, объединяющая два списка, не проверяет элементы списка, а только саму структуру списка. Поэтому, ${\mathsf {append}}$ можно задать аналогичное семейство типов, например $[{\mathsf {Int}}]\times [{\mathsf {Int}}]\to [{\mathsf {Int}}]$, $[{\mathsf {Bool}}]\times [{\mathsf {Bool}}]\to [{\mathsf {Bool}}]$и так далее, где $[T]$ обозначает список элементов типа $T$. Поэтому наиболее общим типом является

${\mathsf {append}}:\forall \alpha .[\alpha ]\times [\alpha ]\to [\alpha ]$

который может быть создан для любого типа в семействе.

Параметрически полиморфные функции типа ${\mathsf {id}}$ и ${\mathsf {append}}$ называются параметризованными по произвольному типу $\alpha$. Оба ${\mathsf {id}}$ и ${\mathsf {append}}$ параметризуются по одному типу, но функции могут быть параметризованы по произвольному числу типов. Например, ${\mathsf {fst}}$ и ${\mathsf {snd}}$ функциям, возвращающим первый и второй элементы пары соответственно , можно присвоить следующие типы:

${\begin{aligned}{\mathsf {fst}}&:\forall \alpha .\forall \beta .\alpha \times \beta \to \alpha \\{\mathsf {snd}}&:\forall \alpha .\forall \beta .\alpha \times \beta \to \beta \end{aligned}}$

В выражении ${\mathsf {fst}}((3,{\mathsf {true}}))$, $\alpha$ создается для ${\mathsf {Int}}$ и $\beta$ создается для ${\mathsf {Bool}}$ в звонке ${\mathsf {fst}}$, поэтому тип общего выражения равен ${\mathsf {Int}}$.

Синтаксис , используемый для введения параметрического полиморфизма, значительно различается в разных языках программирования. Например, в некоторых языках программирования, таких как Haskell , $\forall \alpha$ Квантор неявный и может быть опущен. параметрически полиморфной функции Другие языки требуют, чтобы типы были созданы явно на некоторых или всех сайтах вызова .

История

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

Предикативность, непредикативность и полиморфизм

ранга 1 (

В системе предикативных типов (также известной как пренекс- полиморфная система) переменные типа не могут быть созданы с помощью полиморфных типов. Теории предикативных типов включают теорию типов Мартина-Лёфа и Nuprl . Это очень похоже на то, что называется «стилем ML» или «Let-полиморфизмом» (технически Let-полиморфизм ML имеет несколько других синтаксических ограничений).Это ограничение делает различие между полиморфными и неполиморфными типами очень важным; таким образом, в предикативных системах полиморфные типы иногда называют схемами типов, чтобы отличить их от обычных (мономорфных) типов, которые иногда называют монотипами .

Следствием предикативности является то, что все типы могут быть записаны в форме, в которой все кванторы располагаются в самой внешней (пренексной) позиции. Например, рассмотрим ${\mathsf {append}}$ описанная выше функция, которая имеет следующий тип:

${\mathsf {append}}:\forall \alpha .[\alpha ]\times [\alpha ]\to [\alpha ]$

Чтобы применить эту функцию к паре списков, нужен конкретный тип $T$ необходимо заменить переменную $\alpha$ так, чтобы результирующий тип функции соответствовал типам аргументов. В импредикативной системе $T$ может быть любым типом, включая тип, который сам по себе является полиморфным; таким образом ${\mathsf {append}}$ может применяться к парам списков с элементами любого типа — даже к спискам полиморфных функций, таких как ${\mathsf {append}}$ сам.Полиморфизм в языке ML является предикативным. Это связано с тем, что предикативность вместе с другими ограничениями делает систему типов достаточно простой, поэтому полный вывод типов всегда возможен.

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

Полиморфизм более высокого ранга

Некоторые системы типов поддерживают непредикативный конструктор типов функций, хотя другие конструкторы типов остаются предикативными. Например, тип $(\forall \alpha .\alpha \rightarrow \alpha )\rightarrow T$ разрешено в системе, поддерживающей полиморфизм более высокого ранга, даже если $[\forall \alpha .\alpha \rightarrow \alpha ]$ может быть и нет.

Говорят, что тип имеет ранг k (для некоторого фиксированного целого числа k ), если нет пути от его корня до $\forall$ квантор проходит слева от k или более стрелок, если тип нарисован в виде дерева. Говорят, что система типов поддерживает полиморфизм ранга k, если она допускает типы с рангом, меньшим или равным k . Например, система типов, поддерживающая полиморфизм ранга 2, позволит $(\forall \alpha .\alpha \rightarrow \alpha )\rightarrow T$ но не $((\forall \alpha .\alpha \rightarrow \alpha )\rightarrow T)\rightarrow T$. Система типов, допускающая типы произвольного ранга, называется «полиморфной ранга n ».

Вывод типа для полиморфизма ранга 2 разрешим, но для полиморфизма ранга 3 и выше — нет.

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

Импредикативный полиморфизм (также называемый полиморфизмом первого класса ) является наиболее мощной формой параметрического полиморфизма. В формальной логике определение называется непредикативным, если оно самореферентно; в теории типов это относится к способности типа находиться в области содержащегося в нем квантора. Это позволяет создавать экземпляры любой переменной типа любого типа, включая полиморфные типы. Примером системы, поддерживающей полную непредикативность, является Система F , которая позволяет создавать экземпляры. $\forall \alpha .\alpha \to \alpha$ любого типа, включая самого себя.

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

полиморфизм

Основная статья: Ограниченная количественная оценка

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

См. также

• Параметричность
• Полиморфная рекурсия
• Класс типов # Полиморфизм высшего рода
• Черта (компьютерное программирование)

Ссылки

• Хиндли, Дж. Роджер (1969), «Основная схема типа объекта в комбинаторной логике», Transactions of the American Mathematical Society , 146 : 29–60, doi : 10.2307/1995158 , JSTOR   1995158 , MR   0253905 .
• Жирар, Жан-Ив (1971). «Расширение интерпретации Гёделя на анализ и его применение для устранения сокращений в анализе и теории типов». Материалы Второго скандинавского логического симпозиума . Исследования по логике и основам математики (на французском языке). Полет. 63. Амстердам. стр. 63–92. дои : 10.1016/S0049-237X(08)70843-7 . ISBN  9780720422597 .
• Жирар, Жан-Ив (1972), Функциональная интерпретация и устранение сокращений в арифметике высшего порядка (докторская диссертация) (на французском языке), Парижский университет 7 .
• Рейнольдс, Джон К. (1974), «К теории типовой структуры» , Коллок по программированию , Конспекты лекций по информатике , 19 , Париж: 408–425, номер документа : 10.1007/3-540-06859-7_148 , ISBN  978-3-540-06859-4 .
• Милнер, Робин (1978). «Теория полиморфизма типов в программировании» (PDF) . Журнал компьютерных и системных наук . 17 (3): 348–375. дои : 10.1016/0022-0000(78)90014-4 . S2CID   388583 .
• Карделли, Лука ; Вегнер, Питер (декабрь 1985 г.). «О понимании типов, абстракции данных и полиморфизме» (PDF) . Обзоры вычислительной техники ACM . 17 (4): 471–523. CiteSeerX   10.1.1.117.695 . дои : 10.1145/6041.6042 . ISSN   0360-0300 . S2CID   2921816 .
• Пирс, Бенджамин К. (2002). Типы и языки программирования . МТИ Пресс. ISBN  978-0-262-16209-8 .