Content deleted Content added
Lexi.lambda (talk | contribs) →Rank-1 (predicative) polymorphism: Update notation to match new definition section |
86-something (talk | contribs) →History: missed 1 author |
||
| (31 intermediate revisions by 10 users not shown) | |||
Line 1:
{{Short description|Basis of generic programming}}
{{polymorphism}}
In [[programming language]]s and [[type theory]], '''parametric polymorphism''' allows a single piece of code to be given a "generic" type, using variables in place of actual types, and then instantiated with particular types as needed.<ref name="TAPL" />{{rp|340}} Parametrically polymorphic
Parametric polymorphism may be contrasted with [[ad hoc polymorphism]]. Parametrically polymorphic definitions are ''uniform'': they behave identically regardless of the type they are instantiated at.<ref name="TAPL" />{{rp|340}}<ref name="Strachey 1967" />{{rp|37}} In contrast, ad hoc polymorphic definitions are given a distinct definition for each type. Thus, ad hoc polymorphism can generally only support a limited number of such distinct types, since a separate implementation has to be provided for each type.
The usual theoretical device for studying paramedic polymorphism is [[system F]], which extends [[simply typed lambda calculus]] with [[Quantifier (logic)|quantification]] over types.
== Basic definition ==
Line 13 ⟶ 15:
The polymorphic definition can then be ''instantiated'' by substituting any concrete type for <math>\alpha</math>, yielding the full family of potential types.<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 October 2022}}</ref>
The identity function is a particularly extreme example, but many other functions also benefit from parametric polymorphism. For example, an <math>\mathsf{append}</math> function that [[append|concatenate]]s two [[linked list|lists]] does not inspect the elements of the list, only the list structure itself. Therefore, <math>\mathsf{append}</math> can be given a similar family of types, such as <math>
:<math>\mathsf{append} : \forall \alpha. [\alpha]
which can be instantiated to any type in the family.
Parametrically polymorphic functions like <math>\mathsf{id}</math> and <math>\mathsf{append}</math> are said to be ''parameterized over'' an arbitrary type <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 October 2022 |archive-date=1 October 2022 |archive-url=https://web.archive.org/web/20221001000858/https://smlhelp.github.io/book/concepts/poly.html |url-status=dead }}</ref> Both <math>\mathsf{id}</math> and <math>\mathsf{append}</math> are parameterized over a single type, but functions may be parameterized over arbitrarily many types. For example, the <math>\mathsf{fst}</math> and <math>\mathsf{snd}</math> functions that return the first and second elements of a [[product type|pair]], respectively, can be given the following types:
:<math>
\begin{aligned}
\mathsf{fst} & : \forall \alpha. \forall \beta.
\mathsf{snd} & : \forall \alpha. \forall \beta.
\end{aligned}
</math>
Line 33 ⟶ 35:
== History ==
Parametric polymorphism was first introduced to programming languages in [[ML programming language|ML]] in 1975.<ref>[[Robin Milner|Milner, R.]], Morris, L., Newey, M. "A Logic for Computable Functions with reflexive and polymorphic types", ''Proc. Conference on Proving and Improving Programs'', Arc-et-Senans (1975)</ref> Today it exists in [[Standard ML]], [[OCaml]], [[F Sharp (programming language)|F#]], [[Ada (programming language)|Ada]], [[Haskell (programming language)|Haskell]], [[Mercury (programming language)|Mercury]], [[Visual Prolog]], [[Scala (programming language)|Scala]], [[Julia (programming language)|Julia]], [[Python (programming language)|Python]], [[TypeScript]], [[C++]] and others. [[Java (programming language)|Java]], [[C Sharp (programming language)|C#]], [[Visual Basic .NET]] and [[Object Pascal|Delphi]] have each introduced "generics" for parametric polymorphism. Some implementations of type polymorphism are superficially similar to parametric polymorphism while also introducing ad hoc aspects. One example is [[C++]] [[template specialization]].
In the 1980s, Leivant introduced a stratified (i.e. predicative) version of Girard and Reynold's [[system F]]. Leivant's approach is based on a notion of rank of the quantifiers, which measures their nesting depth inside function [[Type constructor|constructor]]s.<ref>D. Leivant, Polymorphic type inference, in: Conf. Rec. 10th Ann. ACM Symp. Princ. of Prog. Langs., 1983, pp. 88–98.</ref> The ML approach is limited to rank-1 polymorphism in this perspective. Haskell has adopted higher-rank parametric polymorphism in the 1990s. For example, rank-2 parametric polymorphism is used in Haskell to define the <code>runST</code> [[Monad (functional programming)|monad]], which effectively simulates a [[Effect system|type and effect system]],<ref>E. Moggi and Amr Sabry. 2001. Monadic Encapsulation of Effects: A Revised Approach (Extended Version). J. Funct.
Program. 11, 6 (Nov. 2001), 591-627</ref> with "isolated regions of imperative programming". At type level, state isolation essentially stems from the deeper, rank-2 quantification over state in <code>runST</code>. (This is not enough to formally describe the runtime semantics of <code>runST</code>. For the latter, one needs some additional ingredients like [[separation logic]].<ref>Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, Lars Birkedal, "A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST", POPL 2018</ref>)
== Predicativity, impredicativity, and higher-rank polymorphism ==
A type is said to be of rank ''k'' (for some fixed integer ''k'') if no path from its root to a <math>\forall</math> quantifier passes to the left of ''k'' or more arrows, when the type is drawn as a tree.<ref name="TAPL" />{{rp|359}} A type system is said to support rank-''k'' polymorphism if it admits types with rank less than or equal to ''k''. For example, a type system that supports rank-2 polymorphism would allow <math>(\forall \alpha. \alpha \rightarrow \alpha) \rightarrow T</math> but not <math>((\forall \alpha. \alpha \rightarrow \alpha) \rightarrow T) \rightarrow T</math>. A type system that admits types of arbitrary rank is said to be "rank-''n'' polymorphic".▼
(This notion of rank is a different from how [[quantifier rank]] is defined in classical logic because here it measures nesting depth relative to a non-quantifier [[Logical connective|connective]], whereas in classical logic non-quantifier connectives do not increase the rank of quantifiers nested under them, but other quantifiers do.)
=== Rank-1 (predicative) polymorphism ===
{{refimprove section|date=February 2019}}
In a ''[[Impredicativity|predicative]]'' type system (also known as a ''[[prenex]] polymorphic'' system), type variables may not be instantiated with polymorphic types.<ref name="TAPL">{{cite book|author1=[[Benjamin C. Pierce
This restriction makes the distinction between polymorphic and non-polymorphic types very important; thus in predicative systems polymorphic types are sometimes referred to as ''type schemas'' to distinguish them from ordinary (monomorphic) types, which are sometimes called ''monotypes''.
A consequence of predicativity is that all types can be written in a form that places all quantifiers at the outermost (prenex) position. For example, consider the <math>\mathsf{append}</math> function described above, which has the following type:
:<math>\mathsf{append} : \forall \alpha. [\alpha]
In order to apply this function to a pair of lists, a concrete type <math>T</math> must be substituted for the variable <math>\alpha</math> such that the resulting function type is consistent with the types of the arguments. In an ''impredicative'' system, <math>T</math> may be any type whatsoever, including a type that is itself polymorphic; thus <math>\mathsf{append}</math> can be applied to pairs of lists with elements of any type—even to lists of polymorphic functions such as <math>\mathsf{append}</math> itself.
Polymorphism in the language ML is predicative.<ref>{{
As a practical example, [[OCaml]] (a descendant or dialect of [[ML (programming language)|ML]]) performs type inference and supports impredicative polymorphism, but in some cases when impredicative polymorphism is used, the system's type inference is incomplete unless some explicit type annotations are provided by the programmer.
Line 52 ⟶ 61:
Some type systems support an impredicative function type constructor even though other type constructors remain predicative. For example, the type <math>(\forall \alpha. \alpha \rightarrow \alpha) \rightarrow T</math> is permitted in a system that supports higher-rank polymorphism, even though <math>[\forall \alpha. \alpha \rightarrow \alpha]</math> may not be.<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 September 2022}}</ref>
[[Type inference]] for rank-2 polymorphism is decidable, but for rank-3 and above, it is not.<ref>{{cite
▲A type is said to be of rank ''k'' (for some fixed integer ''k'') if no path from its root to a <math>\forall</math> quantifier passes to the left of ''k'' or more arrows, when the type is drawn as a tree.<ref name="TAPL" />{{rp|359}} A type system is said to support rank-''k'' polymorphism if it admits types with rank less than or equal to ''k''. For example, a type system that supports rank-2 polymorphism would allow <math>(\forall \alpha. \alpha \rightarrow \alpha) \rightarrow T</math> but not <math>((\forall \alpha. \alpha \rightarrow \alpha) \rightarrow T) \rightarrow T</math>. A type system that admits types of arbitrary rank is said to be "rank-''n'' polymorphic".
▲[[Type inference]] for rank-2 polymorphism is decidable, but for rank-3 and above, it is not.<ref>{{cite journal |last1=Kfoury |first1=A. J. |last2=Wells |first2=J. B. |title=Principality and decidable type inference for finite-rank intersection types |journal=Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages |date=1 January 1999 |pages=161–174 |doi=10.1145/292540.292556 |url=https://dl.acm.org/doi/abs/10.1145/292540.292556 |publisher=Association for Computing Machinery}}</ref><ref name="TAPL" />{{rp|359}}
=== Impredicative polymorphism ===
Line 60 ⟶ 67:
In [[type theory]], the most frequently studied impredicative [[typed lambda calculus|typed λ-calculi]] are based on those of the [[lambda cube]], especially System F.
=== Generalizations of the notion of rank ===
Leivant's notion of rank can be generalized to symbols other than quantifiers with a simple, suitable substitution. For example, it can be applied to the (constructor of) [[intersection type]]s. However, the rank-based type hierarchy that results can have different properties. For instance, type inference for rank-3 and above system F remains undecidable (as detailed above), however, for intersection types, type inference is decidable for all finite ranks.<ref>{{ cite journal | journal = Theoretical Computer Science | last1 = Kfoury | first1 = A.J. | last2=Wells |first2=J.B. | title = Principality and type inference for intersection types using expansion variables | date = January 2004 | pages = 1-70 }}</ref>
== Bounded parametric polymorphism ==
{{main|Bounded quantification}}
In 1985, [[Luca Cardelli]] and [[Peter Wegner (computer scientist)|Peter Wegner]] recognized the advantages of allowing ''bounds'' on the type parameters.{{sfn|Cardelli|Wegner|1985}} Many operations require some knowledge of the data types, but can otherwise work parametrically. For example, to check whether an item is included in a list, we need to compare the items for equality. In [[Standard ML]], type parameters of the form ''’’a'' are restricted so that the equality operation is available, thus the function would have the type ''’’a'' × ''’’a'' list → bool and ''’’a'' can only be a type with defined equality. In [[Haskell (programming language)|Haskell]], bounding is achieved by requiring types to belong to a [[type class]]; thus the same function has the type <math display=inline>\mathrm{Eq} \, \alpha \, \Rightarrow \alpha \, \rightarrow \left[\alpha \right] \rightarrow \mathrm{Bool}</math> in Haskell. In most object-oriented programming languages that support parametric polymorphism, parameters can be constrained to be [[Subtyping|subtype]]s of a given type (see the articles [[Subtype polymorphism]] and
== See also ==
Line 73 ⟶ 84:
== Notes ==
{{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}}. Republished in: {{cite journal |last1=Strachey |first1=Christopher |title=Fundamental Concepts in Programming Languages |journal=Higher-Order and Symbolic Computation |date=1 April 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|url-access=subscription }}</ref>
}}
Line 121 ⟶ 132:
| doi = 10.1007/3-540-06859-7_148
| isbn = 978-3-540-06859-4
| url = https://figshare.com/articles/journal_contribution
| url-access = subscription
}}.
* {{cite journal
Line 136 ⟶ 148:
| 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 (computer scientist)|title = On Understanding Types, Data Abstraction, and Polymorphism|url=http://lucacardelli.name/Papers/OnUnderstanding.A4.pdf|journal = [[ACM Computing Surveys]]|date = December 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 }}
| |||