Parametrically polymorphic definitions are uniform: they behave identically regardless of the type they are instantiated at.
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.
It is possible to write functions that do not depend on the types of their arguments.
simply returns its argument unmodified.
This naturally gives rise to a family of potential types, such as
, yielding the full family of potential types.
denotes a list of elements of type
functions that return the first and second elements of a pair, respectively, can be given the following types: In the expression
The syntax used to introduce parametric polymorphism varies significantly between programming languages.
[5] Other languages require types to be instantiated explicitly at some or all of a parametrically polymorphic function's call sites.
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.
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.
function described above, which has the following type: In order to apply this function to a pair of lists, a concrete type
Polymorphism in the language ML is predicative.
[citation needed] This is because predicativity, together with other restrictions, makes the type system simple enough that full type inference is always possible.
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.
is permitted in a system that supports higher-rank polymorphism, even though
[7] A type is said to be of rank k (for some fixed integer k) if no path from its root to a
quantifier passes to the left of k 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 to k. For example, a type system that supports rank-2 polymorphism would allow
Type inference for rank-2 polymorphism is decidable, but for rank-3 and above, it is not.
[1]: 340 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.
In type theory, the most frequently studied impredicative typed λ-calculi are based on those of the lambda cube, especially System F. 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.
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 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).