type theory In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a foundat ...

and

programming language A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language. The description of a programming ...

s, a type variable is a

mathematical variable In mathematics, a variable (from Latin language, Latin ''wikt:variabilis, variabilis'', "changeable") is a Mathematical symbol, symbol that represents a mathematical object. A variable may represent a number, a Vector (mathematics), vector, a Mat ...

ranging over types. Even in programming languages that allow mutable variables, a type variable remains an abstraction, in the sense that it does not correspond to some memory locations.

Programming language A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language. The description of a programming ...

s that support parametric polymorphism make use of

universally quantified In mathematical logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as "given any" or "for all". It expresses that a predicate can be satisfied by every member of a domain of discourse. In other w ...

type variables. Languages that support

existential type In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type to every "term" (a word, phrase, or other set of symbols). Usually the terms are various constructs of a computer progra ...

s make use of

existentially quantified In predicate logic, an existential quantification is a type of quantifier, a logical constant which is interpreted as "there exists", "there is at least one", or "for some". It is usually denoted by the logical operator symbol ∃, which, whe ...

type variables. For example, the following

OCaml OCaml ( , formerly Objective Caml) is a general-purpose programming language, general-purpose, multi-paradigm programming language which extends the Caml dialect of ML (programming language), ML with object-oriented programming, object-oriented ...

code defines a polymorphic

identity function Graph of the identity function on the real numbers In mathematics, an identity function, also called an identity relation, identity map or identity transformation, is a function that always returns the value that was used as its argument, un ...

that has a universally quantified type, which is printed by the interpreter on the second line: # let id x = x;; val id : 'a -> 'a = In mathematical notation, the type of the function id is

\forall a.a \to a

, where

a

is a type variable.

See also