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.
Contents
- History
- Basic concepts
- Difference from set theory
- Normalization
- Dependent types
- Equality types or identity types
- Inductive types
- Universe types
- Computational component
- Major
- Minor
- Active
- Programming languages
- Mathematical foundations
- Proof assistants
- Linguistics
- Social sciences
- Relation to category theory
- References
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.
History
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 attempt to avoid 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. In the 1920s, Leon Chwistek and Frank P. Ramsey proposed a simpler theory, now known as the "theory of simple types" or "simple type theory", that collapsed the complicated hierarchy of the "ramified theory" and 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.
Basic concepts
In a system of type theory, each term has a type and operations are restricted to terms of a certain type. A typing judgment
A function in type theory is denoted with an arrow
Type theories also contain rules for rewriting terms. These are called conversion rules or, if the rule only works in one direction, a reduction rule. For example,
Difference from set theory
There are many different set theories and many different systems of type theory, so what follows are generalizations.
Normalization
The term
For a normalizing system, some borrow the word element from set theory and use it to refer to all closed terms that can reduce to the same normal form. A closed term is one without parameters. (A term like
A similar idea that works for open and closed terms is convertibility. Two terms are convertible if there exists a term that they both reduce to. For example,
Dependent types
A dependent type is a type that depends on a term or on another type. Thus, the type returned by a function may depend upon the argument to the function.
For example, a list of
Dependent types play a central role in intuitionistic type theory and in the design of functional programming languages like Idris, ATS, Agda and Epigram.
Equality types (or "identity types")
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 is known as
In practice, it is possible to build a type
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
Homotopy type theory differs from intuitionistic type theory mostly by its handling of the equality type.
Inductive types
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 type 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 that 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.
Universe types
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.
Computational component
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.
Major
Minor
Active
Programming languages
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 intuitionistic type theory 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.
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 current 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:
Multiple 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.
Linguistics
Type theory is also widely in use in formal theories of semantics of natural languages, especially Montague grammar and its descendants. In particular, categorial grammars and pregroup grammars make extensive use of type constructors to define the types (noun, verb, etc.) of words.
The most common construction takes the basic types
A complex type
Social sciences
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.
Relation to 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:
The interplay, known as categorical logic, has been a subject of active research since then; see the monograph of Jacobs (1999) for instance.