- Type theory
In

mathematics ,logic andcomputer science ,**type theory**is any of severalformal systems that can serve as alternatives tonaive set theory , or the study of such formalisms in general. Inprogramming language theory , a branch ofcomputer science , "type theory" can refer to the design, analysis and study oftype system s, 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 thatGottlob Frege 's version ofnaive set theory was afflicted withRussell's paradox . This type theory 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 thelambda calculus , developed ahigher-order logic commonly called "Church's Theory of Types", in order to avoid theKleene-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 atyped lambda calculus . Today many other such calculi are in use, includingPer Martin-Löf 'sIntuitionistic type theory ,Jean-Yves Girard 'sSystem F and theCalculus of Constructions . In typed lambda calculi, types play a role similar to that of sets inset theory .**imple theory of types**The following system is Mendelson's (1997, 289–293)

**ST**. The domain of quantification is partitioned into an ascending hierarchy of types, with allindividual s assigned a type. Quantified variables range over only one type; hence the underlying logic isfirst-order logic .**ST**is "simple" (relative to the type theory of "Principia Mathematica ") primarily because all members of the domain and codomain of any relation must be of the same type.There is a lowest type, whose individuals have no members and are members of the second lowest type. Individuals of the lowest type correspond to the

urelement s of certain set theories. Each type has a next higher type, analogous to the notion of successor inPeano arithmetic . While**ST**is silent as to whether there is a maximal type, atransfinite number of types poses no difficulty. These facts, reminiscent of the Peano axioms, make it convenient and conventional to assign anatural number to each type, starting with 0 for the lowest type. But type theory does not require a prior definition of the naturals. The symbols peculiar to**ST**are primed variables and infix $in$. In any given formula, unprimed variables all have the same type, while primed variables ($x\text{'}$) range over the next higher type. Theatomic formula s of**ST**are of two forms, $x=y$ (identity) and $yin\; x\text{'}$. Theinfix symbol $in$ suggests the intended interpretation, set membership.All variables appearing in the definition of identity and in the axioms "Extensionality" and "Comprehension", range over individuals of one of two consecutive types. Only unprimed (primed) variables, ranging over the "lower" ("higher") type, can appear to the left (right) of '$in$'. The first-order formulation of

**ST**rules out quantifying over types. Hence each pair of consecutive types requires its own axiom of Extensionality and of Comprehension, which is possible if "Extensionality" and "Comprehension" below are taken as axiom schemata "ranging over" types.*

**Identity**, defined by $x=yleftrightarrowforall\; z\text{'}\; [xin\; z\text{'}leftrightarrow\; yin\; z\text{'}]$.*

**Extensionality**. Anaxiom schema . $forall\; x\; [xin\; y\text{'}\; leftrightarrow\; xin\; z\text{'}]\; ightarrow\; y\text{'}=z\text{'}$.: Let $Phi(x)$ denote any first-order formula containing the

free variable $x$.*

**Comprehension**. Anaxiom schema . $exists\; z\text{'}forall\; x\; [xin\; z\text{'}leftrightarrow\; Phi(x)]$.: "Remark". Any collection of elements of the same type may form an object of the next higher type. Comprehension is schematic with respect to $Phi(x)$ as well as to types.

*

**Infinity**. There exists a nonemptybinary relation $R$ over the individuals of the lowest type, that is irreflexive,transitive , and strongly connected: $forall\; x,y\; [x\; eq\; y\; ightarrow\; [xRyvee\; yRx]$.: "Remark". Infinity is the only true axiom of

**ST**and is entirely mathematical in nature. It asserts that $R$ is a stricttotal order , with a domain identical to its codomain. If 0 is assigned to the lowest type, the type of $R$ is 3. Infinity can be satisfied only if the (co)domain of $R$ isinfinite , thus forcing the existence of an infinite set. If relations are defined in terms ofordered pair s, this axiom requires a prior definition of ordered pair; the Kuratowski definition, adapted to**ST**, will do. The literature does not explain why the usualaxiom of infinity (there exists an inductive set) ofZFC of other set theories could not be married to**ST**.**ST**reveals how type theory can be made very similar toaxiomatic set theory . Moreover, the more elaborateontology of**ST**, grounded in what is now called the "iterative conception of set," makes for axiom (schemata) that are far simpler than those of conventional set theories, such asZFC , with simpler ontologies. Set theories whose point of departure is type theory, but whose axioms,ontology , and terminology differ from the above, includeNew Foundations andScott-Potter set theory .**History of type theory****Practical impact of type theory****Computing**The most obvious application of type theory is in constructing type checking algorithms in the semantic analysis phase of

compiler s for programming languages.Type theory is also widely in use in theories of

semantics ofnatural language . The most common construction takes the basic types $e$ and $t$ for individuals and truth-values, respectively, and defines the set of types recursively as follows:- if $a$ and $b$ are types, then so is $langle\; a,b\; angle$.
- Nothing except the basic types, and what can be constructed from them by means of the previous clause are types.

truth-values , i.e.characteristic function s of sets of entities. An expression of type $langlelangle\; e,t\; angle,t\; angle$ is a function from sets of entities to truth-values, i.e. a (characteristic function of a) set of sets. This latter type is standardly taken to be the type of natural language quantifiers, like " everybody" or " nobody" (Montague 1973, Barwise and Cooper 1981).**ocial Sciences**Gregory Bateson introduced a theory of logical types into the social sciences; his notions ofdouble bind and logical levels are based on Russell's theory of types.**Connections to constructive logic****Relation to other topics****Type system**Definitions of "type system" vary, but the following one due to

Benjamin C. Pierce roughly corresponds to the current consensus in the programming language theory community:In other words, a type system divides program values into sets called "types" — this is called a "type assignment" — and makes certain program behaviors illegal on the basis of the types that are thus assigned. For example, a type system may classify the value "hello" as a string and the value 5 as a

number , and prohibit the programmer from adding "hello" to 5 based on that type assignment. In this type system, the programwould be illegal. Hence, any program permitted by the type system would be provably free from the erroneous behavior of adding strings and numbers.

The design and implementation of type systems is a topic nearly as broad as the topic of programming languages itself. In fact, type theory proponents commonly proclaim that the design of type systems is the very essence of programming language design: "Design the type system correctly, and the language will design itself."

**ee also***

Type system for a more practical discussion of type systems for programming languages

*Data type for concrete types of data in programming

*Domain theory

*Category theory **References***

Alonzo Church (1940), [*http://www.jstor.org/view/00224812/di985045/98p0566g/0 A formulation of the simple theory of types*] . "The Journal of Symbolic Logic" 5(2):56-68.* Nagel, Ernest (1951), "Causal Character of Modern Physical Theory", pp. 244–268 in "Freedom and Reason", Salo W. Baron, Ernest Nagel, and Koppel B. Pinson (eds.), The Free Press. Cited on p. 759 of Jefferson Hane Weaver, "The World of Physics", ISBN 0-671-49931-9.

* Pierce, Benjamin C. (2002), "

Types and Programming Languages ", MIT Press, Cambridge, MA. ISBN 0-262-16209-1.**Further reading*** Barwise, Jon and Robin Cooper, 1981. Generalized quantifiers in English. Linguistics and Philosophy 4:159-219.

* Andrews, Peter B., 2002. " [*http://www.springeronline.com/sgw/cda/frontpage/0,11855,4-0-22-33641956-0,00.html?referer=www.springeronline.com/isbn/1-4020-0763-9 An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof*] ", 2nd ed. Kluwer Academic Publishers.

* Cardelli, Luca, 1997, " [*http://citeseer.ist.psu.edu/cardelli97type.html Type Systems,*] " in Allen B. Tucker, ed., "The Computer Science and Engineering Handbook". CRC Press: 2208-2236.

* Carl A. Gunter, "Semantics of Programming Languages: Structures and Techniques", MIT Press 1992.

*Mendelson, Elliot, 1997. "Introduction to Mathematical Logic", 4th ed. Chapman & Hall.

* Montague, Richard,1973. The proper treatment of quantification in English. In Hintikka, K. "et al.", editor, Approaches to Natural Language, pages 221--242.

* Thompson, Simon, 1991. " [*http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ Type Theory and Functional Programming*] ". Addison-Wesley. ISBN 0-201-41667-0.

* Winskel, Glynn, 1993. "The Formal Semantics of Programming Languages, An Introduction". MIT Press. ISBN 0-262-23169-7.

* Wittgenstein, Ludwig, 1922. "Tractatus Logico-Philosophicus". New York, NY: Routledge, 2005. ISBN 0-415-25562-7**External links***

Stanford Encyclopedia of Philosophy : [*http://plato.stanford.edu/entries/type-theory/ Type Theory*] " -- by Thierry Coquand.

*National Institute of Standards and Technology : [*http://www.nist.gov/dads/HTML/abstractDataType.html Abstract data type*]

* [*http://www.cs.ucsd.edu/users/goguen/ps/beatcs-adj.ps.gz A summary paper on the formal basis of ADTs, relationship to category theory, and list of good references*] . Pages 3-4 appear relevant. Reference number [6] looks good, but it may not be available online.

* Constable, Robert L., 2002, " [*http://www.nuprl.org/documents/Constable/NaiveTypeTheoryPreface.html Naïve Computational Type Theory,*] " in H. Schwichtenberg and R. Steinbruggen (eds.), "Proof and System-Reliability": 213-259.

* The Nuprl Book: " [*http://www.cs.cornell.edu/Info/Projects/NuPrl/book/node31.html Introduction to Type Theory.*] "

*Wikimedia Foundation.
2010.*