Перегляд вихідного коду сторінки Параметричний поліморфізм

У [[мови програмування|мовах програмування]] та [[теорія типів|теорії типів]] '''параметричний поліморфізм''' дозволяє одному й тому ж коду отримувати "загальний" тип із використанням змінних замість конкретних типів, які можуть бути підставлені за потреби.<ref name="TAPL" />{{rp|340}} Параметрично поліморфні [[функція (програмування)|функції]] та [[тип даних|типи даних]] іноді називають відповідно '''узагальненими функціями''' та '''узагальненими типами даних'''. Вони є основою [[узагальнене програмування|узагальненого програмування]].

Параметричний поліморфізм може бути протиставлений [[ad hoc поліморфізм|ad hoc поліморфізму]]. Параметрично поліморфні визначення є ''універсальними'': вони поводяться однаково незалежно від того, для якого типу вони інстанційовані.<ref name="TAPL" />{{rp|340}}<ref name="Strachey 1967" />{{rp|37}} На відміну від цього, визначення ad hoc поліморфізму створюються окремо для кожного типу. Таким чином, ad hoc поліморфізм зазвичай підтримує лише обмежену кількість таких окремих типів, оскільки для кожного типу потрібна окрема реалізація.
== Основне визначення ==

Можна писати функції, які не залежать від типів своїх аргументів. Наприклад, [[тотожна функція]] <math>\mathsf{id}(x) = x</math> просто повертає свій аргумент без змін. Це природно породжує сімейство можливих типів, таких як <math>\mathsf{Int} \to \mathsf{Int}</math>, <math>\mathsf{Bool} \to \mathsf{Bool}</math>, <math>\mathsf{String} \to \mathsf{String}</math> тощо. Параметричний поліморфізм дозволяє задати для <math>\mathsf{id}</math> єдиний, [[Уніфікація_(інформатика)#Узагальнення,_спеціалізація|найзагальніший]] тип, вводячи [[Квантор загальності|універсально квантифіковану]] [[змінна типу|змінну типу]]:

:<math>\mathsf{id} : \forall \alpha. \alpha \to \alpha</math>

Параметрично поліморфне визначення потім може бути ''інстанційоване'' шляхом підстановки будь-якого конкретного типу замість <math>\alpha</math>, що утворює повне сімейство можливих типів.<ref>{{Cite web |last1=Yorgey |first1=Brent |title=More polymorphism and type classes |url=https://www.seas.upenn.edu/~cis1940/spring13/lectures/05-type-classes.html |website=www.seas.upenn.edu |access-date=1 жовтня 2022}}</ref>

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

:<math>\mathsf{append} : \forall \alpha. [\alpha] \times [\alpha] \to [\alpha]</math>

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

Параметрично поліморфні функції, такі як <math>\mathsf{id}</math> і <math>\mathsf{append}</math>, кажуть, що вони ''параметризовані'' довільним типом <math>\alpha</math>.<ref>{{Cite web |last1=Wu |first1=Brandon |title=Parametric Polymorphism - SML Help |url=https://smlhelp.github.io/book/concepts/poly.html |website=smlhelp.github.io |access-date=1 жовтня 2022}}</ref> Обидві функції <math>\mathsf{id}</math> і <math>\mathsf{append}</math> параметризовані одним типом, але функції можуть бути параметризовані довільною кількістю типів. Наприклад, функції <math>\mathsf{fst}</math> і <math>\mathsf{snd}</math>, які повертають перший і другий елементи [[декартів добуток|пари]], відповідно, можуть мати такі типи:

:<math>
\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}
</math>

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

[[Синтаксис (програмування)|Синтаксис]], який використовується для введення параметричного поліморфізму, значно відрізняється між мовами програмування. Наприклад, у деяких мовах програмування, таких як [[Haskell]], [[Квантор|квантор]] <math>\forall \alpha</math> є неявним і може бути опущеним.<ref>{{Cite web |title=Haskell 2010 Language Report § 4.1.2 Syntax of Types |url=https://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-650004.1.2 |website=www.haskell.org |access-date=1 жовтня 2022 |quote=З одним винятком (спеціальний змінний тип у декларації класу (розділ 4.3.1)), змінні типу в Haskell завжди вважаються універсально квантифікованими; синтаксис для універсальної квантифікації відсутній.}}</ref> Інші мови вимагають явно визначати типи в деяких або всіх [[точка виклику|точках виклику]] параметрично поліморфної функції.

== Історія ==
Параметричний поліморфізм вперше був введений у мови програмування в [[ML (мова програмування)|ML]] у 1975 році.<ref>[[Робін Мілнер|Мілнер, Р.]], Морріс, Л., Ньюї, М. "Логіка для обчислюваних функцій з рефлексивними та поліморфними типами", ''Proc. Conference on Proving and Improving Programs'', Arc-et-Senans (1975)</ref> Сьогодні він існує у [[Standard ML]], [[OCaml]], [[F Sharp|F#]], [[Ada (мова програмування)|Ada]], [[Haskell (мова програмування)|Haskell]], [[Mercury (мова програмування)|Mercury]], [[Visual Prolog]], [[Scala (мова програмування)|Scala]], [[Julia (мова програмування)|Julia]], [[Python]], [[TypeScript]], [[C++]] та інших. [[Java (мова програмування)|Java]], [[C Sharp (мова програмування)|C#]], [[Visual Basic .NET]] та [[Object Pascal|Delphi]] також додали підтримку "дженериків" для параметричного поліморфізму. Деякі реалізації типового поліморфізму зовнішньо схожі на параметричний поліморфізм, але також включають елементи ад-хок. Наприклад, [[C++]] підтримує [[спеціалізація шаблону|спеціалізацію шаблонів]].

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

=== Поліморфізм 1-го рангу (предикативний) ===
{{refimprove section|date=лютий 2019}}
У ''[[імпредикативність|предикативній]]'' типізованій системі (також відомій як ''[[пренексний]] поліморфізм''), змінні типів не можуть бути замінені на поліморфні типи.<ref name="TAPL">{{Cite book|author1=[[Бенджамін К. Пірс]]|title=Types and Programming Languages|url=https://books.google.com/books?id=ti6zoAC9Ph8C|year=2002|publisher=MIT Press|isbn=978-0-262-16209-8}}</ref>{{rp|pages=359–360}} Предикативні теорії типів включають [[інтуїціоністська теорія типів|теорію типів Мартіна-Льофа]] та [[Nuprl]]. Це дуже схоже на так званий "ML-стиль" або "Let-поліморфізм" (технічно Let-поліморфізм у ML має кілька інших синтаксичних обмежень).  
Це обмеження робить розрізнення між поліморфними і неполіморфними типами дуже важливим; таким чином, у предикативних системах поліморфні типи іноді називають ''схемами типів'', щоб відрізняти їх від звичайних (монополіморфних) типів, які іноді називають ''монотипами''.  

Наслідком предикативності є те, що всі типи можуть бути записані у формі, яка розміщує всі квантори на зовнішній (пренексній) позиції. Наприклад, розглянемо функцію <math>\mathsf{append}</math>, описану вище, яка має наступний тип:  
:<math>\mathsf{append} : \forall \alpha. [\alpha] \times [\alpha] \to [\alpha]</math>  
Щоб застосувати цю функцію до пари списків, необхідно підставити конкретний тип <math>T</math> замість змінної <math>\alpha</math> так, щоб отриманий тип функції відповідав типам аргументів.  

В ''імпредикативній'' системі <math>T</math> може бути будь-яким типом, включаючи тип, який сам є поліморфним; таким чином, <math>\mathsf{append}</math> можна застосовувати до пар списків із елементами будь-якого типу — навіть до списків поліморфних функцій, таких як сама <math>\mathsf{append}</math>.  
Поліморфізм у мові ML є предикативним.{{citation needed|date=лютий 2019}} Це тому, що предикативність разом з іншими обмеженнями робить [[Система типізації|систему типів]] настільки простою, що повне [[Вивід типів|виведення типів]] завжди можливе.

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

=== Поліморфізм вищого рангу ===
Деякі системи типів підтримують імпредикативний конструктор функційного типу, навіть якщо інші конструктори типів залишаються предикативними. Наприклад, тип <math>(\forall \alpha. \alpha \rightarrow \alpha) \rightarrow T</math> дозволений у системі, яка підтримує поліморфізм вищого рангу, навіть якщо тип <math>[\forall \alpha. \alpha \rightarrow \alpha]</math> може бути недоступним.<ref>{{cite web |author1=Kwang Yul Seo |title=Kwang's Haskell Blog - Higher rank polymorphism |url=https://kseo.github.io/posts/2016-12-27-higher-rank-polymorphism.html |website=kseo.github.io |access-date=30 вересня 2022}}</ref>

Тип вважається типом рангу ''k'' (для деякого цілого числа ''k''), якщо жоден шлях від його кореня до квантора <math>\forall</math> не проходить зліва від ''k'' або більше стрілок, якщо тип зображений як дерево.<ref name="TAPL" />{{rp|359}} Система типів підтримує поліморфізм рангу ''k'', якщо вона дозволяє типи з рангом, що не перевищує ''k''. Наприклад, система типів, яка підтримує поліморфізм рангу 2, дозволяє тип <math>(\forall \alpha. \alpha \rightarrow \alpha) \rightarrow T</math>, але не <math>((\forall \alpha. \alpha \rightarrow \alpha) \rightarrow T) \rightarrow T</math>. Система типів, яка допускає типи будь-якого рангу, називається "ранг-''n'' поліморфною".

[[Вивід типів]] для поліморфізму рангу 2 є вирішуваним, але для рангів 3 і вище — ні.<ref>{{cite book |last1=Kfoury |first1=A. J. |last2=Wells |first2=J. B. |title=Proceedings of the 26th ACM SIGPLAN-SIGACT [[Symposium on Principles of Programming Languages]] |chapter=Principality and decidable type inference for finite-rank intersection types |date=1 січня 1999 |pages=161–174 |doi=10.1145/292540.292556 |publisher=Association for Computing Machinery|isbn=1581130953 |s2cid=14183560 |doi-access=free }}</ref><ref name="TAPL" />{{rp|359}}

=== Імпредикативний поліморфізм ===
''Імпредикативний поліморфізм'' (також відомий як ''поліморфізм першого класу'') є найпотужнішою формою параметричного поліморфізму.<ref name="TAPL" />{{rp|340}} У [[формальна логіка|формальній логіці]] визначення називається [[імпредикативність|імпредикативним]], якщо воно є самореференційним; у теорії типів це стосується можливості, щоб тип знаходився в області дії квантора, який його містить. Це дозволяє підстановку будь-якої змінної типу будь-яким типом, включно з поліморфними типами. Прикладом системи, яка підтримує повну імпредикативність, є [[System F]], що дозволяє підстановку <math>\forall \alpha. \alpha \to \alpha</math> для будь-якого типу, включно із самим собою.

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

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

== Примітки ==
{{reflist|2|refs=
<ref name="Strachey 1967">{{citation|first=Christopher|last=Strachey|author-link=Christopher Strachey|year=1967|title=Fundamental Concepts in Programming Languages|type=Lecture notes|publisher=International Summer School in Computer Programming|location=Copenhagen|title-link=Fundamental Concepts in Programming Languages}}. Перевидано у: {{cite journal |last1=Strachey |first1=Christopher |title=Fundamental Concepts in Programming Languages |journal=Higher-Order and Symbolic Computation |date=1 квітня 2000 |volume=13 |issue=1 |pages=11–49 |doi=10.1023/A:1010000313106 |s2cid=14124601 |url=https://doi.org/10.1023/A:1010000313106 |language=en |issn=1573-0557}}</ref>
}}

== Джерела ==
* {{citation
 | last = Hindley | first = J. Roger
 | author-link = J. Roger Hindley
 | year = 1969
 | title = The principal type scheme of an object in combinatory logic
 | journal = [[Transactions of the American Mathematical Society]]
 | volume = 146
 | pages = 29–60
 | doi = 10.2307/1995158
 | jstor = 1995158
 | mr = 0253905
}}.
* {{cite conference
 | first = Jean-Yves | last = Girard | author-link = Jean-Yves Girard
 | title = 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
 | series = Studies in Logic and the Foundations of Mathematics | book-title = Proceedings of the Second Scandinavian Logic Symposium
 | year = 1971
 | volume = 63 | location = Amsterdam
 | pages = 63–92
 | language = fr
 | doi = 10.1016/S0049-237X(08)70843-7
 | isbn = 9780720422597 }}
* {{citation
 | last = Girard | first = Jean-Yves
 | author-link = Jean-Yves Girard 
 | year = 1972
 | title = Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur
 | type = Ph.D. thesis
 | publisher = Université Paris 7
 | language = fr
}}.
* {{citation
 | last = Reynolds | first = John C.
 | author-link = John C. Reynolds
 | year = 1974
 | title = Towards a Theory of Type Structure
 | journal = Colloque Sur la Programmation
 | location = Paris
 | series = [[Lecture Notes in Computer Science]]
 | volume = 19
 | pages = 408–425
 | doi = 10.1007/3-540-06859-7_148
 | isbn = 978-3-540-06859-4
 | url = https://figshare.com/articles/journal_contribution/6611015
 }}.
* {{cite journal
 | last = Milner | first = Robin
 | author-link = Робін Мілнер
 | year = 1978
 | title = A Theory of Type Polymorphism in Programming
 | journal = [[Journal of Computer and System Sciences]]
 | volume = 17
 | issue = 3
 | pages = 348–375
 | doi = 10.1016/0022-0000(78)90014-4
 | s2cid = 388583
 | url = https://www.pure.ed.ac.uk/ws/files/15143545/1_s2.0_0022000078900144_main.pdf
}}
* {{cite journal|last1 = Cardelli|first1=Luca|author-link1=Luca Cardelli|last2=Wegner|first2=Peter|author-link2=Peter Wegner|title = On Understanding Types, Data Abstraction, and Polymorphism|url=http://lucacardelli.name/Papers/OnUnderstanding.A4.pdf|journal = [[ACM Computing Surveys]]|date = грудень 1985| volume = 17|issue=4|issn = 0360-0300|pages = 471–523|doi = 10.1145/6041.6042|citeseerx=10.1.1.117.695|s2cid=2921816 }}
* {{cite book|first=Benjamin C.|last=Pierce|author-link=Benjamin C. Pierce|year=2002|title=Types and Programming Languages|publisher=MIT Press|isbn=978-0-262-16209-8 }}

{{Типи даних}}

<!--Категорії-->
[[Категорія:Теорія типів]]