In the area of
mathematical logic
Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
and
computer science
Computer science is the study of computation, information, and automation. Computer science spans Theoretical computer science, theoretical disciplines (such as algorithms, theory of computation, and information theory) to Applied science, ...
known as
type theory
In mathematics and theoretical computer science, a type theory is the formal presentation of a specific type system. Type theory is the academic study of type systems.
Some type theories serve as alternatives to set theory as a foundation of ...
, a type constructor is a feature of a typed
formal language
In logic, mathematics, computer science, and linguistics, a formal language is a set of strings whose symbols are taken from a set called "alphabet".
The alphabet of a formal language consists of symbols that concatenate into strings (also c ...
that builds new types from old ones.
Basic types are considered to be built using
nullary
In logic
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the study of deductively valid inferences or logical truths. It examines how conclusions follow from premises based on the ...
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 produ ...
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 return ...
s, power types and
list types. New types can be defined by recursively composing type constructors.
For example,
simply typed lambda calculus
The simply typed lambda calculus (), a form
of type theory, is a typed interpretation of the lambda calculus with only one type constructor () that builds function types. It is the canonical and simplest example of a typed lambda calculus. The ...
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
In mathematics and computer science, currying is the technique of translating a function that takes multiple arguments into a sequence of families of functions, each taking a single argument.
In the prototypical example, one begins with a functi ...
.
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ω.
Some
functional programming languages make explicit use of type constructors. A notable example is
Haskell
Haskell () is a general-purpose, statically typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research, and industrial applications, Haskell pioneered several programming language ...
, in which all
data type declarations are considered to declare type constructors, and basic types (or nullary type constructors) are called type constants.
[
] Type constructors may also be considered as
parametric polymorphic data types.
See also
*
Kind (type theory)
*
Algebraic data type
In computer programming, especially functional programming and type theory, an algebraic data type (ADT) is a kind of composite data type, i.e., a data type formed by combining other types.
Two common classes of algebraic types are product ty ...
*
Recursive data type
References
* , chapter 29, "Type Operators and Kinding"
*
P.T. Johnstone, ''Sketches of an Elephant'', p. 940
{{Data types
Type theory