Type theory

In mathematical logic, and theoretical computer science, type theory is the study of formal systems that classify expressions or mathematical objects by their types. Roughly speaking, a type plays a similar role to that played by a data type in programming: it specifies what kind of thing an expression is and how it may be used. Type theories are used in the study of programming languages (type systems), formal logic, and the formalization of mathematics.

Some type theories have been proposed as alternatives to set theory as a foundation of mathematics. Examples include Alonzo Church's simple theory of types and Per Martin-Löf's intuitionistic type theory.

Many proof assistants are based on type theory. For example, the underlying formal language of Rocq (formerly Coq) is the calculus of inductive constructions, while Lean is based on dependent type theory.

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 (previously known as Coq), 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 (ETCS). 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).

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 (previously known as 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.

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 (Luo's Unified Theory of dependent Types) for its type system.

The programming language ML was developed for manipulating type theories (see Logic for Computable Functions) 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 (noun, verb, etc.) of words.

The most common construction takes the basic types <math>e</math> and <math>t</math> for individuals and truth-values, respectively, and defines the set of types recursively as follows:

if <math>a</math> and <math>b</math> 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 <math>\langle a,b\rangle</math> is the type of functions from entities of type <math>a</math> to entities of type . Thus one has types like <math>\langle e,t\rangle</math> 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 <math>\langle\langle e,t\rangle,t\rangle</math> 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).

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.

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.

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 <math>\varphi</math> is true", or "The formula <math>\varphi</math> 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 <math>\mathrm{S}</math> and conditional operator . Thus some terms could be , , , and .

Judgments

Most type theories have 4 judgments:

"<math>T</math> is a type"
"<math>t</math> is a term of type "
"Type <math>T_1</math> is equal to type "
"Terms <math>t_1</math> and <math>t_2</math> both of type <math>T</math> are equal"

Judgments may follow from assumptions. For example, one might say "assuming <math>x</math> is a term of type <math>\mathsf{bool}</math> and <math>y</math> is a term of type , it follows that <math>(\textrm{if}\,x\,y\,y)</math> is a term of type ". Such judgments are formally written with the turnstile symbol .

: <math>x:\mathsf{bool},y:\mathsf{nat}\vdash(\mathrm{if}\,x\,y\,y): \mathsf{nat}</math>

If there are no assumptions, there will be nothing to the left of the turnstile.

: <math>\vdash \mathrm{S}:\mathsf{nat}\to\mathsf{nat}</math>

The list of assumptions on the left is the context of the judgment. Capital greek letters, such as <math>\Gamma</math> and <math>\Delta</math>, are common choices to represent some or all of the assumptions. The 4 different judgments are thus usually written as follows.

{| class="wikitable"

! Formal notation for judgments !! Description

|<math>\Gamma \vdash T</math> Type||<math>T</math> is a type (under assumptions ).

|<math>\Gamma \vdash t : T</math>||<math>t</math> is a term of type <math>T</math> (under assumptions ).

|<math>\Gamma \vdash T_1 = T_2 </math>||Type <math>T_1</math> is equal to type <math>T_2</math> (under assumptions ).

|<math>\Gamma \vdash t_1 = t_2 : T </math>||Terms <math>t_1</math> and <math>t_2</math> are both of type <math>T</math> and are equal (under assumptions ).

Some textbooks use a triple equal sign <math>\equiv</math> 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.<math display="block">

\begin{array}{c}

\Gamma\vdash t:T_1 \qquad \Delta\vdash T_1 = T_2 \\

\hline

\Gamma,\Delta\vdash t:T_2

\end{array}

</math>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 <math>0</math> of type , one would write the following.

\begin{array}{c}

\hline

\vdash 0 : \mathsf{nat} \\

\end{array}

</math>

Type inhabitation

Generally, the desired conclusion of a proof in type theory is one of type inhabitation. The decision problem of type inhabitation (abbreviated by ) is:

: Given a context and a type , decide whether there exists a term that can be assigned the type in the type environment .

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 (known as a context in this case)
add an assumption to the context (context weakening)
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,

Connections to foundations

The logical framework of a type theory bears a resemblance to intuitionistic, or constructive, logic. Formally, type theory is often cited as an implementation of the Brouwer–Heyting–Kolmogorov interpretation of intuitionistic logic.

Most of the type theories proposed as foundations are constructive, and this includes most of the ones used by proof assistants. It is possible to add non-constructive features to a type theory, by rule or assumption. These include operators on continuations such as call with current continuation. However, these operators tend to break desirable properties such as canonicity and parametricity.

Curry–Howard correspondence

The Curry–Howard correspondence is the observed similarity between logics and programming languages. The implication in logic, "A <math>\to</math> B" resembles a function from type "A" to type "B". For a variety of logics, the rules are similar to expressions in a programming language's types. The similarity goes farther, as applications of the rules resemble programs in the programming languages. Thus, the correspondence is often summarized as "proofs as programs".

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

Type inference

Many programs that work with type theory (e.g., interactive theorem provers) also do type inferencing. It lets them select the rules that the user intends, with fewer actions by the user.

Research areas

Category theory

Although the initial motivation for category theory was far removed from foundationalism, the two fields turned out to have deep connections. As John Lane Bell writes: "In fact categories can themselves be viewed as type theories of a certain kind; this fact alone indicates that type theory is much more closely related to category theory than it is to set theory." In brief, a category can be viewed as a type theory by regarding its objects as types (or sorts ), i.e. "Roughly speaking, a category may be thought of as a type theory shorn of its syntax." A number of significant results follow in this way:

cartesian closed categories correspond to the typed λ-calculus (Lambek, 1970);
C-monoids (categories with products and exponentials and one non-terminal object) correspond to the untyped λ-calculus (observed independently by Lambek and Dana Scott around 1980);
locally cartesian closed categories correspond to Martin-Löf type theories (Seely, 1984).

The interplay, known as categorical logic, has been a subject of active research since then; see the monograph of Jacobs (1999) for instance.

Homotopy type theory

Homotopy type theory attempts to combine type theory and category theory. It focuses on equalities, especially equalities between types. Homotopy type theory differs from intuitionistic type theory mostly by its handling of the equality type. In 2016, cubical type theory was proposed, which is a homotopy type theory with normalization. because it lacks a name. The concept of anonymous functions appears in many programming languages.

Inference Rules

Function application

The power of type theories is in specifying how terms may be combined by way of inference rules.

There are foundational issues that can arise from dependent types if a theory is not careful about what dependences are allowed, such as Girard's Paradox. The logician Henk Barendegt introduced the lambda cube as a framework for studying various restrictions and levels of dependent typing.

Dependent products and sums

Two common type dependences, dependent product and dependent sum types, allow for the theory to encode BHK intuitionistic logic by acting as equivalents to universal and existential quantification; this is formalized by Curry–Howard correspondence. Thus, , , , , .

Axioms

Most type theories do not have axioms. This is because a type theory is defined by its rules of inference. This is a source of confusion for people familiar with Set Theory, where a theory is defined by both the rules of inference for a logic (such as first-order logic) and axioms about sets.

Sometimes, a type theory will add a few axioms. An axiom is a judgment that is accepted without a derivation using the rules of inference. They are often added to ensure properties that cannot be added cleanly through the rules.

Axioms can cause problems if they introduce terms without a way to compute on those terms. That is, axioms can interfere with the normalizing property of the type theory.

Some commonly encountered axioms are:

"Axiom K" ensures "uniqueness of identity proofs". That is, that every term of an identity type is equal to reflexivity.
"Univalence axiom" holds that equivalence of types is equality of types. The research into this property led to cubical type theory, where the property holds without needing an axiom.
"Law of excluded middle" is often added to satisfy users who want classical logic, instead of intuitionistic logic.

The axiom of choice does not need to be added to type theory, because in most type theories it can be derived from the rules of inference. This is because of the constructive nature of type theory, where proving that a value exists requires a method to compute the value. The axiom of choice is less powerful in type theory than most set theories, because type theory's functions must be computable and, being syntax-driven, the number of terms in a type must be countable. (See '.)

List of type theories

Major

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

Minor

Automath
ST type theory
UTT (Luo's unified theory of dependent types)
some forms of combinatory logic
others defined in the lambda cube (also known as pure type systems)
others under the name typed lambda calculus

Active research

Homotopy type theory explores equality of types
Cubical type theory is an implementation of homotopy type theory

Notes

References

External links

Introductory material

Type Theory at nLab, which has articles on many topics.
Intuitionistic Type Theory article at the Stanford Encyclopedia of Philosophy
Lambda Calculi with Types book by Henk Barendregt
Calculus of Constructions / Typed Lambda Calculus textbook style paper by Helmut Brandl
Intuitionistic Type Theory notes by Per Martin-Löf
Programming in Martin-Löf's Type Theory book
Homotopy Type Theory book, which proposed homotopy type theory as a mathematical foundation.

Advanced material

The TYPES Forum – moderated e-mail forum focusing on type theory in computer science, operating since 1987.
Types Project lecture notes of summer schools 2005–2008
The 2005 summer school has introductory lectures
Oregon Programming Languages Summer School, many lectures and some notes.
Summer 2013 lectures including Robert Harper's talks on YouTube
Summer 2015 Types, Logic, Semantics, and Verification
Andrej Bauer's blog

History

Applications

Mathematical foundations

Proof assistants

Programming languages

Linguistics

Logic

Terms

Judgments

Rules of inference

Type inhabitation

Connections to foundations

Curry–Howard correspondence

Type inference

Research areas

Category theory

Homotopy type theory

Inference Rules

Function application

Dependent products and sums

Axioms

List of type theories

Major

Minor

Active research

See also

Notes

References

Further reading

External links

Introductory material

Advanced material

History

Applications

Mathematical foundations

Proof assistants

Programming languages

Linguistics

Social sciences

Logic

Terms

Judgments

Rules of inference

Type inhabitation

Connections to foundations

Curry–Howard correspondence

Type inference

Research areas

Category theory

Homotopy type theory

Inference Rules

Function application

Dependent products and sums

Axioms

List of type theories

Major

Minor

Active research

See also

Notes

References

Further reading

External links

Introductory material

Advanced material