Type theory

In mathematics, logic, and computer science, type theory generally refers to a class of formal systems, some of which can serve as alternatives to naive 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. The types of type theory were created to avoid paradoxes in a variety of formal logics and rewrite systems and sometimes "type theory" is used to refer to this broader application.

Two well-known type theories that can serve as mathematical foundations are Alonzo Church's typed λ-calculi and Per Martin-Löf's intuitionistic type theory. Type theories are often the mathematical foundation used by computer proof assistants because of the Curry-Howard correspondence which equates programs with proofs.

History

Main article: History of type theory

The types of type theory were invented by Bertrand Russell in response to his discovery that Gottlob Frege's version of naive set theory was afflicted with Russell's paradox. This theory of types features prominently in Whitehead and Russell's Principia Mathematica. It avoids 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.

The common usage of "type theory" is when those types are used with a combinatory logic (or a term rewrite system). The most famous early example is Alonzo Church's lambda calculus. Church's Theory of Types^[1] 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. This forces the rules of the system to have at least two different judgements, where a premise or conclusion is a "term" or a "type".

For example, $nat$ may be a type representing the natural numbers and $0, 1, 2, ...$ may be terms. The judgement that $nat$ is a type is usually written $nat\, \mbox{Type}$ . The judgement that a term $2$ has type $nat$ is usually written $2:nat$ .

A function in type theory is denoted with an arrow: " $\to$ ". The function $addOne$ (commonly called "successor" or just " $S$ "), could have the judgement $addOne : nat \to nat$ . Calling or "applying" a function to an argument is usually written without parentheses, so $addOne\ 2$ instead of $addOne(2)$ . (See currying for why.)

In type theory, $addOne\ 2$ and $3$ are different terms of type $nat$ . A reduction rule is necessary to convert one into the other. Because of this, many systems of type theory have judgements for "term equality" written $a=b:A$ and for "type equality" written $A=B\, \mbox{Type}$ . (Warning: This "equality judgement" is separate from the "equality type" (often called "identity") that may be defined in a type theory.)

For further reading, see Simply typed lambda calculus. It is an early type theory that has few concepts and many later type theories are derived from it.

Difference from set theory

There are many different set theories and many different systems of type theory, so what follows are generalizations.

Set theory is built on top of logic. It requires a system like Frege's underneath it. In type theory, concepts like "and" and "or" can be encoded as types.
Type theory has terms that are separate from types. Some set theories only have sets (and non-set values of logic).
Type theory can have computation ("reduction"). The terms $addOne\ 2$ and $3$ are separate and differentiable.
Set theory usually encodes numbers as sets. Type theory can encode numbers as functions using Church encoding or as inductive types, which are a type with well-behaved constant terms.
In set theory, an element can belong to multiple sets, either to a subset or superset. In type theory, terms (generally) belong to only one type. Where a subset would be used, type theory creates a new type, called a dependent sum type, with new terms. Union is similarly achieved by a new sum type and new terms.
Type theory has a simple connection to constructive mathematics through the BHK interpretation.

Optional features

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". So the "term"s of the language can be reduced using rewriting rules (usually this means substitution).

Some example are reductions in lambda calculus.

Normalization

A value like $addOne\ 2$ reduces to $3$ . Since $3$ cannot be reduced further, it is called a "normal form". A system of type theory is said to be strongly normalizing if all terms have a "normal form" and any order of reductions reaches it. Weakly normalizing systems have a normal form but some orders of reductions may loop forever and never reach it.

Usually, two terms have a judgement of term equality if there exists a term that they both reduce to. Strongly normalizing systems can always test if two terms are equal by checking if they both reduce to the same normal form.

Also see Confluence. Applied to the lambda calculus, it is the Church–Rosser theorem

Constructive

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

For non-constructive mathematics in these systems, it is possible to assume the Law of excluded middle and, if needed, the Axiom of choice. However, those assumptions will not have a computational component.

Homotopy type theory currently assumes the univalence axiom, but the area is actively being researched and it has been hypothesized that the univalence axiom may be able to be proven rather than assumed.

Dependent types

Main article: 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 $nat$ s of length 4 may be a different type than a list of $nat$ s of length 5. In a type theory with dependent types, it is possible to define a function that take 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.

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

Equality types (or "identity types")

Many type theories have a type that represents equality of types and terms. It is separate from the judgement of equality and is often called "propositional equality" to differentiate it.

In intuitionistic type theory, the dependent type is known as $I$ for identity. There is a type $I\ A\ a\ b$ when $A$ is a type and $a$ and $b$ are both terms of type $A$ . A term of type $I\ A\ a\ b$ is interpreted as meaning that $a$ is equal to $b$ .

In practice, it is possible to build a type $I\ 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 $3$ is a term of type $nat$ , then there exists a term of type $I\ nat\ 3\ 3$ . More complicated equalities can be created by creating a reflexive term and then doing a reduction on one side. So if $addOne\ 2$ is a term of type $nat$ , then there is a term of type $I\ nat\ (addOne\ 2)\ (addOne\ 2)$ and, by reduction, generate a term of type $I\ nat\ (addOne\ 2)\ 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. However, it is possible to state that using types. It is usually stated as "there exists a function mapping $I\ nat\ 3\ 4$ to a type that has no terms". As crazy as it sounds, there can be term $f$ with type $(I\ nat\ 3\ 4) \to EmptyType$ even though both $I\ nat\ 3\ 4$ and $EmptyType$ have no terms.

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

Inductive types

Main article: Inductive 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 types and functions that generate terms (called "constructors") that have well-behaved properties. For example, certain recursive functions called on inductive types are guaranteed to terminate.

"Coinductive types" are infinite data types, but functions to generate the next term are guaranteed to terminate in a finite number of steps. See Coinduction and Corecursion.

Induction recursion allows a wider range of well-behaved types but requires that the type and the recursive functions that operate on them be defined at the same time.

Type universes

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 contain all other types.

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.

Systems of type theory

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
some forms of combinatory logic
ST type theory
others defined in the lambda cube
others under the name typed lambda calculus
others under the name pure type system

Active

Homotopy type theory is being researched

Practical impact

Programming languages

Main article: Type system

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. Definitions of type system vary, but the following one due to Benjamin C. Pierce roughly corresponds to the current consensus in the programming language theory community:

[A type system is a] tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.^[2]

In other words, a type system divides program values into sets called types — this is called a type assignment — and makes certain program behaviors illegal on the basis of the types that are thus assigned. For example, a type system may classify the value "hello" as a string and the value 5 as a number, and prohibit the programmer from adding "hello" to 5 based on that type assignment. In this type system, the program

"hello" + 5

would be illegal. Hence, any program permitted by the type system would be provably free from the erroneous behavior of adding strings and numbers.

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 influence by them.

Proof assistants

Main article: Proof assistant

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. This is not surprising, given the close connection between type theory and programming languages.

LF is used by Twelf, often to define other type theories
Multiple type theories falling under higher-order logic are used by the HOL family of provers and PVS
Intuitionistic type theory is used by Agda which is both a programming language and proof assistant.
Computational Type Theory is used by NuPRL
The calculus of constructions and its derivatives are used by Coq and Matita.

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. The most common construction takes the basic types $e$ and $t$ for individuals and truth-values, respectively, and defines the set of types recursively as follows:

if $a$ and $b$ are types, then so is $\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 $\langle a,b\rangle$ is the type of functions from entities of type $a$ to entities of type $b$ . Thus one has types like $\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 $\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).

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.

Mathematical foundations

There is current research into mathematical foundations using homotopy type theory. It is exploring connections between dependent types (especially the identity type) and algebraic topology (specifically homotopy).

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 a type theory shorn of its syntax." A number significant results follow in this way:^[3]

cartesian closed categories correspond to the typed λ-calculus (Lambek, 1970)
C-monoids (categories with products and exponentials and a single, nonterminal 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.

References

W. Farmer, The seven virtues of simple type theory, Journal of Applied Logic, Vol. 6, No. 3. (September 2008), pp. 267–286.

^ Alonzo Church, A formulation of the simple theory of types, The Journal of Symbolic Logic 5(2):56–68 (1940)
^ Types and Programming Languages, Benjamin C. Pierce, The MIT Press, Cambridge, MA. (2002), ISBN 0-262-16209-1.
^ John L. Bell (2012). "Types, Sets and Categories". In Akihiro Kanamory. Handbook of the History of Logic. Volume 6. Sets and Extensions in the Twentieth Century. Elsevier. ISBN 978-0-08-093066-4.

External links

Computational type theory at Scholarpedia, curated by Robert L. Constable.
The TYPES Forum — moderated e-mail forum focusing on type theory in computer science, operating since 1987.
The Nuprl Book: "Introduction to Type Theory."
Types Project lecture notes of summer schools 2005-2008
- The 2005 summer school has introductory lectures

Logic

Overview

Academic areas	Argumentation theory Axiology Critical thinking Computability theory Formal semantics History of logic Informal logic Logic in computer science Mathematical logic Mathematics Metalogic Metamathematics Model theory Philosophical logic Philosophy Philosophy of logic Philosophy of mathematics Proof theory Set theory

Foundations	Abduction Analytic truth Antinomy A priori Deduction Definition Description Induction Inference Logical form Logical consequence Logical truth Name Necessity Meaning Paradox Possible world Presupposition Probability Reason Reasoning Reference Semantics Statement Strict implication Substitution Syntax Truth Truth value Validity

Philosophical logic

Critical thinking Informal logic	Analysis Ambiguity Argument Belief Bias Credibility Evidence Explanation Explanatory power Fact Fallacy Inquiry Opinion Parsimony Premise Propaganda Prudence Reasoning Relevance Rhetoric Rigor Vagueness

Theories of deduction	Constructivism Dialetheism Fictionalism Finitism Formalism Intuitionism Logical atomism Logicism Nominalism Platonic realism Pragmatism Realism

Metalogic Metamathematics

Cantor's theorem Church's theorem Church's thesis Consistency Effective method Foundations of mathematics Gödel's completeness theorem Gödel's incompleteness theorems Soundness Completeness Decidability Interpretation Löwenheim–Skolem theorem Metatheorem Satisfiability Independence Type–token distinction Use–mention distinction

Mathematical logic

General	Formal language Formation rule Formal system Deductive system Formal proof Formal semantics Well-formed formula Set Element Class Classical logic Axiom Natural deduction Rule of inference Relation Theorem Logical consequence Axiomatic system Type theory Symbol Syntax Theory

Traditional logic	Proposition Inference Argument Validity Cogency Syllogism Square of opposition Venn diagram

Propositional calculus Boolean logic	Boolean functions Propositional calculus Propositional formula Logical connectives Truth tables

Predicate logic	First-order Quantifiers Predicate Second-order Monadic predicate calculus

Set theory	Set Empty set Enumeration Extensionality Finite set Function Subset Power set Countable set Recursive set Domain Range Ordered pair Uncountable set

Model theory	Model Interpretation Non-standard model Finite model theory Truth value Validity

Proof theory	Formal proof Deductive system Formal system Theorem Logical consequence Rule of inference Syntax

Computability theory	Recursion Recursive set Recursively enumerable set Decision problem Church–Turing thesis Computable function Primitive recursive function

Non-classical logic

Modal logic	Alethic Axiologic Deontic Doxastic Epistemic Temporal

Intuitionism	Intuitionistic logic Constructive analysis Heyting arithmetic Intuitionistic type theory Constructive set theory

Fuzzy logic	Degree of truth Fuzzy rule Fuzzy set Fuzzy finite element Fuzzy set operations

Substructural logic	Structural rule Relevance logic Linear logic

Paraconsistent logic	Dialetheism

Description logic	Ontology Ontology language

Logicians

Anderson Aristotle Averroes Avicenna Bain Barwise Bernays Boole Boolos Cantor Carnap Church Chrysippus Curry De Morgan Frege Geach Gentzen Gödel Hilbert Kleene Kripke Leibniz Löwenheim Peano Peirce Putnam Quine Russell Schröder Scotus Skolem Smullyan Tarski Turing Whitehead William of Ockham Wittgenstein Zermelo

Lists

Topics	Index of logic articles Mathematical logic Boolean algebra Set theory

Other	Logicians Rules of inference Paradoxes Fallacies Logic symbols

Common logical symbols

& ∨ ¬ ~ → ⊃ ≡ \| ∀ ∃ ⊤ ⊥ ⊢ ⊨ ∴ ∵

Portal
Category
Outline
WikiProject
Talk
changes

Contents