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. Typical type constructors encountered are product types, function types, power types and list types. Basic types are considered (nullary) type constructors. New types can be defined by recursively composing type constructors. The "type" of a type constructor is called a kind. Product types can generally be considered "built-in" in typed lambda calculi via currying, even when not explicitly added. Function type constructors correspond to the 2nd axis in the lambda cube.
Se also
- system F-omega, a polymorphic type system which uses only function type constructors to recursively define new types
- algebraic data type
- recursive data type
Refereces
- P.T. Johnstone, Sketches of an Elepahnt, p. 940
This programming language theory or type theory-related article is a stub. You can help Wikipedia by expanding it. |
