# Type constructor

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Type_constructor
> Markdown URL: https://mediated.wiki/source/Type_constructor.md
> Source: https://en.wikipedia.org/wiki/Type_constructor
> Source revision: 1170555323
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

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

In the area of [mathematical logic](/source/Mathematical_logic) and [computer science](/source/Computer_science) known as [type theory](/source/Type_theory), a **type constructor** is a feature of a typed [formal language](/source/Formal_language) that builds new types from old ones. [Basic types](/source/Basic_type) are considered to be built using [nullary](/source/Nullary) type constructors. Some type constructors take another type as an argument, e.g., the constructors for [product types](/source/Product_type), [function types](/source/Function_type), power types and [list types](/source/List_type). New types can be defined by recursively composing type constructors.

For example, [simply typed lambda calculus](/source/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](/source/Typed_lambda_calculus) via [currying](/source/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](/source/Kind_(type_theory))*.

Type operators may bind type variables. For example, giving the structure of the [simply-typed λ-calculus](/source/Simply_typed_%CE%BB-calculus) at the type level requires binding, or higher-order, type operators. These binding type operators correspond to the 2nd axis of the [λ-cube](/source/Lambda_cube), and type theories such as the [simply-typed λ-calculus](/source/Simply_typed_%CE%BB-calculus) with type operators, λω. Combining type operators with the polymorphic λ-calculus ([System F](/source/System_F)) yields [System Fω](/source/System_F-omega).

Some [functional programming languages](/source/Functional_programming) make explicit use of type constructors. A notable example is [Haskell](/source/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](/source/Parametric_polymorphism).

## See also

- [Kind (type theory)](/source/Kind_(type_theory))

- [Algebraic data type](/source/Algebraic_data_type)

- [Recursive data type](/source/Recursive_data_type)

## References

1. **[^](#cite_ref-1)** Marlow, Simon (April 2010), ["4.1.2 Syntax of Types"](https://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-650004.1.2), [*Haskell 2010 Language Report*](https://www.haskell.org/onlinereport/haskell2010/), retrieved 15 August 2023

1. **[^](#cite_ref-2)** ["Constructor"](https://wiki.haskell.org/Constructor). *HaskellWiki*. Retrieved 15 August 2023.

- Pierce, Benjamin (2002). *Types and Programming Languages*. MIT Press. [ISBN](/source/ISBN_(identifier)) [0-262-16209-1](https://en.wikipedia.org/wiki/Special:BookSources/0-262-16209-1)., chapter 29, "Type Operators and Kinding"

- [P.T. Johnstone](/source/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 Reference Address physical virtual Pointer 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 Any type Boolean Bottom type Collection Enumerated type Exception Function type Opaque data type Recursive data type Semaphore Stream Strongly typed identifier Type class Empty type Unit type Void Related topics Value 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

---
Adapted from the Wikipedia article [Type constructor](https://en.wikipedia.org/wiki/Type_constructor) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Type_constructor?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.