World Library  
Flag as Inappropriate
Email this Article

Type constructor

Article Id: WHEBN0024047271
Reproduction Date:

Title: Type constructor  
Author: World Heritage Encyclopedia
Language: English
Subject: Kind (type theory), Type theory, Process Environment Block, Rational data type, Opaque data type
Collection:
Publisher: World Heritage Encyclopedia
Publication
Date:
 

Type constructor

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.

For example, simply typed lambda calculus can be seen as a language with a single 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 *, 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.

Instituting a simply typed lambda calculus over the type operators results in more than just a formalization of type constructors though. Higher-order type operators become possible. (See Kind (type theory) for some examples.) Type operators correspond to the 2nd axis in the lambda cube, leading to the simply typed lambda-calculus with type operators, λω; while this is not so well known, combining type operators with polymorphic lambda calculus (system F) yields system F-omega.

See also

References

  • , chapter 29, "Type Operators and Kinding"
  • P.T. Johnstone, Sketches of an Elephant, p. 940
This article was sourced from Creative Commons Attribution-ShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and USA.gov, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for USA.gov and content contributors is made possible from the U.S. Congress, E-Government Act of 2002.
 
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
 
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a non-profit organization.
 


Copyright © World Library Foundation. All rights reserved. eBooks from Project Gutenberg are sponsored by the World Library Foundation,
a 501c(4) Member's Support Non-Profit Organization, and is NOT affiliated with any governmental agency or department.