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. The usual theoretical device for studying parametric polymorphism is system F, which extends simply typed lambda calculus with quantification over types.
Basic definition It is possible to write functions that do not depend on the types of their arguments. For example, the identity function i d ( x ) = x {\displaystyle {\mathsf {id}}(x)=x} simply returns its argument unmodified. This naturally gives rise to a family of potential types, such as I n t → I n t {\displaystyle {\mathsf {Int}}\to {\mathsf {Int}}} , B o o l → B o o l {\displaystyle {\mathsf {Bool}}\to {\mathsf {Bool}}} , S t r i n g → S t r i n g {\displaystyle {\mathsf {String}}\to {\mathsf {String}}} , and so on. Parametric polymorphism allows i d {\displaystyle {\mathsf {id}}} to be given a single, most general type by introducing a universally quantified type variable:
i d : ∀ α . α → α {\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. The identity function is a particularly extreme example, but many other functions also benefit from parametric polymorphism. For example, an a p p e n d {\displaystyle {\mathsf {append}}} function that concatenates two lists does not inspect the elements of the list, only the list structure itself. Therefore, a p p e n d {\displaystyle {\mathsf {append}}} can be given a similar family of types, such as [ I n t ] × [ I n t ] → [ I n t ] {\displaystyle [{\mathsf {Int}}]\times [{\mathsf {Int}}]\to [{\mathsf {Int}}]} , [ B o o l ] × [ B o o l ] → [ B o o l ] {\displaystyle [{\mathsf {Bool}}]\times [{\mathsf {Bool}}]\to [{\mathsf {Bool}}]} , and so on, where [ T ] {\displaystyle [T]} denotes a list of elements of type T {\displaystyle T} . The most general type is therefore
a p p e n d : ∀ α . [ α ] × [ α ] → [ α ] {\displaystyle {\mathsf {append}}:\forall \alpha .[\alpha ]\times [\alpha ]\to [\alpha ]}
… excerpt ends here. Continue reading the full article.
