Type theory

In a system of type theory, a term is opposed to a type. For example, 4, 2 + 2, and ${\displaystyle 2\cdot 2}$ are all separate terms with the type nat for natural numbers. Traditionally, the term is followed by a colon and its type, such as 2 : nat - this means that the number 2 is of type nat. Beyond this opposition and syntax, little can be said about types in this generality, but often, they are interpreted as some kind of collection (not necessarily sets) of the values that the term might evaluate to. It is usual to denote terms by e and types by τ. How terms and types are shaped depends on the particular type system and is made precise by some syntax and additional restrictions of well-formedness.

Typing usually takes place in some context or environment denoted by the symbol ${\displaystyle \Gamma }$. Often, an environment is a list of pairs ${\displaystyle e:\tau }$. This pair is sometimes called an assignment. The context completes the above opposition. Together they form a judgement denoted ${\displaystyle \Gamma \vdash e:\tau }$.

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, ${\displaystyle 2+2}$ and ${\displaystyle 4}$ are syntactically different terms, but the former reduces to the latter. This reduction is written ${\displaystyle 2+2\twoheadrightarrow 4}$. These rules also establish corresponding equivalences between the terms, written ${\displaystyle 2+2\equiv 4}$.

The term ${\displaystyle 2+1}$ reduces to ${\displaystyle 3}$. Since ${\displaystyle 3}$ cannot be reduced further, it is called a normal form. Various systems of typed lambda calculus including the simply typed lambda calculus, Jean-Yves Girard's System F, and Thierry Coquand's calculus of constructions are strongly normalizing. In such systems, a successful type check implies a termination proof of the term.

Based on the judgements and equivalences type inference rules can be used to describe how a type system assigns a type to a syntactic constructions (terms), much like in natural deduction. To be meaningful, conversion and type rules are usually closely related as in e.g. by a subject reduction property, which might establish a part of the soundness of a type system.

The decision problem of type checking (abbreviated by ${\displaystyle \Gamma \vdash e:\tau$ ?} ) is:

Given a type environment ${\displaystyle \Gamma }$, a term ${\displaystyle e}$, and a type ${\displaystyle \tau }$, decide whether the term ${\displaystyle e}$ can be assigned the type ${\displaystyle \tau }$ in the type environment ${\displaystyle \Gamma }$.

Decidability of type checking means that type safety of any given program text (source code) can be verified.

The decision problem of typability (abbreviated by ${\displaystyle \exists \Gamma ,\tau .\Gamma \vdash e:\tau$ ?} ) is:

Given a term ${\displaystyle e}$, decide whether there exists a type environment ${\displaystyle \Gamma }$ and a type ${\displaystyle \tau }$ such that the term ${\displaystyle e}$ can be assigned the type ${\displaystyle \tau }$ in the type environment ${\displaystyle \Gamma }$.

A variant of typability is typability wrt. a type environment (abbreviated by ${\displaystyle \exists \tau .\Gamma \vdash e:\tau$ ?} ), for which a type environment is part of the input. If the given term does not contain external references (such as free term variables), then typability coincides with typability wrt. the empty type environment.

Typability is closely related to type inference. Whereas typability (as a decision problem) addresses the existence of a type for a given term, type inference (as a computation problem) requires an actual type to be computed.

The decision problem of type inhabitation (abbreviated by ${\displaystyle \exists e.\Gamma \vdash e:\tau$ ?} ) is:

Given a type environment ${\displaystyle \Gamma }$ and a type ${\displaystyle \tau }$, decide whether there exists a term ${\displaystyle e}$ that can be assigned the type ${\displaystyle \tau }$ in the type environment ${\displaystyle \Gamma }$.

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.

The opposition of terms and types can also be views as one of implementation and specification. By program synthesis (the computational counterpart of) type inhabitation (see below) can be used to construct (all or parts of) programs from specification given in form of type information.[4]

Beside the view of types as collection of values of a term, type theory offers a second interpretation of the opposition of term and types. Types can be seen as propositions and terms as proofs. In this way of reading a typing, a function type ${\displaystyle \alpha \rightarrow \beta }$ is viewed as an implication, i.e. as the proposition, that ${\displaystyle \beta }$ follows from ${\displaystyle \alpha }$.

The internal language of the cartesian closed category is the simply typed lambda calculus. This view can be extend to other typed lambda calculi. Certain Cartesian closed categories, the topoi, have been proposed as a general setting for mathematics, instead of traditional set theory.

A dependent type is a type that depends on a term or another type. Thus, the type returned by a function may depend on the argument to the function.

For example, a list of ${\displaystyle \mathrm {nat} }$s of length 4 may be a different type than a list of ${\displaystyle \mathrm {nat} }$s of length 5. In a type theory with dependent types, it is possible to define a function that takes a parameter "n" and returns a list containing "n" zeros. Calling the function with 4 would produce a term with a different type than if the function was called with 5.

Another example is the type consisting of the proofs that the argument term has a certain property, such as the term of ${\displaystyle \mathrm {nat} }$ type, e.g., a given natural number, is prime. See Curry-Howard Correspondence.

Dependent types play a central role in intuitionistic type theory and in the design of functional programming languages like Idris, ATS, Agda and Epigram.

Many systems of type theory have a type that represents equality of types and of terms. This type is different from convertibility, and is often denoted propositional equality.

In intuitionistic type theory, the equality type (also called the identity type) is known as ${\displaystyle I}$ for identity. There is a type ${\displaystyle I\ A\ a\ b}$ when ${\displaystyle A}$ is a type and ${\displaystyle a}$ and ${\displaystyle b}$ are both terms of type ${\displaystyle A}$. A term of type ${\displaystyle I\ A\ a\ b}$ is interpreted as meaning that ${\displaystyle a}$ is equal to ${\displaystyle b}$.

In practice, it is possible to build a type ${\displaystyle I\ \mathrm {nat} \ 3\ 4}$ but there will not exist a term of that type. In intuitionistic type theory, new terms of equality start with reflexivity. If ${\displaystyle 3}$ is a term of type ${\displaystyle \mathrm {nat} }$, then there exists a term of type ${\displaystyle I\ \mathrm {nat} \ 3\ 3}$. More complicated equalities can be created by creating a reflexive term and then doing a reduction on one side. So if ${\displaystyle 2+1}$ is a term of type ${\displaystyle \mathrm {nat} }$, then there is a term of type ${\displaystyle I\ \mathrm {nat} \ (2+1)\ (2+1)}$ and, by reduction, generate a term of type ${\displaystyle I\ \mathrm {nat} \ (2+1)\ 3}$. Thus, in this system, the equality type denotes that two values of the same type are convertible by reductions.

Having a type for equality is important because it can be manipulated inside the system. There is usually no judgement to say two terms are not equal; instead, as in the Brouwer–Heyting–Kolmogorov interpretation, we map ${\displaystyle \neg (a=b)}$ to ${\displaystyle (a=b)\to \bot }$, where ${\displaystyle \bot }$ is the bottom type having no values. There exists a term with type ${\displaystyle (I\ \mathrm {nat} \ 3\ 4)\to \bot }$, but not one of type ${\displaystyle (I\ \mathrm {nat} \ 3\ 3)\to \bot }$.

Homotopy type theory differs from intuitionistic type theory mostly by its handling of the equality type.

A system of type theory requires some basic terms and types to operate on. Some systems build them out of functions using Church encoding. Other systems have inductive types: a set of base types and a set of type constructors that generate types with well-behaved properties. For example, certain recursive functions called on inductive types are guaranteed to terminate.

Coinductive types are infinite data types created by giving a function that generates the next element(s). See Coinduction and Corecursion.

Induction-induction is a feature for declaring an inductive type and a family of types which depends on the inductive type.

Induction recursion allows a wider range of well-behaved types, allowing the type and recursive functions operating on it to be defined at the same time.

Types were created to prevent paradoxes, such as Russell's paradox. However, the motives that lead to those paradoxes—being able to say things about all types—still exist. So, many type theories have a "universe type", which contains all other types (and not itself).

In systems where you might want to say something about universe types, there is a hierarchy of universe types, each containing the one below it in the hierarchy. The hierarchy is defined as being infinite, but statements must only refer to a finite number of universe levels.

Type universes are particularly tricky in type theory. The initial proposal of intuitionistic type theory suffered from Girard's paradox.

Many systems of type theory, such as the simply-typed lambda calculus, intuitionistic type theory, and the calculus of constructions, are also programming languages. That is, they are said to have a "computational component". The computation is the reduction of terms of the language using rewriting rules.

A system of type theory that has a well-behaved computational component also has a simple connection to constructive mathematics through the BHK interpretation.

Non-constructive mathematics in these systems is possible by adding operators on continuations such as call with current continuation. However, these operators tend to break desirable properties such as canonicity and parametricity.

• Simply typed lambda calculus which is a higher-order logic;
• intuitionistic type theory;
• system F;
• LF is often used to define other type theories;
• calculus of constructions and its derivatives.

• Automath;
• ST type theory;
• UTT (Lao's Unified Theory of dependent Types)
• some forms of combinatory logic;
• others defined in the lambda cube;
• others under the name typed lambda calculus;
• others under the name pure type system.

• Homotopy type theory is being researched.

There is extensive overlap and interaction between the fields of type theory and type systems. Type systems are a programming language feature designed to identify bugs. 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 (Luo's Unified Theory of dependent Types) for its type system. The programming language ML was developed for manipulating type theories (see LCF) and its own type system was heavily influenced by them.

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 (ETCS).[5] Homotopy type theory continues in this line using type theory. Researchers are exploring connections between dependent types (especially the identity type) and algebraic topology (specifically homotopy).

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 Coq, Matita, and Lean;
• UTT (Luo's Unified Theory of dependent Types) 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.

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 (noun, verb, etc.) of words.

The most common construction takes the basic types ${\displaystyle e}$ and ${\displaystyle t}$ for individuals and truth-values, respectively, and defines the set of types recursively as follows:

• if ${\displaystyle a}$ and ${\displaystyle b}$ are types, then so is ${\displaystyle \langle a,b\rangle }$;
• nothing except the basic types, and what can be constructed from them by means of the previous clause are types.

A complex type ${\displaystyle \langle a,b\rangle }$ is the type of functions from entities of type ${\displaystyle a}$ to entities of type ${\displaystyle b}$. Thus one has types like ${\displaystyle \langle e,t\rangle }$ which 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 ${\displaystyle \langle \langle e,t\rangle ,t\rangle }$ is a function from sets of entities to truth-values, i.e. a (indicator 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).

Gregory Bateson 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.