Type constructor

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 ones. Basic types are considered to be built using nullary type constructors. Some type constructors take another type as an argument, e.g., the constructors for product types, function types, power types and list types. 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 kinds.

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

References

Pierce, Benjamin (2002). Types and Programming Languages. MIT Press. ISBN 0-262-16209-1. , chapter 29, "Type Operators and Kinding"
P.T. Johnstone, Sketches of an Elephant, p. 940

Data types

Uninterpreted	Bit Byte Octet Trit Tryte Word

Numeric	Bignum Complex Decimal Fixed point Floating point Double precision Extended precision Half precision Minifloat Octuple precision Quadruple precision Single precision Integer signedness Interval Rational

Text	Character String null-terminated

Pointer	Address physical virtual Reference

Composite	Algebraic data type generalized Array Associative array Class Dependent Equality Inductive List Object metaobject Option type Product Record Set Union tagged

Other	Boolean Bottom type Collection Enumerated type Exception Function type Opaque data type Recursive data type Semaphore Stream Top type Type class Unit type Void

Related topics	Abstract data type Data structure Generic Kind metaclass Parametric polymorphism Primitive data type Protocol interface Subtyping Type constructor Type conversion Type system

This article is issued from Wikipedia - version of the Friday, February 12, 2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.

Type constructor

See also

References