Параметричний поліморфізм

У мовах програмування та теорії типів параметричний поліморфізм дозволяє одному й тому ж коду отримувати "загальний" тип із використанням змінних замість конкретних типів, які можуть бути підставлені за потреби.^[1]:340 Параметрично поліморфні функції та типи даних іноді називають відповідно узагальненими функціями та узагальненими типами даних. Вони є основою узагальненого програмування.

Параметричний поліморфізм може бути протиставлений ad hoc поліморфізму. Параметрично поліморфні визначення є універсальними: вони поводяться однаково незалежно від того, для якого типу вони інстанційовані.^{[1]:340[2]:37} На відміну від цього, визначення ad hoc поліморфізму створюються окремо для кожного типу. Таким чином, ad hoc поліморфізм зазвичай підтримує лише обмежену кількість таких окремих типів, оскільки для кожного типу потрібна окрема реалізація.

Основне визначення

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

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

Параметрично поліморфне визначення потім може бути інстанційоване шляхом підстановки будь-якого конкретного типу замість ${\displaystyle \alpha }$, що утворює повне сімейство можливих типів.^[3]

Тотожна функція є надзвичайним прикладом, але багато інших функцій також виграють від параметричного поліморфізму. Наприклад, функція ${\displaystyle {\mathsf {append}}}$, яка з’єднує два списки, не аналізує елементи списку, а працює лише зі структурою самого списку. Тому ${\displaystyle {\mathsf {append}}}$ може мати подібну сім'ю типів, таких як ${\displaystyle [{\mathsf {Int}}]\times [{\mathsf {Int}}]\to [{\mathsf {Int}}]}$, ${\displaystyle [{\mathsf {Bool}}]\times [{\mathsf {Bool}}]\to [{\mathsf {Bool}}]}$ тощо, де ${\displaystyle [T]}$ позначає список елементів типу ${\displaystyle T}$. Найзагальніший тип, таким чином, виглядає так:

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

Цей тип може бути інстанційований для будь-якого типу з сім'ї.

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

${\displaystyle {\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}}}$

У виразі ${\displaystyle {\mathsf {fst}}((3,{\mathsf {true}}))}$ тип ${\displaystyle \alpha }$ інстанційований як ${\displaystyle {\mathsf {Int}}}$, а ${\displaystyle \beta }$ — як ${\displaystyle {\mathsf {Bool}}}$ у виклику ${\displaystyle {\mathsf {fst}}}$. Тому тип усього виразу є ${\displaystyle {\mathsf {Int}}}$.

Синтаксис, який використовується для введення параметричного поліморфізму, значно відрізняється між мовами програмування. Наприклад, у деяких мовах програмування, таких як Haskell, квантор ${\displaystyle \forall \alpha }$ є неявним і може бути опущеним.^[5] Інші мови вимагають явно визначати типи в деяких або всіх точках виклику параметрично поліморфної функції.

Історія

Параметричний поліморфізм вперше був введений у мови програмування в ML у 1975 році.^[6] Сьогодні він існує у Standard ML, OCaml, F#, Ada, Haskell, Mercury, Visual Prolog, Scala, Julia, Python, TypeScript, C++ та інших. Java, C#, Visual Basic .NET та Delphi також додали підтримку "дженериків" для параметричного поліморфізму. Деякі реалізації типового поліморфізму зовнішньо схожі на параметричний поліморфізм, але також включають елементи ад-хок. Наприклад, C++ підтримує спеціалізацію шаблонів.

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

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

У предикативній типізованій системі (також відомій як пренексний поліморфізм), змінні типів не можуть бути замінені на поліморфні типи.^[1]: Предикативні теорії типів включають теорію типів Мартіна-Льофа та Nuprl. Це дуже схоже на так званий "ML-стиль" або "Let-поліморфізм" (технічно Let-поліморфізм у ML має кілька інших синтаксичних обмежень). Це обмеження робить розрізнення між поліморфними і неполіморфними типами дуже важливим; таким чином, у предикативних системах поліморфні типи іноді називають схемами типів, щоб відрізняти їх від звичайних (монополіморфних) типів, які іноді називають монотипами.

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

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

Щоб застосувати цю функцію до пари списків, необхідно підставити конкретний тип ${\displaystyle T}$ замість змінної ${\displaystyle \alpha }$ так, щоб отриманий тип функції відповідав типам аргументів.

В імпредикативній системі ${\displaystyle T}$ може бути будь-яким типом, включаючи тип, який сам є поліморфним; таким чином, ${\displaystyle {\mathsf {append}}}$ можна застосовувати до пар списків із елементами будь-якого типу — навіть до списків поліморфних функцій, таких як сама ${\displaystyle {\mathsf {append}}}$. Поліморфізм у мові ML є предикативним.^{[джерело?]} Це тому, що предикативність разом з іншими обмеженнями робить систему типів настільки простою, що повне виведення типів завжди можливе.

Як практичний приклад, OCaml (нащадок або діалект ML) виконує виведення типів і підтримує імпредикативний поліморфізм, але в деяких випадках, коли використовується імпредикативний поліморфізм, система виведення типів є неповною, якщо програміст не надає явні анотації типів.

Поліморфізм вищого рангу

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

Тип вважається типом рангу k (для деякого цілого числа k), якщо жоден шлях від його кореня до квантора ${\displaystyle \forall }$ не проходить зліва від k або більше стрілок, якщо тип зображений як дерево.^[1]:359 Система типів підтримує поліморфізм рангу k, якщо вона дозволяє типи з рангом, що не перевищує k. Наприклад, система типів, яка підтримує поліморфізм рангу 2, дозволяє тип ${\displaystyle (\forall \alpha .\alpha \rightarrow \alpha )\rightarrow T}$, але не ${\displaystyle ((\forall \alpha .\alpha \rightarrow \alpha )\rightarrow T)\rightarrow T}$. Система типів, яка допускає типи будь-якого рангу, називається "ранг-n поліморфною".

Вивід типів для поліморфізму рангу 2 є вирішуваним, але для рангів 3 і вище — ні.^[8][1]:359

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

Імпредикативний поліморфізм (також відомий як поліморфізм першого класу) є найпотужнішою формою параметричного поліморфізму.^[1]:340 У формальній логіці визначення називається імпредикативним, якщо воно є самореференційним; у теорії типів це стосується можливості, щоб тип знаходився в області дії квантора, який його містить. Це дозволяє підстановку будь-якої змінної типу будь-яким типом, включно з поліморфними типами. Прикладом системи, яка підтримує повну імпредикативність, є System F, що дозволяє підстановку ${\displaystyle \forall \alpha .\alpha \to \alpha }$ для будь-якого типу, включно із самим собою.

У теорії типів найчастіше досліджуваними імпредикативними типізованими λ-численнями є ті, що базуються на лямбда-куб, особливо System F.

Обмежений параметричний поліморфізм

Докладніше: Обмежена квантифікація

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