Type theory

In mathematics, logic, and computer science, a type theory is any of a class of formal systems, some of which can serve as alternatives to set theory as a foundation for all mathematics. In type theory, every 'term' has a 'type' and operations are restricted to terms of a certain type. In mathematics, logic, and computer science, a type theory is any of a class of formal systems, some of which can serve as alternatives to set theory as a foundation for all mathematics. In type theory, every 'term' has a 'type' and operations are restricted to terms of a certain type. Type theory is closely related to (and in some cases overlaps with) type systems, which are a programming language feature used to reduce bugs. Type theory was created to avoid paradoxes in a variety of formal logics and rewrite systems. Two well-known type theories that can serve as mathematical foundations are Alonzo Church's typed λ-calculus and Per Martin-Löf's intuitionistic type theory. Between 1902 and 1908 Bertrand Russell proposed various 'theories of type' in response to his discovery that Gottlob Frege's version of naive set theory was afflicted with Russell's paradox. By 1908 Russell arrived at a 'ramified' theory of types together with an 'axiom of reducibility' both of which featured prominently in Whitehead and Russell's Principia Mathematica published between 1910 and 1913. They attempted to resolve Russell's paradox by first creating a hierarchy of types, then assigning each concrete mathematical (and possibly other) entity to a type. Entities of a given type are built exclusively from entities of those types that are lower in their hierarchy, thus preventing an entity from being assigned to itself. In the 1920s, Leon Chwistek and Frank P. Ramsey proposed an unramified type theory, now known as the 'theory of simple types' or 'simple type theory', that collapsed the hierarchy of the types in the earlier ramified theory and as such did not require the axiom of reducibility. The common usage of 'type theory' is when those types are used with a term rewrite system. The most famous early example is Alonzo Church's simply typed lambda calculus. Church's theory of types helped the formal system avoid the Kleene–Rosser paradox that afflicted the original untyped lambda calculus. Church demonstrated that it could serve as a foundation of mathematics and it was referred to as a higher-order logic. Some other type theories include Per Martin-Löf's intuitionistic type theory, which has been the foundation used in some areas of constructive mathematics and for the proof assistant Agda. Thierry Coquand's calculus of constructions and its derivatives are the foundation used by Coq and others. The field is an area of active research, as demonstrated by homotopy type theory. In a system of type theory, each term has a type. For example, 4 {displaystyle 4} , 2 + 2 {displaystyle 2+2} , and 2 ⋅ 2 {displaystyle 2cdot 2} are all separate terms with the type n a t {displaystyle mathrm {nat} } for natural numbers. Traditionally, the term is followed by a colon and its type, such as 2 : n a t {displaystyle 2:mathrm {nat} } - this means that the number 2 {displaystyle 2} is of type n a t {displaystyle mathrm {nat} } . Type theories have explicit computation and it is encoded in rules for rewriting terms. These are called conversion rules or, if the rule only works in one direction, a reduction rule. For example, 2 + 2 {displaystyle 2+2} and 4 {displaystyle 4} are syntactically different terms, but the former reduces to the latter. This reduction is written 2 + 2 ↠ 4 {displaystyle 2+2 woheadrightarrow 4} . Functions in type theory have a special reduction rule: the argument of the function call gets substituted for every occurrence of the parameter in the function definition. Let's say the function d o u b l e {displaystyle mathrm {double} } is defined as λ x . x + x {displaystyle lambda x.x+x} (using Church's lambda notation) or x ↦ x + x {displaystyle xmapsto x+x} (using a more modern notation). Then, the function call d o u b l e   2 {displaystyle mathrm {double} 2} would be reduced by substituting 2 {displaystyle 2} for every copy of x {displaystyle x} in the body of the function definition. Thus, d o u b l e   2 ↠ 2 + 2 {displaystyle mathrm {double} 2 woheadrightarrow 2+2} .