Type Constructor

Definition

In Type Theory, a type constructor is an operation that builds new types from existing types. Type constructors take one or more types as parameters and produce a new type.

A type constructor can be viewed as a function at the type level: it maps types to types rather than values to values.

Examples

Nullary Type Constructors

Type constructors with no parameters are simply base types:

• $\mathbb{N}$: Natural numbers
• $\text{Bool}$: Boolean values

Unary Type Constructors

Type constructors taking one type parameter:

• $\text{List}(A)$: Lists of elements of type $A$
• $\text{Maybe}(A)$: Optional values of type $A$
• $\text{Tree}(A)$: Trees with nodes labeled by $A$

Binary Type Constructors

Type constructors taking two type parameters:

• $A\times B$: Product Type of $A$ and $B$
• $A+B$: Sum Type of $A$ and $B$
• $A\to B$: Function Type from $A$ to $B$

Higher-Order Type Constructors

Type constructors can themselves take type constructors as arguments. For example, a functor or monad is a higher-order type constructor.

Dependent Type Constructors

In dependently typed language, type constructors can depend on values, not just types:

• $\text{Vec}(A,n)$: Vectors of type $A$ with length $n:\mathbb{N}$
• ${\Sigma }_{x:A}B(x)$: Dependent Pair where $B$ is a type family indexed by $A$
• ${\Pi }_{x:A}B(x)$: Dependent Function Type where the codomain depends on the input

Related Concepts

• Type Theory: The formal system in which type constructors are defined
• Product Type: A fundamental binary type constructor
• Sum Type: The dual to product types
• Function Type: Functions as a type constructor
• Dependent Pair: A generalization allowing dependency on values
• Kind: The type of a type constructor