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

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

Параметричний поліморфізм може бути протиставлений ad hoc поліморфізму. Параметрично поліморфні визначення є універсальними: вони поводяться однаково незалежно від того, для якого типу вони інстанційовані.Шаблон:RpШаблон:Rp На відміну від цього, визначення ad hoc поліморфізму створюються окремо для кожного типу. Таким чином, ad hoc поліморфізм зазвичай підтримує лише обмежену кількість таких окремих типів, оскільки для кожного типу потрібна окрема реалізація.

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

Можна писати функції, які не залежать від типів своїх аргументів. Наприклад, тотожна функція $𝗂𝖽(x)=x$ просто повертає свій аргумент без змін. Це природно породжує сімейство можливих типів, таких як $𝖨𝗇𝗍\to 𝖨𝗇𝗍$, $𝖡𝗈𝗈𝗅\to 𝖡𝗈𝗈𝗅$, $𝖲𝗍𝗋𝗂𝗇𝗀\to 𝖲𝗍𝗋𝗂𝗇𝗀$ тощо. Параметричний поліморфізм дозволяє задати для $𝗂𝖽$ єдиний, найзагальніший тип, вводячи універсально квантифіковану змінну типу:

$𝗂𝖽:\mathrm{\forall }\alpha .\alpha \to \alpha$

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

Тотожна функція є надзвичайним прикладом, але багато інших функцій також виграють від параметричного поліморфізму. Наприклад, функція $𝖺𝗉𝗉𝖾𝗇𝖽$, яка з’єднує два списки, не аналізує елементи списку, а працює лише зі структурою самого списку. Тому $𝖺𝗉𝗉𝖾𝗇𝖽$ може мати подібну сім'ю типів, таких як $[𝖨𝗇𝗍]\times [𝖨𝗇𝗍]\to [𝖨𝗇𝗍]$, $[𝖡𝗈𝗈𝗅]\times [𝖡𝗈𝗈𝗅]\to [𝖡𝗈𝗈𝗅]$ тощо, де $[T]$ позначає список елементів типу $T$. Найзагальніший тип, таким чином, виглядає так:

$𝖺𝗉𝗉𝖾𝗇𝖽:\mathrm{\forall }\alpha .[\alpha ]\times [\alpha ]\to [\alpha ]$

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

Параметрично поліморфні функції, такі як $𝗂𝖽$ і $𝖺𝗉𝗉𝖾𝗇𝖽$, кажуть, що вони параметризовані довільним типом $\alpha$. Обидві функції $𝗂𝖽$ і $𝖺𝗉𝗉𝖾𝗇𝖽$ параметризовані одним типом, але функції можуть бути параметризовані довільною кількістю типів. Наприклад, функції $𝖿𝗌𝗍$ і $𝗌𝗇𝖽$, які повертають перший і другий елементи пари, відповідно, можуть мати такі типи:

$\begin{array}{cc}𝖿𝗌𝗍& :\mathrm{\forall }\alpha .\mathrm{\forall }\beta .\alpha \times \beta \to \alpha \\ 𝗌𝗇𝖽& :\mathrm{\forall }\alpha .\mathrm{\forall }\beta .\alpha \times \beta \to \beta \end{array}$

У виразі $𝖿𝗌𝗍((3,𝗍𝗋𝗎𝖾))$ тип $\alpha$ інстанційований як $𝖨𝗇𝗍$, а $\beta$ — як $𝖡𝗈𝗈𝗅$ у виклику $𝖿𝗌𝗍$. Тому тип усього виразу є $𝖨𝗇𝗍$.

Синтаксис, який використовується для введення параметричного поліморфізму, значно відрізняється між мовами програмування. Наприклад, у деяких мовах програмування, таких як Haskell, квантор $\mathrm{\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-го рангу (предикативний)

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

Наслідком предикативності є те, що всі типи можуть бути записані у формі, яка розміщує всі квантори на зовнішній (пренексній) позиції. Наприклад, розглянемо функцію $𝖺𝗉𝗉𝖾𝗇𝖽$, описану вище, яка має наступний тип:

$𝖺𝗉𝗉𝖾𝗇𝖽:\mathrm{\forall }\alpha .[\alpha ]\times [\alpha ]\to [\alpha ]$

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

В імпредикативній системі $T$ може бути будь-яким типом, включаючи тип, який сам є поліморфним; таким чином, $𝖺𝗉𝗉𝖾𝗇𝖽$ можна застосовувати до пар списків із елементами будь-якого типу — навіть до списків поліморфних функцій, таких як сама $𝖺𝗉𝗉𝖾𝗇𝖽$. Поліморфізм у мові ML є предикативним.Шаблон:Citation needed Це тому, що предикативність разом з іншими обмеженнями робить систему типів настільки простою, що повне виведення типів завжди можливе.

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

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

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

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

Вивід типів для поліморфізму рангу 2 є вирішуваним, але для рангів 3 і вище — ні.Шаблон:Rp

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

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

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

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

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

Джерела

• Шаблон:Citation.
• Шаблон:Cite conference
• Шаблон:Citation.
• Шаблон:Citation.
• Шаблон:Cite journal
• Шаблон:Cite journal
• Шаблон:Cite book