Параметричний поліморфізм — Вікіпедія

У мовах програмування та теорії типів параметричний поліморфізм дозволяє одному й тому ж коду отримувати "загальний" тип із використанням змінних замість конкретних типів, які можуть бути підставлені за потреби.^[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++ підтримує спеціалізацію шаблонів.

Цей розділ потребує додаткових посилань на джерела для поліпшення його перевірності. Будь ласка, допоможіть удосконалити цей розділ, додавши посилання на надійні (авторитетні) джерела. Зверніться на сторінку обговорення за поясненнями та допоможіть виправити недоліки. Матеріал без джерел може бути піддано сумніву та вилучено. (лютий 2019)

У предикативній типізованій системі (також відомій як пренексний поліморфізм), змінні типів не можуть бути замінені на поліморфні типи.^[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. У більшості об'єктно-орієнтованих мов програмування, які підтримують параметричний поліморфізм, параметри можуть бути обмежені підтипами певного типу (див. статті Підтиповий поліморфізм і Узагальнене програмування).

• Hindley, J. Roger (1969), The principal type scheme of an object in combinatory logic, Transactions of the American Mathematical Society, 146: 29—60, doi:10.2307/1995158, JSTOR 1995158, MR 0253905.
• Girard, Jean-Yves (1971). Une Extension de l'Interpretation de Gödel à l'Analyse, et son Application à l'Élimination des Coupures dans l'Analyse et la Théorie des Types. Proceedings of the Second Scandinavian Logic Symposium. Studies in Logic and the Foundations of Mathematics (фр.). Т. 63. Amsterdam. с. 63—92. doi:10.1016/S0049-237X(08)70843-7. ISBN 9780720422597.
• Girard, Jean-Yves (1972), Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur (Ph.D. thesis) (фр.), Université Paris 7.
• Reynolds, John C. (1974), Towards a Theory of Type Structure, 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.
• Milner, Robin (1978). A Theory of Type Polymorphism in Programming (PDF). Journal of Computer and System Sciences. 17 (3): 348—375. doi:10.1016/0022-0000(78)90014-4. S2CID 388583.
• Cardelli, Luca; Wegner, Peter (грудень 1985). On Understanding Types, Data Abstraction, and Polymorphism (PDF). ACM Computing Surveys. 17 (4): 471—523. CiteSeerX 10.1.1.117.695. doi:10.1145/6041.6042. ISSN 0360-0300. S2CID 2921816.
• Pierce, Benjamin C. (2002). Types and Programming Languages. MIT Press. ISBN 978-0-262-16209-8.