Inprogramming languages andtype 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 polymorphicfunctions anddata types are sometimes calledgeneric functions andgeneric datatypes, respectively, and they form the basis ofgeneric programming.

Parametric polymorphism may be contrasted withad hoc polymorphism. Parametrically polymorphic definitions areuniform: 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.

The usual theoretical device for studying parametric polymorphism issystem F, which extendssimply typed lambda calculus withquantification over types.

It is possible to write functions that do not depend on the types of their arguments. For example, theidentity function${\displaystyle \mathsf{i}\mathsf{d}(x)=x}$ simply returns its argument unmodified. This naturally gives rise to a family of potential types, such as${\displaystyle \mathsf{I}\mathsf{n}\mathsf{t}\to \mathsf{I}\mathsf{n}\mathsf{t}}$,${\displaystyle \mathsf{B}\mathsf{o}\mathsf{o}\mathsf{l}\to \mathsf{B}\mathsf{o}\mathsf{o}\mathsf{l}}$,${\displaystyle \mathsf{S}\mathsf{t}\mathsf{r}\mathsf{i}\mathsf{n}\mathsf{g}\to \mathsf{S}\mathsf{t}\mathsf{r}\mathsf{i}\mathsf{n}\mathsf{g}}$, and so on. Parametric polymorphism allows${\displaystyle \mathsf{i}\mathsf{d}}$ to be given a single,most general type by introducing auniversally quantifiedtype variable:

${\displaystyle \mathsf{i}\mathsf{d}:\mathrm{\forall }\alpha .\alpha \to \alpha }$

The polymorphic definition can then beinstantiated 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{a}\mathsf{p}\mathsf{p}\mathsf{e}\mathsf{n}\mathsf{d}}$ function thatconcatenates twolists does not inspect the elements of the list, only the list structure itself. Therefore,${\displaystyle \mathsf{a}\mathsf{p}\mathsf{p}\mathsf{e}\mathsf{n}\mathsf{d}}$ can be given a similar family of types, such as${\displaystyle [\mathsf{I}\mathsf{n}\mathsf{t}]\times [\mathsf{I}\mathsf{n}\mathsf{t}]\to [\mathsf{I}\mathsf{n}\mathsf{t}]}$,${\displaystyle [\mathsf{B}\mathsf{o}\mathsf{o}\mathsf{l}]\times [\mathsf{B}\mathsf{o}\mathsf{o}\mathsf{l}]\to [\mathsf{B}\mathsf{o}\mathsf{o}\mathsf{l}]}$, and so on, where${\displaystyle [T]}$ denotes a list of elements of type${\displaystyle T}$. The most general type is therefore

${\displaystyle \mathsf{a}\mathsf{p}\mathsf{p}\mathsf{e}\mathsf{n}\mathsf{d}:\mathrm{\forall }\alpha .[\alpha ]\times [\alpha ]\to [\alpha ]}$

which can be instantiated to any type in the family.

Parametrically polymorphic functions like${\displaystyle \mathsf{i}\mathsf{d}}$ and${\displaystyle \mathsf{a}\mathsf{p}\mathsf{p}\mathsf{e}\mathsf{n}\mathsf{d}}$ are said to beparameterized over an arbitrary type${\displaystyle \alpha }$.^[4] Both${\displaystyle \mathsf{i}\mathsf{d}}$ and${\displaystyle \mathsf{a}\mathsf{p}\mathsf{p}\mathsf{e}\mathsf{n}\mathsf{d}}$ are parameterized over a single type, but functions may be parameterized over arbitrarily many types. For example, the${\displaystyle \mathsf{f}\mathsf{s}\mathsf{t}}$ and${\displaystyle \mathsf{s}\mathsf{n}\mathsf{d}}$ functions that return the first and second elements of apair, respectively, can be given the following types:

In the expression${\displaystyle \mathsf{f}\mathsf{s}\mathsf{t}((3,\mathsf{t}\mathsf{r}\mathsf{u}\mathsf{e}))}$,${\displaystyle \alpha }$ is instantiated to${\displaystyle \mathsf{I}\mathsf{n}\mathsf{t}}$ and${\displaystyle \beta }$ is instantiated to${\displaystyle \mathsf{B}\mathsf{o}\mathsf{o}\mathsf{l}}$ in the call to${\displaystyle \mathsf{f}\mathsf{s}\mathsf{t}}$, so the type of the overall expression is${\displaystyle \mathsf{I}\mathsf{n}\mathsf{t}}$.

Thesyntax used to introduce parametric polymorphism varies significantly between programming languages. For example, in some programming languages, such asHaskell, the${\displaystyle \mathrm{\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'scall sites.

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

In the 1980s, Leivant introduced a stratified (i.e. predicative) version of Girard and Reynold'ssystem F. Leivant's approach is based on a notion of rank of the quantifiers, which measures their nesting depth inside functionconstructors.^[7] 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 therunSTmonad, which effectively simulates atype and effect system,^[8] with "isolated regions of imperative programming". At type level, state isolation essentially stems from the deeper, rank-2 quantification over state inrunST. (This is not enough to formally describe the runtime semantics ofrunST. For the latter, one needs some additional ingredients likeseparation logic.^[9])

A type is said to be of rankk (for some fixed integerk) if no path from its root to a${\displaystyle \mathrm{\forall }}$ quantifier passes to the left ofk or more arrows, when the type is drawn as a tree.^[1]: 359 A type system is said to support rank-k polymorphism if it admits types with rank less than or equal tok. For example, a type system that supports rank-2 polymorphism would allow${\displaystyle (\mathrm{\forall }\alpha .\alpha \to \alpha )\to T}$ but not${\displaystyle ((\mathrm{\forall }\alpha .\alpha \to \alpha )\to T)\to T}$. A type system that admits types of arbitrary rank is said to be "rank-n polymorphic".

(This notion of rank is a different from howquantifier rank is defined in classical logic because here it measures nesting depth relative to a non-quantifierconnective, whereas in classical logic non-quantifier connectives do not increase the rank of quantifiers nested under them, but other quantifiers do.)

This sectionneeds additional citations forverification. Please helpimprove this article byadding citations to reliable sources in this section. Unsourced material may be challenged and removed.(February 2019) (Learn how and when to remove this message)

In apredicative type system (also known as aprenex polymorphic system), type variables may not be instantiated with polymorphic types.^{[1]: 359–360} Predicative type theories includeMartin-Löf type theory andNuprl. 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 astype schemas to distinguish them from ordinary (monomorphic) types, which are sometimes calledmonotypes.

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${\displaystyle \mathsf{a}\mathsf{p}\mathsf{p}\mathsf{e}\mathsf{n}\mathsf{d}}$ function described above, which has the following type:

${\displaystyle \mathsf{a}\mathsf{p}\mathsf{p}\mathsf{e}\mathsf{n}\mathsf{d}:\mathrm{\forall }\alpha .[\alpha ]\times [\alpha ]\to [\alpha ]}$

In order to apply this function to a pair of lists, a concrete type${\displaystyle T}$ must be substituted for the variable${\displaystyle \alpha }$ such that the resulting function type is consistent with the types of the arguments. In animpredicative system,${\displaystyle T}$ may be any type whatsoever, including a type that is itself polymorphic; thus${\displaystyle \mathsf{a}\mathsf{p}\mathsf{p}\mathsf{e}\mathsf{n}\mathsf{d}}$ can be applied to pairs of lists with elements of any type—even to lists of polymorphic functions such as${\displaystyle \mathsf{a}\mathsf{p}\mathsf{p}\mathsf{e}\mathsf{n}\mathsf{d}}$ itself.Polymorphism in the language ML is predicative.^[10] This is because predicativity, together with other restrictions, makes thetype system simple enough that fulltype inference is always possible.

As a practical example,OCaml (a descendant or dialect ofML) 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${\displaystyle (\mathrm{\forall }\alpha .\alpha \to \alpha )\to T}$ is permitted in a system that supports higher-rank polymorphism, even though${\displaystyle [\mathrm{\forall }\alpha .\alpha \to \alpha ]}$ may not be.^[11]

Type inference for rank-2 polymorphism is decidable, but for rank-3 and above, it is not.^{[12][1]: 359}

Impredicative polymorphism (also calledfirst-class polymorphism) is the most powerful form of parametric polymorphism.^[1]: 340 Informal logic, a definition is said to beimpredicative 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 isSystem F, which allows instantiating${\displaystyle \mathrm{\forall }\alpha .\alpha \to \alpha }$ at any type, including itself.

Intype theory, the most frequently studied impredicativetyped λ-calculi are based on those of thelambda cube, especially System F.

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 types. 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.^[13]

In 1985,Luca Cardelli andPeter Wegner recognized the advantages of allowingbounds on the type parameters.^[14] 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. InStandard 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. InHaskell, bounding is achieved by requiring types to belong to atype class; thus the same function has the type$\mathrm{E}\mathrm{q}\alpha \Rightarrow \alpha \to \left[\alpha \right]\to \mathrm{B}\mathrm{o}\mathrm{o}\mathrm{l}$ in Haskell. In most object-oriented programming languages that support parametric polymorphism, parameters can be constrained to besubtypes of a given type (see the articlesSubtype polymorphism andGeneric programming).

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

• 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,19, Paris: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.

• Generic programming
• Polymorphism (computer science)
• Type theory

• Articles with short description
• Short description matches Wikidata
• Articles needing additional references from February 2019
• All articles needing additional references
• CS1 French-language sources (fr)