In mathematics, logic, and computer science, type theory is any of several formal systems that can serve as alternatives to naive set theory, or the study of such formalisms in general. In programming language theory, a branch of computer science, type theory can refer to the design, analysis and study of type systems, although some computer scientists limit the term's meaning to the study of abstract formalisms such as typed λ-calculi.
Bertrand Russell invented the first type theory in response to his discovery that Gottlob Frege's version of naive set theory was afflicted with Russell's paradox. This theory of types features prominently in Whitehead and Russell's Principia Mathematica. It avoids Russell's paradox by first creating a hierarchy of types, then assigning each mathematical (and possibly other) entity to a type. Objects of a given type are built exclusively from objects of preceding types (those lower in the hierarchy), thus preventing loops.
Alonzo Church, inventor of the lambda calculus, developed a higher-order logic commonly called Church's Theory of Types, in order to avoid the Kleene–Rosser paradox afflicting the original pure lambda calculus. Church's type theory is a variant of the lambda calculus in which expressions (also called formulas or λ-terms) are classified into types, and the types of expressions restrict the ways in which they can be combined. In other words, it is a typed lambda calculus. The article Church's Type Theory in the Stanford Encyclopedia of Philosophy is devoted to this subject.
Today many other such calculi are in use, including Per Martin-Löf's Intuitionistic type theory, Jean-Yves Girard's System F and the Calculus of Constructions. In typed lambda calculi, types play a role similar to that of sets in set theory.
Read more about Type Theory: Relation To Category Theory
Famous quotes containing the words type and/or theory:
“It is not true that there is dignity in all work. Some jobs are definitely better than others.... People who have good jobs are happy, rich, and well dressed. People who have bad jobs are unhappy, poor and use meat extenders. Those who seek dignity in the type of work that compels them to help hamburgers are certain to be disappointed.”
—Fran Lebowitz (b. 1950)
“We have our little theory on all human and divine things. Poetry, the workings of genius itself, which, in all times, with one or another meaning, has been called Inspiration, and held to be mysterious and inscrutable, is no longer without its scientific exposition. The building of the lofty rhyme is like any other masonry or bricklaying: we have theories of its rise, height, decline and fall—which latter, it would seem, is now near, among all people.”
—Thomas Carlyle (1795–1881)