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:
“This immediate dependence of language upon nature, this conversion of an outward phenomenon into a type of somewhat in human life, never loses its power to affect us. It is this which gives that piquancy to the conversation of a strong-natured farmer or backwoodsman, which all men relish.”
—Ralph Waldo Emerson (18031882)
“Dont confuse hypothesis and theory. The former is a possible explanation; the latter, the correct one. The establishment of theory is the very purpose of science.”
—Martin H. Fischer (18791962)