This articledoes notcite anysources. Please helpimprove this article byadding citations to reliable sources. Unsourced material may be challenged andremoved. Find sources: "Type variable" – news ·newspapers ·books ·scholar ·JSTOR(January 2025) (Learn how and when to remove this message)

Intype theory andprogramming languages, atype variable is amathematical variable ranging overtypes. Even in programming languages that allowmutable variables, a type variable remains an abstraction, in the sense that it does not correspond to some memory locations.

Programming languages that supportparametric polymorphism make use ofuniversally quantified type variables. Languages that supportexistential types make use ofexistentially quantified type variables. For example, the followingOCaml code defines a polymorphicidentity function that has a universally quantified type, which is printed by the interpreter on the second line:

#letidx=x;;valid:'a->'a=<fun>

In mathematical notation, the type of the functionid is${\displaystyle \mathrm{\forall }a.a\to a}$, where${\displaystyle a}$ is a type variable.

• System F

${\displaystyle \mathrm{\Gamma }⊢}$

Thisprogramming language theory ortype theory-related article is astub. You can help Wikipedia byadding missing information.

• v
• t
• e

• Programming language theory stubs
• Type theory
• Functional programming
• Dependently typed programming

• Articles lacking sources from January 2025
• All articles lacking sources
• All stub articles