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 founda ...

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 ranging over

types Type may refer to: Science and technology Computing * Typing, producing text via a keyboard, typewriter, etc. * Data type In computer science and computer programming, a data type (or simply type) is a set of possible values and a set of allo ...

. 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 In programming languages and type theory, parametric polymorphism allows a single piece of code to be given a "generic" type, using variables in place of actual types, and then instantiated with particular types as needed. Parametrically polymorph ...

make use of

universally quantified In mathematical logic, a universal quantification is a type of Quantification (logic), quantifier, a logical constant which is interpretation (logic), interpreted as "given any" or "for all". It expresses that a predicate (mathematical logic), pr ...

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 progr ...

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, ...

type variables. For example, the following

OCaml OCaml ( , formerly Objective Caml) is a general-purpose, multi-paradigm programming language Programming paradigms are a way to classify programming languages based on their features. Languages can be classified into multiple paradigms. ...

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