In programming languages 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.^[1]: 340 Parametrically polymorphic functions and data types are sometimes called generic functions and generic datatypes, respectively, and they form the basis of generic programming.

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.^{[1]: 340 [2]: 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.

Basic definition

It is possible to write functions that do not depend on the types of their arguments. For example, the identity function ${\displaystyle {\mathsf {id}}(x)=x}$ simply returns its argument unmodified. This naturally gives rise to a family of potential types, such as ${\displaystyle {\mathsf {Int}}\to {\mathsf {Int}}}$, ${\displaystyle {\mathsf {Bool}}\to {\mathsf {Bool}}}$, ${\displaystyle {\mathsf {String}}\to {\mathsf {String}}}$, and so on. Parametric polymorphism allows ${\displaystyle {\mathsf {id}}}$ to be given a single, most general type by introducing a universally quantified type variable:

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

The polymorphic definition can then be instantiated by substituting any concrete type for ${\displaystyle \alpha }$, yielding the full family of potential types.^[3]

The identity function is a particularly extreme example, but many other functions also benefit from parametric polymorphism. For example, an ${\displaystyle {\mathsf {append}}}$ function that concatenates two lists does not inspect the elements of the list, only the list structure itself. Therefore, ${\displaystyle {\mathsf {append}}}$ can be given a similar family of types, such as ${\displaystyle (([{\mathsf {Int}}],[{\mathsf {Int}}])\to [{\mathsf {Int}}])}$, ${\displaystyle (([{\mathsf {Bool}}],[{\mathsf {Bool}}])\to [{\mathsf {Bool}}])}$, and so on, where ${\displaystyle [T]}$ denotes a list of elements of type ${\displaystyle T}$. The most general type is therefore

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

which can be instantiated to any type in the family.

Parametrically polymorphic functions like ${\displaystyle {\mathsf {id}}}$ and ${\displaystyle {\mathsf {append}}}$ are said to be parameterized over an arbitrary type ${\displaystyle \alpha }$.^[4] Both ${\displaystyle {\mathsf {id}}}$ and ${\displaystyle {\mathsf {append}}}$ are parameterized over a single type, but functions may be parameterized over arbitrarily many types. For example, the ${\displaystyle {\mathsf {fst}}}$ and ${\displaystyle {\mathsf {snd}}}$ functions that return the first and second elements of a pair, respectively, can be given the following types:

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

In the expression ${\displaystyle {\mathsf {fst}}((3,{\mathsf {true}}))}$, ${\displaystyle \alpha }$ is instantiated to ${\displaystyle {\mathsf {Int}}}$ and ${\displaystyle \beta }$ is instantiated to ${\displaystyle {\mathsf {Bool}}}$ in the call to ${\displaystyle {\mathsf {fst}}}$, so the type of the overall expression is ${\displaystyle {\mathsf {Int}}}$.

The syntax used to introduce parametric polymorphism varies significantly between programming languages. For example, in some programming languages, such as Haskell, the ${\displaystyle \forall \alpha }$ quantifier is implicit and may be omitted.^[5] Other languages require types to be instantiated explicitly at some or all of a parametrically polymorphic function's call sites.

History

Parametric polymorphism was first introduced to programming languages in ML in 1975.^[6] Today it exists in Standard ML, OCaml, F#, Ada, Haskell, Mercury, Visual Prolog, Scala, Julia, Python, TypeScript, C++ and others. Java, C#, Visual Basic .NET and 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.

Predicativity, impredicativity, and higher-rank polymorphism

Bounded parametric polymorphism

In 1985, Luca Cardelli and Peter Wegner recognized the advantages of allowing bounds on the type parameters.^[9] 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, bounding is achieved by requiring types to belong to a type class; thus the same function has the type ${\textstyle \mathrm {Eq} \,\alpha \,\Rightarrow \alpha \,\rightarrow \left[\alpha \right]\rightarrow \mathrm {Bool} }$ in Haskell. In most object-oriented programming languages that support parametric polymorphism, parameters can be constrained to be subtypes of a given type (see the articles Subtype polymorphism and Generic programming).

See also

• Parametricity
• Polymorphic recursion
• Type class#Higher-kinded polymorphism
• Trait (computer programming)

Notes

References

• 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 (in French). Vol. 63. Amsterdam. pp. 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) (in French), 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 (December 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.