Parametric polymorphism
Encyclopedia
In programming language
s and type theory
, parametric polymorphism is a way to make a language more expressive, while still maintaining full static type-safety. Using parametric polymorphism, a function or a data type can be written generically so that it can handle values identically without depending on their type. Such functions and data types are called generic functions and generic datatypes respectively and form the basis of generic programming
.
For example, a function
Following Christopher Strachey
, parametric polymorphism may be contrasted with ad-hoc polymorphism
, also called function overloading, in which a single polymorphic function can have a number of distinct and potentially heterogeneous implementations depending on the type of argument(s) to which it is applied. 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.
in 1976. Today it exists in Standard ML
, OCaml
, Ada
, Haskell
, Visual Prolog
and others. Java
, C#, Visual Basic .NET
and Delphi (CodeGear) have each recently 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.
The most general form of polymorphism is "higher-rank impredicative
polymorphism". Two popular restrictions of this form are restricted rank polymorphism (for example, rank-1 or prenex polymorphism) and predicative polymorphism. Together, these restrictions give "predicative prenex polymorphism", which is essentially the form of polymorphism found in ML and early versions of Haskell.
Rank-k polymorphism
Rank-n ("higher-rank") polymorphism
Impredicative polymorphism ("first class" polymorphism)
and Wegner recognized in 1985 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 subtype
s of a given type (see Subtype polymorphism
and the article on Generic programming
).
Programming language
A programming language is an artificial language designed to communicate instructions to a machine, particularly a computer. Programming languages can be used to create programs that control the behavior of a machine and/or to express algorithms precisely....
s and type theory
Type theory
In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general...
, parametric polymorphism is a way to make a language more expressive, while still maintaining full static type-safety. Using parametric polymorphism, a function or a data type can be written generically so that it can handle values identically without depending on their type. Such functions and data types are called generic functions and generic datatypes respectively and form the basis of generic programming
Generic programming
In a broad definition, generic programming is a style of computer programming in which algorithms are written in terms of to-be-specified-later types that are then instantiated when needed for specific types provided as parameters...
.
For example, a function
append that joins two lists can be constructed so that it does not care about the type of elements: it can append lists of integers, lists of real numbers, lists of strings, and so on. Let the type variable a denote the type of elements in the lists. Then append can be typed [a] × [a] → [a], where [a] denotes the type of lists with elements of type a. We say that the type of append is parameterized by a for all values of a. (Note that since there is only one type variable, the function cannot be applied to just any pair of lists: the pair, as well as the result list, must consist of the same type of elements.) For each place where append is applied, a value is decided for a.Following Christopher Strachey
Christopher Strachey
Christopher Strachey was a British computer scientist. He was one of the founders of denotational semantics, and a pioneer in programming language design...
, parametric polymorphism may be contrasted with ad-hoc polymorphism
Ad-hoc polymorphism
In programming languages, ad-hoc polymorphism is a kind of polymorphism in which polymorphic functions can be applied to arguments of different types, because a polymorphic function can denote a number of distinct and potentially heterogeneous implementations depending on the type of argument to...
, also called function overloading, in which a single polymorphic function can have a number of distinct and potentially heterogeneous implementations depending on the type of argument(s) to which it is applied. 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.
History
Parametric polymorphism was first introduced to programming languages in MLML programming language
ML is a general-purpose functional programming language developed by Robin Milner and others in the early 1970s at the University of Edinburgh, whose syntax is inspired by ISWIM...
in 1976. Today it exists in Standard ML
Standard ML
Standard ML is a general-purpose, modular, functional programming language with compile-time type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of theorem provers.SML is a modern descendant of the ML...
, OCaml
Objective Caml
OCaml , originally known as Objective Caml, is the main implementation of the Caml programming language, created by Xavier Leroy, Jérôme Vouillon, Damien Doligez, Didier Rémy and others in 1996...
, Ada
Ada (programming language)
Ada is a structured, statically typed, imperative, wide-spectrum, and object-oriented high-level computer programming language, extended from Pascal and other languages...
, Haskell
Haskell (programming language)
Haskell is a standardized, general-purpose purely functional programming language, with non-strict semantics and strong static typing. It is named after logician Haskell Curry. In Haskell, "a function is a first-class citizen" of the programming language. As a functional programming language, the...
, Visual Prolog
Visual Prolog
Visual Prolog, also formerly known as PDC Prolog and Turbo Prolog, is a strongly typed object-oriented extension of Prolog. As Turbo Prolog it was marketed by Borland, but it is now developed and marketed by the Danish firm Prolog Development Center that originally developed it...
and others. Java
Java (programming language)
Java is a programming language originally developed by James Gosling at Sun Microsystems and released in 1995 as a core component of Sun Microsystems' Java platform. The language derives much of its syntax from C and C++ but has a simpler object model and fewer low-level facilities...
, C#, Visual Basic .NET
Visual Basic .NET
Visual Basic .NET , is an object-oriented computer programming language that can be viewed as an evolution of the classic Visual Basic , which is implemented on the .NET Framework...
and Delphi (CodeGear) have each recently 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++
C++
C++ is a statically typed, free-form, multi-paradigm, compiled, general-purpose programming language. It is regarded as an intermediate-level language, as it comprises a combination of both high-level and low-level language features. It was developed by Bjarne Stroustrup starting in 1979 at Bell...
template specialization.
The most general form of polymorphism is "higher-rank impredicative
Impredicative
In mathematics and logic, impredicativity is the property of a self-referencing definition. More precisely, a definition is said to be impredicative if it invokes the set being defined, or another set which contains the thing being defined.Russell's paradox is a famous example of an impredicative...
polymorphism". Two popular restrictions of this form are restricted rank polymorphism (for example, rank-1 or prenex polymorphism) and predicative polymorphism. Together, these restrictions give "predicative prenex polymorphism", which is essentially the form of polymorphism found in ML and early versions of Haskell.
Higher-ranked polymorphism
Rank-1 (prenex) polymorphism- In a prenex polymorphic system, type variables may not be instantiated with polymorphic types. 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 is that all types can be written in a form which places all quantifiers at the outermost (prenex) position.
- For example, consider the
appendfunction described above, which has type [a] × [a] → [a]; in order to apply this function to a pair of lists, a type must be substituted for the variable a in the type of the function such that the type of the arguments matches up with the resulting function type. In an impredicative system, the type being substituted may be any type whatsoever, including a type that is itself polymorphic; thusappendcan be applied to pairs of lists with elements of any type—even to lists of polymorphic functions such asappenditself. - Polymorphism in the language ML and its close relatives is predicative. This is because predicativity, together with other restrictions, makes the type systemType systemA type system associates a type with each computed value. By examining the flow of these values, a type system attempts to ensure or prove that no type errors can occur...
simple enough that type inferenceType inferenceType inference refers to the automatic deduction of the type of an expression in a programming language. If some, but not all, type annotations are already present it is referred to as type reconstruction....
is possible. In languages where explicit type annotations are necessary when applying a polymorphic function, the predicativity restriction is less important; thus these languages are generally impredicative. Haskell manages to achieve type inference without predicativity but with a few complications.
Rank-k polymorphism
- For some fixed value k, rank-k polymorphism is a system in which a quantifier may not appear to the left of k or more arrows (when the type is drawn as a tree).
- Type inferenceType inferenceType inference refers to the automatic deduction of the type of an expression in a programming language. If some, but not all, type annotations are already present it is referred to as type reconstruction....
for rank-2 polymorphism is decidable, but reconstruction for rank-3 and above is not.
Rank-n ("higher-rank") polymorphism
- Rank-n polymorphism is polymorphism in which quantifiers may appear to the left of arbitrarily many arrows.
Predicativity and impredicativity
Predicative polymorphism- In a predicative parametric polymorphic system, a type
containing a type variable 
may not be used in such a way that 
is instantiated to a polymorphic type.
Impredicative polymorphism ("first class" polymorphism)
- Also called first-class polymorphism. Impredicative polymorphism allows the instantiation of a variable in a type
with any type, including polymorphic types, such as 
itself. - In type theoryType theoryIn mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general...
, the most frequently studied impredicative typed λ-calculiTyped lambda calculusA typed lambda calculus is a typed formalism that uses the lambda-symbol to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered...
are based on those of the lambda cubeLambda cubeIn mathematical logic and type theory, the λ-cube is a framework for exploring the axes of refinement in Coquand's calculus of constructions, starting from the simply typed lambda calculus as the vertex of a cube placed at the origin, and the calculus of constructions as its diametrically opposite...
, especially System FSystem FSystem F, also known as the polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types...
. Predicative type theories include Martin-Löf Type TheoryIntuitionistic type theoryIntuitionistic type theory, or constructive type theory, or Martin-Löf type theory or just Type Theory is a logical system and a set theory based on the principles of mathematical constructivism. Intuitionistic type theory was introduced by Per Martin-Löf, a Swedish mathematician and philosopher,...
and NuPRLNuPRLNuPRL is a higher-order proof development system developed at Cornell University. It was founded by Joseph L. Bates and Robert L. Constable in 1979 and, since then, many have contributed to the development of NuPRL....
.
Bounded parametric polymorphism
Luca CardelliLuca Cardelli
Luca Cardelli is an Italian computer scientist who is currently an Assistant Director at Microsoft Research in Cambridge, UK. Cardelli is well-known for his research in type theory and operational semantics. Among other contributions he implemented the first compiler for the functional programming...
and Wegner recognized in 1985 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
Standard ML
Standard ML is a general-purpose, modular, functional programming language with compile-time type checking and type inference. It is popular among compiler writers and programming language researchers, as well as in the development of theorem provers.SML is a modern descendant of the 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
Haskell (programming language)
Haskell is a standardized, general-purpose purely functional programming language, with non-strict semantics and strong static typing. It is named after logician Haskell Curry. In Haskell, "a function is a first-class citizen" of the programming language. As a functional programming language, the...
, bounding is achieved by requiring types to belong to a type class
Type class
In computer science, a type class is a type system construct that supports ad-hoc polymorphism. This is achieved by adding constraints to type variables in parametrically polymorphic types...
; 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 subtypeSubtype
In programming language theory, subtyping or subtype polymorphism is a form of type polymorphism in which a subtype is a datatype that is related to another datatype by some notion of substitutability, meaning that program constructs, typically subroutines or functions, written to operate on...
s of a given type (see Subtype polymorphism
Subtype polymorphism
In programming language theory, subtyping or subtype polymorphism is a form of type polymorphism in which a subtype is a datatype that is related to another datatype by some notion of substitutability, meaning that program constructs, typically subroutines or functions, written to operate on...
and the article on Generic programming
Generic programming
In a broad definition, generic programming is a style of computer programming in which algorithms are written in terms of to-be-specified-later types that are then instantiated when needed for specific types provided as parameters...
).