In the area ofmathematical logic andcomputer science known astype theory, atype constructor is a feature of a typedformal language that builds new types from old ones.Basic types are considered to be built usingnullary type constructors. Some type constructors take another type as an argument, e.g., the constructors forproduct types,function types, power types andlist 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" intyped lambda calculi viacurrying.
Abstractly, a type constructor is ann-arytype 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 calledproper types in order to distinguish them from the types of the type operators in their own calculus, which are calledkinds.
Type operators may bind type variables. For example, giving the structure of thesimply-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 thesimply-typed λ-calculus with type operators, λω. Combining type operators with the polymorphic λ-calculus (System F) yieldsSystem Fω.
Somefunctional programming languages make explicit use of type constructors. A notable example isHaskell, in which alldata 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 asparametric polymorphic data types.