Type constructor
Encyclopedia
In the area of mathematical logic
and computer science
known as type theory
, a type constructor is a feature of a typed formal language
that builds new types from old. Typical type constructors encountered are product type
s, function type
s, power types and list types. Basic types are considered nullary type constructors. New types can be defined by recursively composing type constructors.
For example, simply typed lambda calculus
can be seen as a language with a single 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 kind
s.
Instituting a simply typed lambda calculus over the type operators results in more than just a formalization of type constructors though. Higher-order type operators become possible. (See Kind (type theory)#Examples for some examples.) Type operators correspond to the 2nd axis in the lambda cube
, leading to the simply typed lambda-calculus with type operators, λω; while this is not so well known, combining type operators with polymorphic lambda calculus (system F
) yields system F-omega.
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
and computer science
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
known as type theory
Type theory
In mathematics, logic and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general...
, a type constructor is a feature of a typed formal language
Formal language
A formal language is a set of words—that is, finite strings of letters, symbols, or tokens that are defined in the language. The set from which these letters are taken is the alphabet over which the language is defined. A formal language is often defined by means of a formal grammar...
that builds new types from old. Typical type constructors encountered are product type
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 product. An instance of a product type retains the fixed...
s, function type
Function type
In computer science, a function type is the type of a variable or parameter to which a function has or can be assigned or the result type of a higher-order function returning a function....
s, power types and list types. Basic types are considered nullary type constructors. New types can be defined by recursively composing type constructors.
For example, simply typed lambda calculus
Simply typed lambda calculus
The simply typed lambda calculus , a formof 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 calculus...
can be seen as a language with a single type constructor—the function type constructor. Product types can generally be considered "built-in" in typed lambda calculi
Typed lambda calculus
A typed lambda calculus is a typed formalism that uses the lambda-symbol to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered...
via currying
Currying
In mathematics and computer science, currying is the technique of transforming a function that takes multiple arguments in such a way that it can be called as a chain of functions each with a single argument...
.
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 kind
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...
s.
Instituting a simply typed lambda calculus over the type operators results in more than just a formalization of type constructors though. Higher-order type operators become possible. (See Kind (type theory)#Examples for some examples.) Type operators correspond to the 2nd axis in the lambda cube
Lambda cube
In mathematical logic and type theory, the λ-cube is a framework for exploring the axes of refinement in Coquand's calculus of constructions, starting from the simply typed lambda calculus as the vertex of a cube placed at the origin, and the calculus of constructions as its diametrically opposite...
, leading to the simply typed lambda-calculus with type operators, λω; while this is not so well known, combining type operators with polymorphic lambda calculus (system F
System F
System F, also known as the polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types...
) yields system F-omega.