Type constructor

Feature of a typed formal language that builds new types from old ones

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 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  ∗ {\displaystyle *} , 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) yields System Fω.

Some functional programming languages make explicit use of type constructors. A notable example is Haskell, in which all `data` type declarations are considered to declare type constructors, and basic types (or nullary type constructors) are called type constants.[1][2] Type constructors may also be considered as parametric polymorphic data types.

## See also

[edit]

* Kind (type theory)
* Algebraic data type
* Recursive data type

## References

[edit]

1. ^ Marlow, Simon (April 2010), "4.1.2 Syntax of Types", Haskell 2010 Language Report, retrieved 15 August 2023
2. ^ "Constructor". HaskellWiki. Retrieved 15 August 2023.

* 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

* v
* t
* e

Data types

Uninterpreted|

* Bit
* Byte
* Trit
* Tryte
* Word
* Bit array

Numeric|

* Arbitrary-precision or bignum
* Complex
* Decimal
* Fixed point
* Block floating point
* Floating point
* Reduced precision
* Minifloat
* Half precision
* bfloat16
* Single precision
* Double precision
* Quadruple precision
* Octuple precision
* Extended precision
* Long double
* Integer
* signedness
* Interval
* Rational

Pointer|

* Address
* physical
* virtual
* Reference

Text|

* Character
* String
* null-terminated

Composite|

* Algebraic data type
* generalized
* Array
* Associative array
* Class
* Dependent
* Equality
* Inductive
* Intersection
* List
* Object
* metaobject
* Option type
* Product
* Record or Struct
* Refinement
* Set
* Union
* tagged

Other|

* Boolean
* Bottom type
* Collection
* Enumerated type
* Exception
* Function type
* Opaque data type
* Recursive data type
* Semaphore
* Stream
* Strongly typed identifier
* Top type
* Type class
* Empty type
* Unit type
* Void

Related
topics|

* Abstract data type
* Boxing
* Data structure
* Generic
* Kind
* metaclass
* Parametric polymorphism
* Primitive data type
* Interface
* Subtyping
* Type constructor
* Type conversion
* Type system
* Type theory
* Variable

*[v]: View this template
*[t]: Discuss this template
*[e]: Edit this template