imported>Jlwoodwa: Added {{Unreferenced}} tag

2025-01-08T00:28:03Z

New page

{{Unreferenced|date=January 2025}}
In [[type theory]] and [[programming language]]s, a '''type variable''' is a [[Variable_(mathematics)|mathematical variable]] ranging over [[data types|types]]. Even in programming languages that allow [[variable (programming)|mutable variable]]s, a type variable remains an abstraction, in the sense that it does not correspond to some memory locations.

[[Programming language]]s that support [[parametric polymorphism]] make use of [[universally quantified]] type variables. Languages that support [[existential type]]s make use of [[existentially quantified]] type variables. For example, the following [[OCaml]] code defines a polymorphic [[identity function]] that has a universally quantified type, which is printed by the interpreter on the second line:

<syntaxhighlight lang="ocaml">
# let id x = x;;
val id : 'a -> 'a = <fun>
</syntaxhighlight>

In mathematical notation, the type of the function <code>id</code> is <math>\forall a.a \to a</math>, where <math>a</math> is a type variable.

== See also ==
* [[System F]]

{{type-theory-stub}}

[[Category:Type theory]]
[[Category:Functional programming]]
[[Category:Dependently typed programming]]

Type variable - Revision history

imported>Jlwoodwa: Added {{Unreferenced}} tag