Type theory

In mathematics and theoretical computer science, a type theory is the formal presentation of a specific type system. Type theory is the academic study of type systems.
Some type theories serve as alternatives to set theory as a foundation of mathematics. Two influential type theories that have been proposed as foundations are:

Most computerized proof-writing systems use a type theory for their foundation. A common one is Thierry Coquand's calculus of inductive constructions.

History

Type theory was created to avoid paradoxes in naive set theory and formal logic, such as Russell's paradox which demonstrates that, without proper axioms, it is possible to define the set of all sets that are not members of themselves; this set both contains itself and does not contain itself. Between 1902 and 1908, Bertrand Russell proposed various solutions to this problem.
By 1908, Russell arrived at a ramified theory of types together with an axiom of reducibility, both of which appeared in Whitehead and Russell's Principia Mathematica published in 1910, 1912, and 1913. This system avoided contradictions suggested in Russell's paradox by creating a hierarchy of types and then assigning each concrete mathematical entity to a specific type. Entities of a given type were built exclusively of subtypes of that type, thus preventing an entity from being defined using itself. This resolution of Russell's paradox is similar to approaches taken in other formal systems, such as Zermelo-Fraenkel set theory.
Type theory is particularly popular in conjunction with Alonzo Church's lambda calculus. One notable early example of type theory is 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.
In the modern literature, "type theory" refers to a typed system based around lambda calculus. One influential system is Per Martin-Löf's intuitionistic type theory, which was proposed as a foundation for constructive mathematics. Another is Thierry Coquand's calculus of constructions, which is used as the foundation by Rocq, Lean, and other computer proof assistants. Type theory is an active area of research, one direction being the development of homotopy type theory.

Applications

Mathematical foundations

The first computer proof assistant, called Automath, used type theory to encode mathematics on a computer. Martin-Löf specifically developed intuitionistic type theory to encode all mathematics to serve as a new foundation for mathematics. There is ongoing research into mathematical foundations using homotopy type theory.
Mathematicians working in category theory already had difficulty working with the widely accepted foundation of Zermelo–Fraenkel set theory. This led to proposals such as Lawvere's Elementary Theory of the Category of Sets. Homotopy type theory continues in this line using type theory. Researchers are exploring connections between dependent types and algebraic topology.

Proof assistants

Much of the current research into type theory is driven by proof checkers, interactive proof assistants, and automated theorem provers. Most of these systems use a type theory as the mathematical foundation for encoding proofs, which is not surprising, given the close connection between type theory and programming languages:

LF is used by Twelf, often to define other type theories;
many type theories which fall under higher-order logic are used by the HOL family of provers and PVS;
computational type theory is used by NuPRL;
calculus of constructions and its derivatives are used by Rocq, Matita, and Lean;
UTT is used by Agda which is both a programming language and proof assistant

Many type theories are supported by LEGO and Isabelle. Isabelle also supports foundations besides type theories, such as ZFC. Mizar is an example of a proof system that only supports set theory.

Programming languages

Any static program analysis, such as the type checking algorithms in the semantic analysis phase of compiler, has a connection to type theory. A prime example is Agda, a programming language which uses UTT for its type system.
The programming language ML was developed for manipulating type theories and its own type system was heavily influenced by them.

Linguistics

Type theory is also widely used in formal theories of semantics of natural languages, especially Montague grammar and its descendants. In particular, categorial grammars and pregroup grammars extensively use type constructors to define the types of words.
The most common construction takes the basic types and for individuals and truth-values, respectively, and defines the set of types recursively as follows:

if and are types, then so is ;
nothing except the basic types, and what can be constructed from them by means of the previous clause are types.

A complex type is the type of functions from entities of type to entities of type. Thus one has types like that are interpreted as elements of the set of functions from entities to truth-values, i.e. indicator functions of sets of entities. An expression of type is a function from sets of entities to truth-values, i.e. a set of sets. This latter type is standardly taken to be the type of natural language quantifiers, like everybody or nobody.
Type theory with records is a formal semantics representation framework, using records to express type theory types. It has been used in natural language processing, principally computational semantics and dialogue systems.

Social sciences

introduced a theory of logical types into the social sciences; his notions of double bind and logical levels are based on Russell's theory of types.

Logic

A type theory is a mathematical logic, which is to say it is a collection of rules of inference that result in judgments. Most logics have judgments asserting "The proposition is true", or "The formula is a well-formed formula". A type theory has judgments that define types and assign them to a collection of formal objects, known as terms. A term and its type are often written together as.

Terms

A term in logic is recursively defined as a constant symbol, variable, or a function application, where a term is applied to another term. Constant symbols could include the natural number, the Boolean value, and functions such as the successor function and conditional operator. Thus some terms could be,,, and.

Judgments

Most type theories have 4 judgments:

" is a type"
" [|is a term] of type "
"Type [|is equal to] type "
"Terms and both of type are equal"

Judgments may follow from assumptions. For example, one might say "assuming is a term of type and is a term of type, it follows that is a term of type ". Such judgments are formally written with the turnstile symbol.
If there are no assumptions, there will be nothing to the left of the turnstile.
The list of assumptions on the left is the context of the judgment. Capital greek letters, such as Gamma| and, are common choices to represent some or all of the assumptions. The 4 different judgments are thus usually written as follows.

Formal notation for judgments	Description
Type	is a type.
	is a term of type .
	Type is equal to type .
	Terms and are both of type and [\|are equal].

Some textbooks use a triple equal sign to stress that this is judgmental equality and thus an extrinsic notion of equality. The judgments enforce that every term has a type. The type will restrict which rules can be applied to a term.

Rules of inference

A type theory's inference rules say what judgments can be made, based on the existence of other judgments. Rules are expressed as a Gentzen-style deduction using a horizontal line, with the required input judgments above the line and the resulting judgment below the line. For example, the following inference rule states a substitution rule for judgmental equality.The rules are syntactic and work by rewriting. The metavariables,,,, and may actually consist of complex terms and types that contain many function applications, not just single symbols.
To generate a particular judgment in type theory, there must be a rule to generate it, as well as rules to generate all of that rule's required inputs, and so on. The applied rules form a proof tree, where the top-most rules need no assumptions. One example of a rule that does not require any inputs is one that states the type of a constant term. For example, to assert that there is a term of type, one would write the following.

Type inhabitation

Generally, the desired conclusion of a proof in type theory is one of type inhabitation. The decision problem of type inhabitation is:
Girard's paradox shows that type inhabitation is strongly related to the consistency of a type system with Curry–Howard correspondence. To be sound, such a system must have uninhabited types.
A type theory usually has several rules, including ones to:

create a judgment
add an assumption to the context
rearrange the assumptions
use an assumption to create a variable
define reflexivity, symmetry and transitivity for judgmental equality
define substitution for application of lambda terms
list all the interactions of equality, such as substitution
define a hierarchy of type universes
assert the existence of new types

Also, for each "by rule" type, there are 4 different kinds of rules:

"type formation" rules say how to create the type
"term introduction" rules define the canonical terms and constructor functions, like "pair" and "S".
"term elimination" rules define the other functions like "first", "second", and "R".
"computation" rules specify how computation is performed with the type-specific functions.

For examples of rules, an interested reader may follow Appendix A.2 of the Homotopy Type Theory book, or read Martin-Löf's Intuitionistic Type Theory.