Parametric polymorphism

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.