In the area of
mathematical logic
Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal ...
and
computer science
Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to practical disciplines (includi ...
known as
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 fou ...
, a type constructor is a feature of a typed
formal language
In logic, mathematics, computer science, and linguistics, a formal language consists of words whose letters are taken from an alphabet and are well-formed according to a specific set of rules.
The alphabet of a formal language consists of sy ...
that builds new types from old ones.
Basic type
In computer science, primitive data types are a set of basic data types from which all other data types are constructed. Specifically it often refers to the limited set of data representations in use by a particular processor, which all compiled pr ...
s are considered to be built using
nullary
Arity () is the number of arguments or operands taken by a function, operation or relation in logic, mathematics, and computer science. In mathematics, arity may also be named ''rank'', but this word can have many other meanings in mathematics. ...
type constructors. Some type constructors take another type as an argument, e.g., the constructors for
product type
In programming languages and type theory, a product of ''types'' is another, compounded, type in a structure. The "operands" of the product are types, and the structure of a product type is determined by the fixed order of the operands in the prod ...
s,
function type In computer science and mathematical logic, a function type (or arrow type or exponential) is the type of a variable or parameter to which a function has or can be assigned, or an argument or result type of a higher-order function taking or re ...
s, power types and
list type
In computer science, a list or sequence is an abstract data type that represents a finite number of ordered values, where the same value may occur more than once. An instance of a list is a computer representation of the mathematical concept of ...
s. New types can be defined by recursively composing type constructors.
For example,
simply typed lambda calculus
The simply typed lambda calculus (\lambda^\to), a form
of type theory, is a typed interpretation of the lambda calculus with only one type constructor (\to) that builds function types. It is the canonical and simplest example of a typed lambda c ...
can be seen as a language with a single non-basic type constructor—the function type constructor. Product types can generally be considered "built-in" in
typed lambda calculi via
currying.
Abstractly, a type constructor is an ''n''-ary type operator taking as argument zero or more types, and returning another type. Making use of currying, ''n''-ary type operators can be (re)written as a sequence of applications of unary type operators. Therefore, we can view the type operators as a simply typed lambda calculus, which has only one basic type, usually denoted
, and pronounced "type", which is the type of all types in the underlying language, which are now called ''proper types'' in order to distinguish them from the types of the type operators in their own calculus, which are called ''
kinds''.
Type operators may bind type variables. For example, giving the structure of the
simply-typed λ-calculus at the type level requires binding, or higher-order, type operators. These binding type operators correspond to the 2nd axis of the
λ-cube, and type theories such as the
simply-typed λ-calculus with type operators, λ
ω. Combining type operators with the polymorphic λ-calculus (
System F
System F (also polymorphic lambda calculus or second-order lambda calculus) is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorph ...
) yields
System Fω.
See also
*
Kind (type theory) In the area of mathematical logic and computer science known as type theory, a kind is the type of a type constructor or, less commonly, the type of a higher-order type operator. A kind system is essentially a simply typed lambda calculus "one le ...
*
Algebraic data type
In computer programming, especially functional programming and type theory, an algebraic data type (ADT) is a kind of composite type, i.e., a type formed by combining other types.
Two common classes of algebraic types are product types (i.e., ...
*
Recursive data type
In computer programming languages, a recursive data type (also known as a recursively-defined, inductively-defined or inductive data type) is a data type for values that may contain other values of the same type. Data of recursive types are usuall ...
References
* , chapter 29, "Type Operators and Kinding"
*
P.T. Johnstone, ''Sketches of an Elephant'', p. 940
{{Data types
Type theory