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 simply returns its