= Type variable
{title2=$\alpha$}
{wiki}
A <type variable> is a placeholder for a type. In a <function type> $\alpha\to\alpha$, the repeated <type variable> requires the argument and result types to agree; $\alpha\to\beta$ does not impose that agreement. A <type substitution> replacing $\alpha$ by `int` changes $\alpha\to\alpha$ to $\mathrm{int}\to\mathrm{int}$ everywhere within that instance.
For the <identity function> written as the <lambda abstraction> $\lambda x.x$, assume $x:\alpha$ in the body. Looking up $x$ gives result type $\alpha$, so the abstraction rule gives $\lambda x.x:\alpha\to\alpha$. In the pure <Hindley-Milner type system>, `let identity = λx.x in ...` gives `identity` the <type scheme> $\forall\alpha.\alpha\to\alpha$ by <let polymorphism>. Each use receives fresh <type variables>: `identity 3` chooses `int` for its instance, and `identity true` chooses `bool` for a separate instance. These choices do not change the original <type scheme>.
\Image[/polymorphic-identity-instantiation.png]
{title=Independent type instantiations of a let-bound identity function}
{description=The <type scheme> stays general while two uses receive different <type substitutions>. Each use preserves the equality of its own argument and result types.}
For example, `let identity = λx.x in let a = identity 3 in identity true` is valid and has type `bool`. By contrast, `(λf. let a = f 3 in f true) (λx.x)` is rejected by the <Hindley-Milner type system>: the <lambda abstraction> binds `f` to one monomorphic <function type>. The first call requires its argument type to be `int`, and the second requires that same type to be `bool`. Naming the first result with `let a` does not generalize `f`. The distinction makes reusable code possible while keeping the assumptions about a supplied argument consistent.
// Target: computer-science.bigb
Back to article page
