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. 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. 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.
id(x)=x
Int\toInt
Bool\toBool
String\toString
id
id:\forall\alpha.\alpha\to\alpha
The polymorphic definition can then be instantiated by substituting any concrete type for
\alpha
The identity function is a particularly extreme example, but many other functions also benefit from parametric polymorphism. For example, an
append
append
[Int] x [Int]\to[Int]
[Bool] x [Bool]\to[Bool]
[T]
T
append:\forall\alpha.[\alpha] x [\alpha]\to[\alpha]
which can be instantiated to any type in the family.
Parametrically polymorphic functions like
id
append
\alpha
id
append
fst
snd
\begin{aligned} fst&:\forall\alpha.\forall\beta.\alpha x \beta\to\alpha\\ snd&:\forall\alpha.\forall\beta.\alpha x \beta\to\beta \end{aligned}
In the expression
fst((3,true))
\alpha
Int
\beta
Bool
fst
Int
The syntax used to introduce parametric polymorphism varies significantly between programming languages. For example, in some programming languages, such as Haskell, the
\forall\alpha
Parametric polymorphism was first introduced to programming languages in ML in 1975.[4] 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.
In a predicative type system (also known as a prenex polymorphic system), type variables may not be instantiated with polymorphic types.[5] Predicative type theories include Martin-Löf type theory and Nuprl. This is very similar to what is called "ML-style" or "Let-polymorphism" (technically ML's Let-polymorphism has a few other syntactic restrictions).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
append
append:\forall\alpha.[\alpha] x [\alpha]\to[\alpha]
T
\alpha
T
append
append
As a practical example, OCaml (a descendant or dialect of 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.
Some type systems support an impredicative function type constructor even though other type constructors remain predicative. For example, the type
(\forall\alpha.\alpha → \alpha) → T
[\forall\alpha.\alpha → \alpha]
A type is said to be of rank k (for some fixed integer k) if no path from its root to a
\forall
(\forall\alpha.\alpha → \alpha) → T
((\forall\alpha.\alpha → \alpha) → T) → T
Type inference for rank-2 polymorphism is decidable, but for rank-3 and above, it is not.[7]
Impredicative polymorphism (also called first-class polymorphism) is the most powerful form of parametric polymorphism. In formal logic, a definition is said to be impredicative if it is self-referential; in type theory, it refers to the ability for a type to be in the domain of a quantifier it contains. This allows the instantiation of any type variable with any type, including polymorphic types. An example of a system supporting full impredicativity is System F, which allows instantiating
\forall\alpha.\alpha\to\alpha
In type theory, the most frequently studied impredicative typed λ-calculi are based on those of the lambda cube, especially System F.
See main article: Bounded quantification. In 1985, Luca Cardelli and Peter Wegner recognized the advantages of allowing bounds on the type parameters. 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 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).