Lukas' Notes

type-theory

Definition

Type Variable

A type variable is a variable that ranges over types.

Formally, if is a universe of types, then a type variable denotes an unspecified element of :

In polymorphic type systems, type variables mark the positions where a type may later be instantiated.