In

(rev. Mon Oct 12, 2020) Russell’s Paradox

3. Early Responses to the Paradox Types did gain a hold when used with one particular logic,

Natural_deduction#Proofs_and_type_theory

) An example of a rule that does not require any inputs is one that states there is a term "0" of type "nat": $$\backslash begin\; \backslash hline\; \backslash vdash\; 0\; :\; nat\; \backslash \backslash \; \backslash end$$ A type theory usually has a number of rules, including ones to: * rearrange the assumptions * add an assumption ("weakening") * define reflexivity, symmetry, and transitivity for judgemental equality * define substitution for application of lambda terms, judgemental equality, etc. * ... Each axiomatic type usually comes with 4 different sets 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.

intuitionistic type theory
Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory
In mathematics, logic, and computer science, a type system is a formal system in which every term has a "type" which defines its meanin ...

* system F
* Logical framework, LF is often used to define other type theories
*

intuitionistic type theory
Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory
In mathematics, logic, and computer science, a type system is a formal system in which every term has a "type" which defines its meanin ...

to encode ''all'' mathematics to serve as a new foundation for mathematics. There is ongoing research into mathematical foundations using

Type Theory at nLab

which has articles on many topics.

Intuitionistic Type Theory

article at the Stanford Encyclopedia of Philosophy

Lambda Calculus with Types

book by Henk Barendregt

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.

The TYPES Forum

— moderated e-mail forum focusing on type theory in computer science, operating since 1987. * [ftp://ftp.cs.cornell.edu/pub/nuprl/doc/book.ps.gz The Nuprl Book]:

Introduction to Type Theory.

of summer schools 2005–2008 ** Th

has introductory lectures

many lectures and some notes.

includin

Robert Harper's talks on YouTube

Book review

* * *

mathematics
Mathematics (from Greek: ) includes the study of such topics as numbers ( and ), formulas and related structures (), shapes and spaces in which they are contained (), and quantities and their changes ( and ). There is no general consensus abo ...

, logic
Logic is an interdisciplinary field which studies truth and reasoning
Reason is the capacity of consciously making sense of things, applying logic
Logic (from Ancient Greek, Greek: grc, wikt:λογική, λογική, label=none, lit ...

, and computer science
Computer science deals with the theoretical foundations of information, algorithms and the architectures of its computation as well as practical techniques for their application.
Computer science is the study of , , and . Computer science ...

, a type theory is a formal system
A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system.
A form ...

in which every "term" has a "type". A "type" in type theory has a role similar to a "type" in a programming language: it dictates the operations that can be performed on a term and, for variables, the possible values it might be replaced with.
Some type theories serve as alternatives to set theory
Set theory is the branch of that studies , which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of , is mostly concerned with those that are relevant to ...

as a foundation of mathematics. Two influential type theories that were proposed as foundations are Alonzo Church
Alonzo Church (June 14, 1903 – August 11, 1995) was an American
American(s) may refer to:
* American, something of, from, or related to the United States of America, commonly known as the United States
The United States of America (USA ...

's typed λ-calculus and Per Martin-Löf
Per Erik Rutger Martin-Löf (; ; born 8 May 1942) is a Swedish
Swedish or ' may refer to:
* Anything from or related to Sweden, a country in Northern Europe
* Swedish language, a North Germanic language spoken primarily in Sweden and Finland
* S ...

's intuitionistic type theory
Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory
In mathematics, logic, and computer science, a type system is a formal system in which every term has a "type" which defines its meanin ...

. Most computerized proof-writing systems use a type theory for their foundation. A common one is Thierry Coquand
Thierry Coquand (; born 18 April 1961 in Jallieu, Isère, France) is a professor in computer science at the University of Gothenburg, Sweden. He is known for his work in constructive mathematics, especially the calculus of constructions. He received ...

's Calculus of Inductive Constructions.
Type theory is closely related to, and in some cases overlaps with, type system
In programming language
A programming language is a formal language comprising a Instruction set architecture, set of instructions that produce various kinds of Input/output, output. Programming languages are used in computer programming to ...

s, which are a programming language
A programming language is a formal language
In mathematics
Mathematics (from Ancient Greek, Greek: ) includes the study of such topics as quantity (number theory), mathematical structure, structure (algebra), space (geometry), and calcu ...

feature used to reduce bugs and facilitate certain compiler optimizations
In computing
Computing is any goal-oriented activity requiring, benefiting from, or creating computing machinery. It includes the study and experimentation of algorithmic processes and development of both computer hardware , hardware and softwar ...

. Because type theory and type systems can overlap, some experts use the phrase "type system" to refer to a specific formal system and the phrase "type theory" to refer to the academic study of them.
History

Type theory was created to avoid a paradox in a mathematical foundation based onnaive set theory
Naive set theory is any of several theories of sets used in the discussion of the foundations of mathematics
Foundations of mathematics is the study of the philosophical and logical and/or algorithmic basis of mathematics, or, in a broader sens ...

and formal logic
Logic is an interdisciplinary field which studies truth
Truth is the property of being in accord with fact or reality.Merriam-Webster's Online Dictionarytruth 2005 In everyday language, truth is typically ascribed to things that aim to re ...

. Russell's paradox
In the foundations of mathematics
Foundations of mathematics is the study of the philosophical and logical and/or algorithmic basis of mathematics, or, in a broader sense, the mathematical investigation of what underlies the philosophical theori ...

, which was discovered by Bertrand Russell
Bertrand Arthur William Russell, 3rd Earl Russell (18 May 1872 – 2 February 1970) was a British , , , , , , , , and .Stanford Encyclopedia of Philosophy"Bertrand Russell" 1 May 2003 Throughout his life, Russell considered himself a , a and ...

, existed because a set could be defined using "all possible sets", which included itself. Between 1902 and 1908, Bertrand Russell proposed various "theories of type" to fix the problem. By 1908 Russell arrived at a "ramified" theory of types together with an "axiom of reducibility
The axiom of reducibility was introduced by Bertrand Russell in the early 20th century as part of his Type theory, ramified theory of types. Russell devised and introduced the axiom in an attempt to manage the contradictions he had discovered in h ...

" both of which featured prominently in Whitehead and Russell's ''Principia Mathematica
Image:Principia Mathematica 54-43.png, 500px, ✸54.43:
"From this proposition it will follow, when arithmetical addition has been defined, that 1 + 1 = 2." – Volume I, 1st editionp. 379(p. 362 in 2nd edition; p. 360 in abridged v ...

'' published between 1910 and 1913. This system avoided Russell's paradox by creating a hierarchy of types and then assigning each concrete mathematical (and possibly other) entity to a type. Entities of a given type are built exclusively from entities of those types that are lower in their hierarchy, thus preventing an entity from being defined using itself.
Types were not always used in logic. There were other techniques to avoid Russell's paradox.''Stanford Encyclopedia of Philosophy'(rev. Mon Oct 12, 2020) Russell’s Paradox

3. Early Responses to the Paradox Types did gain a hold when used with one particular logic,

Alonzo Church
Alonzo Church (June 14, 1903 – August 11, 1995) was an American
American(s) may refer to:
* American, something of, from, or related to the United States of America, commonly known as the United States
The United States of America (USA ...

's Lambda calculus
Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computability, computation based on function Abstraction (computer science), abstraction and function application, application using variable N ...

.
The most famous early example is Alonzo Church
Alonzo Church (June 14, 1903 – August 11, 1995) was an American
American(s) may refer to:
* American, something of, from, or related to the United States of America, commonly known as the United States
The United States of America (USA ...

's simply typed lambda calculus
The simply typed lambda calculus (\lambda^\to), a form
of type theory
In mathematics, logic, and computer science, a type system is a formal system in which every term has a "type" which defines its meaning and the operations that may be performed ...

. Church's theory of types helped the formal system avoid the Kleene–Rosser paradox
In mathematics
Mathematics (from Ancient Greek, Greek: ) includes the study of such topics as quantity (number theory), mathematical structure, structure (algebra), space (geometry), and calculus, change (mathematical analysis, analysis). It h ...

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 mathematics
Mathematics (from Ancient Greek, Greek: ) includes the study of such topics as quantity (number theory), mathematical structure, structure (algebra), space (geometry), and calculus, change (mathematical analysis, analysis). It h ...

.
The phrase "type theory" now generally refers to a typed system based around lambda calculus. One influential system is Per Martin-Löf
Per Erik Rutger Martin-Löf (; ; born 8 May 1942) is a Swedish
Swedish or ' may refer to:
* Anything from or related to Sweden, a country in Northern Europe
* Swedish language, a North Germanic language spoken primarily in Sweden and Finland
* S ...

's intuitionistic type theory
Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory
In mathematics, logic, and computer science, a type system is a formal system in which every term has a "type" which defines its meanin ...

, which was proposed as a foundation for constructive mathematics
In the philosophy of mathematics, constructivism asserts that it is necessary to find (or "construct") a mathematical object to prove that it exists. In classical mathematics, one can prove the existence of a mathematical object without "finding ...

. Another is Thierry Coquand
Thierry Coquand (; born 18 April 1961 in Jallieu, Isère, France) is a professor in computer science at the University of Gothenburg, Sweden. He is known for his work in constructive mathematics, especially the calculus of constructions. He received ...

's calculus of constructions#REDIRECT Calculus of constructions
{{Redirect category shell, 1=
{{R from other capitalisation
...

, which is used as the foundation by Coq
Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proo ...

, Lean
Lean, leaning or LEAN may refer to:
Business practices
* Lean thinking, a business methodology adopted in various fields
** Lean construction, an adaption of lean manufacturing principles to the design and construction process
** Lean government, ...

, and other "proof assistants" (computerized proof writing programs). Type theories are an area of active research, as demonstrated by homotopy type theory
In mathematical logic
Mathematical logic, also called formal logic, is a subfield of mathematics
Mathematics (from Ancient Greek, Greek: ) includes the study of such topics as quantity (number theory), mathematical structure, structure (al ...

.
Introduction to Type Theory

There are many type theories, so describing them all is difficult. This section covers features of many major type theories. It is an introduction for those unfamiliar with type theory. This section is ''not'' trying to be a complete categorization of type theories, nor an exhaustive description of them.Basics

Terms and Types

In type theory, every term has a type. A term and its type are often written together as "''term'' : ''type''". A common type to include in a type theory is theNatural numbers
In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and total order, ordering (as in "this is the ''third'' largest city in the country"). In common mathematical terminology, w ...

, often written as "$\backslash mathbb\; N$" or "nat". Another is Boolean logic
In mathematics
Mathematics (from Ancient Greek, Greek: ) includes the study of such topics as quantity (number theory), mathematical structure, structure (algebra), space (geometry), and calculus, change (mathematical analysis, analysis). It ...

values. So, some very simple terms with their types are:
* 0 : nat
* 42 : nat
* true : bool
Terms can be built out of other terms using function calls. In type theory, a function call is called "function application". Function application takes a term of a given type and results in a term of another given type. Function application is written "''function'' ''argument'' ''argument'' ...", instead of the conventional "''function''(''argument'',''argument'', ...)". For natural numbers, it is possible to define a function called "add" that take two natural numbers. Thus, some more terms with their types are:
* add 0 0 : nat
* add 2 3 : nat
* add 1 (add 1 (add 1 0)) : nat
In the last term, parentheses were added to indicate the order of operations. Technically, most type theories require the parentheses to be present for every operation, but, in practice, they are not written and authors assume readers can use precedence and associativity to know where they are. For similar ease, it is a common notation to write "$x\; +\; y$" instead of "add $x$ $y$". So, the above terms might be rewritten as:
* 0 + 0 : nat
* 2 + 3 : nat
* 1 + (1 + (1 + 0)) : nat
Terms may also contain variables. Variables always have a type. So, assuming "x" and "y" are variables of type "nat", the following are also valid terms:
* x : nat
* x + 2 : nat
* x + (x + y) : nat
There are more types than "nat" and "bool". We have already seen the term "add", which is not a "nat", but a function that, when applied to two "nat"s, computes to a "nat". The type of "add" will be covered later. First, we need to describe "computes to".
Computation

Type theory has a built-in notation of computation. The following terms are all different: * 1 + 4 : nat * 3 + 2 : nat * 0 + 5 : nat but they all compute to the term "5 : nat". In type theory, we use the words "reduction" and "reduce" to refer to computation. So, we say "0 + 5 : nat" reduces to "5 : nat". It can be written "0 + 5 : nat $\backslash twoheadrightarrow$ 5 : nat". The computation is mechanical, accomplished byrewriting
In mathematics
Mathematics (from Ancient Greek, Greek: ) includes the study of such topics as quantity (number theory), mathematical structure, structure (algebra), space (geometry), and calculus, change (mathematical analysis, analysis). It ...

the term's syntax.
Terms that contain variables can be reduced too. So the term "x + (1 + 4) : nat" reduces to "x + 5 : nat". (We can reduce any sub-term within a term, thanks to the Church-Rosser theorem.)
A term without any variables that cannot be reduced further is a "canonical term". All the terms above reduce to "5 : nat", which is a canonical term. The canonical terms of the natural numbers are:
* 0 : nat
* 1 : nat
* 2 : nat
* etc.
Obviously, terms that compute to the same term are equal. So, assuming "x : nat", the terms "x + (1 + 4) : nat" and "x + (4 + 1) : nat" are equal because they both reduce to "x + 5 : nat". When two terms are equal, they can be substituted for each other. Equality is a complex topic in type theory and there are many kinds of equality. This kind of equality, where two terms compute to the same term, is called "judgemental equality".
Functions

In type theory, functions are terms. Functions can either be lambda terms or given axiomatically.Lambda Terms

A lambda term looks like "(λ ''variablename'' : ''type1'' . ''term'')" and has type "''type1'' $\backslash to$ ''type2''". The type "''type1'' $\backslash to$ ''type2''" indicates that the lambda term is a function takes a parameter of type "''type1''" and computes to a term of type "''type2''". The term inside the lambda term must be a value of "''type2''", assuming the variable has type "''type1''". An example of a lambda term is this function which doubles its argument: * (λ x : nat . (add x x)) : nat $\backslash to$ nat The variable name is "x" and the variable has type "nat". The term "(add x x) has type "nat", assuming "x : nat". Thus, the lambda term has type "nat $\backslash to$ nat", which means if it is given a "nat" as an argument, it will compute to a "nat". Reduction (a.k.a. computation) is defined for lambda terms. When the function is applied (a.k.a. called), the argument is substituted for the parameter. Earlier, we saw that function application is written by putting the parameter after the function term. So, if we want to call the above function with the parameter "5" of type "nat", we write: * (λ x : nat . (add x x)) 5 : nat The lambda term was type "nat $\backslash to$ nat", which meant that given a "nat" as an argument, it will produce a term of type "nat". Since we have given it the argument "5", the above term has type "nat". Reduction works by substituting the argument "5" for the parameter "x" in the term "(add x x)", so the term computes to: * (add 5 5) : nat which obviously computes to * 10 : nat A lambda term is often called an "anonymous function" because it has no name. Often, to make things easier to read, a name is given to a lambda term. This is merely a notation and has no mathematical meaning. Some authors call it "notational equality". A name might be given to the function above using the notation: * double : nat $\backslash to$ nat ::= (λ x : nat . (add x x)) This is the same function as above, just a different way to write it. So the term * double 5 : nat still computes to * 10 : natDependent Typing

Dependent typing is when the type returned by a function depends on the value of its argument. For example, when a type theory axiomatically defines the type "bool", it also axiomatically defines the function "if". The function "if" takes 3 arguments and "if true b c" computes to "b" and "if false b c" computes to "c". But what is the type of "if a b c"? If "b" and "c" have the same type, it is obvious: "if a b c" has the same type as "b" and "c". Thus, assuming "a : bool", * if a 2 4 : nat * if a false true : bool But if "b" and "c" have different types, then the type of "if a b c" depends on the value of "a". We use the symbol "Π" to indicate a function that takes an argument and returns a type. Assuming we have some types "B" and C" and "a : bool", "b : B" and "c : C", then * if a b c : (Π a : bool . B $\backslash to$ C $\backslash to$ if a B C) That is, the type of the "if" term is either the type of the second or third argument, depending on the value of the first argument. Because the type can contain computation, dependent typing is amazingly powerful. When mathematicians say "there exists a number $x$ such that $x$ is prime" or "there exists a number $x$ such that property $P(x)$ holds", it can be expressed as a dependent type. That is, the property is proven for the specific "$x$" and that is visible in the type of the result. There are many details to dependent typing. They are too long and complicated for this introduction. See the article ondependent typing
In computer science and logic, a dependent type is a type whose definition depends on a value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's Generalized quan ...

and the lambda cube
In mathematical logic
Mathematical logic, also called formal logic, is a subfield of mathematics
Mathematics (from Ancient Greek, Greek: ) includes the study of such topics as quantity (number theory), mathematical structure, structure ( ...

for more information.
Universes

Π-terms return a type. So what is the type of their return value? Well, there must be a type that contains types. A type that contains other types is called a "universe". It is often written with the symbol $U$. Sometimes there is a hierarchy of universes, with "$U\_0$ : $U\_1$", "$U\_1$ : $U\_2$", etc.. Universes are complicated. If a universe contains itself, it can lead to paradoxes likeGirard's Paradox
In mathematical logic, System U and System U− are pure type systems, i.e. special forms of a typed lambda calculus
A typed lambda calculus
Lambda calculus (also written as λ-calculus) is a formal system in mathematical logic for expressing com ...

. The details of universes are too long and complicated for this introduction.
Common Axiomatic Types and Terms

Type theories usually have a "functional core", described above, and a set of axiomatic types and terms. Below is a non-exhaustive list of common ones. The list ends with "inductive types", which is a powerful technique that is able to construct all the other ones in the list. The mathematical foundations used by the proof assistants "Coq" and "Lean" are based on the "Calculus for Inductive Constructions" which is the "Calculus of Constructions" (its "functional core) with inductive types.Empty Type

Theempty type
Empty may refer to:
Music Albums
* Empty (God Lives Underwater album), ''Empty'' (God Lives Underwater album) or the title song, 1995
* Empty (Nils Frahm album), ''Empty'' (Nils Frahm album), 2020
* Empty (Tait album), ''Empty'' (Tait al ...

has no terms. The type is usually written "$\backslash bot$" or "$\backslash mathbb\; 0$".
It is used to show that something is uncomputable. If for a type "A", you can create a function of type "A $\backslash to\; \backslash bot$", you know that "A" has no terms. An example for the type "A" might be "there exists a number $x$ such that both $x$ is even and $x$ is odd". (See "Product Type" below for how the example "A" is constructed.) When a type has no terms, we say it is "uninhabited".
Unit Type

Theunit type
In the area of mathematical logic
Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mat ...

has exactly 1 canonical term. The type is written "$\backslash top$" or "$\backslash mathbb\; 1$" and the single canonical term is written "*".
The unit type is used to show that something exists or is computable. If for a type "A", you can create a function of type "A $\backslash to\; \backslash top$", you know that "A" has one or more terms. When a type has at least 1 term, we say it is "inhabited".
Boolean Type

The Boolean type has exactly 2 canonical terms. The type is usually written "bool" or "$\backslash mathbb\; B$" or "$\backslash mathbb\; 2$". The canonical terms are usually "true" and "false". The Boolean type is defined with a function "if" such that: * if true b c $\backslash twoheadrightarrow$ b * if false b c $\backslash twoheadrightarrow$ cProduct Type

Theproduct type
In programming language
A programming language is a formal language comprising a Instruction set architecture, set of instructions that produce various kinds of Input/output, output. Programming languages are used in computer programming to impl ...

has terms that are . For types "A" and "B", the product type is written "A $\backslash times$ B". Canonical terms are constructed with the function "pair". The terms are "pair a b", where "a" is a term of type "A" and "b" is a term of type "B". The product type is defined with functions "first" and "second" such that:
* first (pair a b) $\backslash twoheadrightarrow$ a
* second (pair a b) $\backslash twoheadrightarrow$ b
Besides ordered pairs, this type is used for logical and
In logic
Logic (from Ancient Greek, Greek: grc, wikt:λογική, λογική, label=none, lit=possessed of reason, intellectual, dialectical, argumentative, translit=logikḗ)Also related to (''logos''), "word, thought, idea, argument ...

, because it holds an "A" and a "B". It is also used for intersection
The line (purple) in two points (red). The disk (yellow) intersects the line in the line segment between the two red points.
In mathematics, the intersection of two or more objects is another, usually "smaller" object. Intuitively, the inter ...

, because it holds one of both types.
If a type theory has dependent typing, it has dependent pairs. In a dependent pair, the second type depends on the value of the first term. Thus, the type is written "$\backslash Sigma$ a:A . B(a)" where "B" has type "A $\backslash to$ U". It is useful when showing existence of an "a" with property "B(a)".
Sum Type

Thesum type
In computer science
Computer science deals with the theoretical foundations of information, algorithms and the architectures of its computation as well as practical techniques for their application.
Computer science is the study of Algorit ...

is a "tagged union". That is, for types "A" and "B", the type "A + B" holds either a term of type "A" or a term of type "B" and it knows which one it holds. The type comes with the constructors "injectionLeft" and "injectionRight". The call "injectionLeft a" takes "a : A" and returns a canonical term of type "A + B". Similarly, injectionRight b" takes "b : B" and returns a canonical term of type "A + B". The type is defined with a function "match" such that for a type "C" and functions "f : A $\backslash to$ C" and "g : B $\backslash to$ C":
* match (injectionLeft a) C f g $\backslash twoheadrightarrow$ (f a)
* match (injectionRight b) C f g $\backslash twoheadrightarrow$ (g b)
The sum type is used for logical or
In logic
Logic (from Ancient Greek, Greek: grc, wikt:λογική, λογική, label=none, lit=possessed of reason, intellectual, dialectical, argumentative, translit=logikḗ)Also related to (''logos''), "word, thought, idea, argument ...

and for union.
Natural Numbers

The natural numbers are usually implemented in the style ofPeano Arithmetic
In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian people, Italian mathematician Giuseppe Peano. These axioms have been ...

. There is a canonical term, "0 : nat" for zero. Canonical values larger than zero use the constructor function "S : nat $\backslash to$ nat". Thus, "S 0" is one. "S (S 0)" is two. "S (S (S 0)))" is three. Etc. The decimal numbers are just notationally equal to those terms.
* 1 : nat ::= S 0
* 2 : nat ::= S (S 0)
* 3 : nat ::= S (S (S 0))
* ...
The natural numbers defined with a function "R" that uses recursion to define a function for all nats. It takes a function "P : nat $\backslash to$ U" which is the type of the function to define. It also takes a term "PZ : P 0" which is the value at zero and a function "PS : P n $\backslash to$ P (S n)" which says how to transform the value at "n" into the value at "n + 1". Thus, its computation rules are:
* R P PZ PS 0 $\backslash twoheadrightarrow$ PZ
* R P PZ PS (S $n$) $\backslash twoheadrightarrow$ PS (R P PZ PS $n$)
The function "add", that was used earlier, can be defined using "R".
* add : nat$\backslash to$nat$\backslash to$nat ::= R (nat$\backslash to$nat) (λ n:nat . n) (λ n:nat . (λ g:nat$\backslash to$nat . (λ m:nat . S (g m))))
Identity Type

The identity type is the third concept of equality in type theory. The first is "notational equality", which is for definitions like "2 : nat ::= (S (S 0))" that have no mathematical meaning but are useful to readers. The second is "judgemental equality", which is when two terms compute to the same term, like "x + (1 + 4)" and "x + (4 + 1)", which both compute to "x + 5". But type theory needs another form of equality, known as the "identity type" or "propositional equality". The reason it needs the identity type is because some equal terms do not compute to the same term. Assuming "x : nat", the terms "x + 1" and "1 + x" do not compute to the same term. Recall that "+" is a notation for the function "add", which is a notation for the function "R". We cannot compute on "R" until the value for "x" is specified and, until it is specified, two different calls to "R" will not compute to the same term. An identity type requires two terms "a" and "b" of the same type and is written "a = b". So, for "x + 1" and "1 + x", the type would be "x+1 = 1+x". Canonical terms are created with the constructor "reflexivity". The call "reflexivity a" takes a term "a" and returns a canonical term of the type "a = a". Computation with the identity type is done with the function "J". The function "J" lets a term dependent on "a", "b", and a term of type "a = b" to be rewritten so that "b" is replaced by "a". While "J" is one directional, only able to substitute "b" with "a", it can be proven that the identity type is reflexive,symmetric
Symmetry (from Greek συμμετρία ''symmetria'' "agreement in dimensions, due proportion, arrangement") in everyday language refers to a sense of harmonious and beautiful proportion and balance. In mathematics, "symmetry" has a more pre ...

and transitive
Transitivity or transitive may refer to:
Grammar
* Transitivity (grammar), a property of verbs that relates to whether a verb can take direct objects
* Transitive verb, a verb which takes an object
* Transitive case, a grammatical case to mark arg ...

.
If the canonical terms are always "a=a" and "x+1" does not compute to the same term as "1+x", how do we create a term of "x+1 = 1+x"? We use the "R" function. (See "Natural Numbers" above.) The "R" function's argument "P" is defined to be "(λ x:nat . x+1 = 1+x)". The other arguments act like the parts of an induction proof, where "PZ : P 0" becomes the base case "0+1 = 1+0" and "PS : P n $\backslash to$ P (S n)" becomes the inductive case. Essentially, this says that when "x+1 = 1+x" has "x" replaced with a canonical value, the expression will be the same as "reflexivity (x+1)". This application of the function "R" has type "x : nat $\backslash to$ x+1 = 1+x". We can use it and the function "J" to substituted "1+x" for "x+1" in any term. In this way, the identity type is able to capture equalities that are not possible with judgemental equality.
To be clear, it is possible to create the type "0 = 1", but there will not be a way to create terms of that type. Without a term of type "0 = 1", it will not be possible to use the function "J" to substitute "0" for "1" in another term.
The complexities of equality in type theory make it an active research area, see homotopy type theory
In mathematical logic
Mathematical logic, also called formal logic, is a subfield of mathematics
Mathematics (from Ancient Greek, Greek: ) includes the study of such topics as quantity (number theory), mathematical structure, structure (al ...

.
Inductive Types

Inductive types is a way to axiomatically create a large variety of types. In fact, all the types described above and more can be defined using inductive types. Once a type's canonical values and "constructor" functions are specified, computation is determined by structural recursion. There are similar, more powerful ways to create types. These include induction-recursion and induction-induction. There is also a way to create similar types using only lambda terms, called Scott encoding. (NOTE: Type theories do not usually include coinductive types. They represent an infinite data type and most type theories limit themselves to functions that can be proven to halt.)Differences from Set Theory

The traditional foundation for mathematics has been set theory paired with a logic. The most common one cited isZermelo–Fraenkel set theory
In set theory
illustrating the intersection of two sets
Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set ...

, known as "ZF" or, with the Axiom of choice
In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product#Infinite Cartesian products, Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the a ...

, "ZFC". Type theories differ from this foundation in a number of ways.
* Set theory is built on top of logic. It requires a separate system like predicate logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses Quantifica ...

underneath it. In type theory, concepts like "and" and "or" can be encoded as types in the type theory itself.
* Set theory and logic have the law of excluded middle
In logic
Logic is an interdisciplinary field which studies truth and reasoning
Reason is the capacity of consciously making sense of things, applying logic
Logic (from Ancient Greek, Greek: grc, wikt:λογική, λογική, la ...

. That is, every theorem is true or false. When a type theory defines the concepts of "and" and "or" as types, it leads to intuitionistic logic
Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems of ...

, which does not have the law of excluded middle. However, the law can be proven for some types.
* In set theory, an element is not restricted to one set. The element can appear in subsets and unions with other sets. In type theory, terms (generally) belong to only one type. Where a subset would be used, type theory can use a predicate function or use a dependently-typed product type, where each element $x$ is paired with a proof that the subset's property holds for $x$. Where a union would be used, type theory uses the sum type, which contains new canonical terms.
* Type theory has a built-in notion of computation. Thus, "1+1" and "2" are different terms in type theory, but they compute to the same value. Moreover, functions are defined computationally as lambda terms. In set theory, "1+1=2" means that "1+1" is just another way to refer the value "2". Type theory's computation does require a complicated concept of equality.
* Set theory usually encodes numbers as sets. (0 is the empty set, 1 is a set containing the empty set, etc. See Set-theoretic definition of natural numbersIn set theory
illustrating the intersection (set theory), intersection of two set (mathematics), sets.
Set theory is a branch of mathematical logic that studies Set (mathematics), sets, which informally are collections of objects. Although any typ ...

.) Type theory can encode numbers as functions using Church encoding
In mathematics
Mathematics (from Ancient Greek, Greek: ) includes the study of such topics as quantity (number theory), mathematical structure, structure (algebra), space (geometry), and calculus, change (mathematical analysis, analysis). It h ...

or more naturally as inductive types. The canonical term "0" and constructor "S" created by the inductive type closely resembling Peano's axioms.
* Set theory has set-builder notation
In set theory
illustrating the intersection (set theory), intersection of two set (mathematics), sets.
Set theory is a branch of mathematical logic that studies Set (mathematics), sets, which informally are collections of objects. Although any ...

. It can create any set that can be defined. This allows it to create Uncountable set
In mathematics
Mathematics (from Ancient Greek, Greek: ) includes the study of such topics as quantity (number theory), mathematical structure, structure (algebra), space (geometry), and calculus, change (mathematical analysis, analysis). It ...

s. Type theories are syntactic, which limits them to a countably infinite
In mathematics
Mathematics (from Ancient Greek, Greek: ) includes the study of such topics as quantity (number theory), mathematical structure, structure (algebra), space (geometry), and calculus, change (mathematical analysis, analysis). It ...

terms. Additionally, most type theories require computation to always halt and limit themselves to recursively generable terms. As a result, most type theories do not use the Real number
In mathematics
Mathematics (from Greek: ) includes the study of such topics as numbers ( and ), formulas and related structures (), shapes and spaces in which they are contained (), and quantities and their changes ( and ). There is no g ...

s but the Computable number
In mathematics
Mathematics (from Ancient Greek, Greek: ) includes the study of such topics as quantity (number theory), mathematical structure, structure (algebra), space (geometry), and calculus, change (mathematical analysis, analysis). It ...

s.
* In set theory, the Axiom of Choice
In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product#Infinite Cartesian products, Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the a ...

is an axiom and is controversial, particularly when applied to uncountable sets. In type theory, the equivalent statement is a theorem (type) and is provable (inhabited by a term).
* In type theory, proofs are mathematical objects. The type "x+1 = 1+x" cannot be used unless there is a term of the type. That term represents a proof that "x+1 = 1+x". Thus, type theory opens up proofs to be studied as mathematical objects.
Proponents of type theory will also point out its connection to constructive mathematics through the BHK interpretationBHK is a three-letter abbreviation that may refer to:
* BHK interpretation of intuitionistic predicate logic
* Baby hamster kidney cells used in molecular biology
* Bachelor of Human Kinetics (BHk) degree.
* Baltische Historische Kommission, ...

, its connected to logic by the Curry–Howard isomorphism, and its connections to Category theory
Category theory formalizes mathematical structure
In mathematics
Mathematics (from Ancient Greek, Greek: ) includes the study of such topics as quantity (number theory), mathematical structure, structure (algebra), space (geometry), and ...

.
Technical Details

A type theory is a formalmathematical logic
Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal sys ...

. Most logics have judgements meaning "The term $x$ is true." or "The term $x$ is a well-formed formula
In mathematical logic
Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical p ...

.". A type theory has additional judgements that define types and relate terms to types.
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. Some constant symbols will be "0" of the natural numbers, "true" of the Booleans, and axiomatic functions like "S" and "if". Thus some terms are "0", "(S 0)", "(S (S x))", and "if true 0 (S 0)".Judgements

Most type theories have 4 judgements: * "$T$ is a type." * "$t$ is a term of type $T$." * "Type $T\_1$ is equal to type $T\_2$." * "Terms $t\_1$ and $t\_2$ are both of type $T$ and are equal." The judgements can be made under an assumption. Thus, we might say, "assuming $x$ is a term of type "bool" and $y$ is a term of type "nat" , (if x y y) is a term of type "nat"". The mathematical notation for assumptions is a comma-separate list of "''term'' : ''type''" that precede the turnstile symbol '$\backslash vdash$'. Thus, the example statement is formally written: * x:bool, y:nat $\backslash vdash$ (if x y y) : nat If there are no assumptions, there will be nothing to the left of the turnstile. * $\backslash vdash$ S : nat $\backslash to$ nat The list of assumptions is called the "context". It is very common to see the symbol '$\backslash Gamma$' used to represent some or all of the assumptions. Thus, the formal notation for the 4 different judgements is usually: (NOTE: The judgement of equality of terms is where the phrase "judgemental equality" comes from. ) The judgements enforce that every term has a type. The type will restrict which rules can be applied to a term.Rules

A type theory'srules
Rule or ruling may refer to:
Human activity
* The exercise of political
Politics (from , ) is the set of activities that are associated with Decision-making, making decisions in Social group, groups, or other forms of Power (social and ...

are expressed using a horizontal line, with the required input judgements above the line and the resulting judgement below the line. The rule for creating a lambda term is:
$$\backslash begin\; \backslash Gamma\; ,\; a:A\; \backslash vdash\; b\; :\; B\; \backslash \backslash \; \backslash hline\; \backslash Gamma\; \backslash vdash\; (\; \backslash lambda\; a:A\; .\; b\; )\; :\; A\; \backslash to\; B\; \backslash \backslash \; \backslash end$$
The judgements required to create the lambda term go above the line. In this case, only one judgement required. It is that there is some term "b" of some type "B", assuming there is some term "a" of some type "A" and some other assumptions "$\backslash Gamma$". The resulting judgement, which states that the new lambda term has type "A $\backslash to$ B" under the other assumptions $\backslash Gamma$, is below the line.
The rules are syntactic and work by rewriting
In mathematics
Mathematics (from Ancient Greek, Greek: ) includes the study of such topics as quantity (number theory), mathematical structure, structure (algebra), space (geometry), and calculus, change (mathematical analysis, analysis). It ...

.
To generate a particular judgement in type theory, there must be a rule to generate it. Then, there must be rules to generate all of that rule's required inputs. And then rules for all the inputs for those rules. The applied rules form a proof tree. This is usually drawn Gentzen-style, where the target judgement (root) is at the bottom and rules that do not require any inputs (leaves) at the top. (SeNatural_deduction#Proofs_and_type_theory

) An example of a rule that does not require any inputs is one that states there is a term "0" of type "nat": $$\backslash begin\; \backslash hline\; \backslash vdash\; 0\; :\; nat\; \backslash \backslash \; \backslash end$$ A type theory usually has a number of rules, including ones to: * rearrange the assumptions * add an assumption ("weakening") * define reflexivity, symmetry, and transitivity for judgemental equality * define substitution for application of lambda terms, judgemental equality, etc. * ... Each axiomatic type usually comes with 4 different sets 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.

Properties of Type Theories

Terms usually belong to a single type. However, there are set theories that define "subtyping". Computation takes place by repeated application of rules. Many type theories are strongly normalizing, which means that any application of the rules will always result in the same result. However, some are not. In a normalizing type theory, the one-directional computation rules are called "reduction rules" and applying the rules "reduces" the term. If a rule is not one-directional, it is called a "conversion rule".Decision problems

A type theory is naturally associated with thedecision problem
In computability theory and computational complexity theory, a decision problem is a problem that can be posed as a yes–no question of the input values. An example of a decision problem is deciding whether a given natural number is prime. Anot ...

of type inhabitation.
Type inhabitation

The decision problem of ''type inhabitation'' (abbreviated by $\backslash exists\; e.\backslash Gamma\; \backslash vdash\; e\; :\; \backslash tau?$) is: :Given a type environment $\backslash Gamma$ and a type $\backslash tau$, decide whether there exists a term $e$ that can be assigned the type $\backslash tau$ in the type environment $\backslash Gamma$.Girard's paradox
In mathematical logic, System U and System U− are pure type systems, i.e. special forms of a typed lambda calculus
A typed lambda calculus
Lambda calculus (also written as λ-calculus) is a formal system in mathematical logic for expressing com ...

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 synthesisIn computer science
Computer science deals with the theoretical foundations of information, algorithms and the architectures of its computation as well as practical techniques for their application.
Computer science is the study of Algorith ...

(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.
Research Areas

Homotopy type theory
In mathematical logic
Mathematical logic, also called formal logic, is a subfield of mathematics
Mathematics (from Ancient Greek, Greek: ) includes the study of such topics as quantity (number theory), mathematical structure, structure (al ...

differs from intuitionistic type theory
Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory
In mathematics, logic, and computer science, a type system is a formal system in which every term has a "type" which defines its meanin ...

mostly by its handling of the equality type. Recently, there have been proposed "Cubical Type Theory", which is a homotopy type theory with normalization.
Interpretations of Type Theory

Type theory has connections to other areas of mathematics. Proponents of type theory as a foundation often mention these connections as justification for its use.Types are Propositions; Terms are Proofs

When used as a foundation, certain types are interpreted aspropositions
In logic and linguistics, a proposition is the meaning of a declarative sentence (linguistics), sentence. In philosophy, "Meaning (philosophy), meaning" is understood to be a non-linguistic entity which is shared by all sentences with the same mea ...

(statements that can be proven) and a term of the type is a proof of that proposition. Thus, the type "Π x:nat . x+1=1+x" represents that, for any "x" of type "nat", "x+1" and "1+x" are equal. And a term of that type represents its proof.
Curry-Howard Correspondence

TheCurry–Howard correspondence
In programming language theory and proof theory
Proof may refer to:
* Proof (truth), argument or sufficient evidence for the truth of a proposition
* Alcohol proof, a measure of an alcoholic drink's strength
Formal sciences
* Formal proof, a c ...

is the observed similarity between logics and programming languages. The implication in logic, "A $\backslash to$ B" resembles a function from type "A" to type "B". For a variety of logics, the rules are a similar to expression 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 logic operators "for all
In mathematical logic, a universal quantification is a type of Quantification (logic), quantifier, a logical constant which is interpretation (logic), interpreted as "given any" or "for all". It expresses that a predicate (mathematical logic), pre ...

" and " exists" led Per Martin-Löf to invented dependent type theory.
Intuitionistic Logic

When some types are interpreted as propositions, there is a set of common types that can be used to connect them to make a logic out of types. However, that logic is notclassical logic Classical logic (or standard logic) is the intensively studied and most widely used class of deductive logic. Classical logic has had much influence on analytic philosophy, the type of philosophy most often found in the English-speaking world.
Char ...

but intuitionistic logic
Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems of ...

. That is, it does not have the law of excluded middle
In logic
Logic is an interdisciplinary field which studies truth and reasoning
Reason is the capacity of consciously making sense of things, applying logic
Logic (from Ancient Greek, Greek: grc, wikt:λογική, λογική, la ...

nor double negation
Double may refer to:
* Look-alike, a person who closely resembles another person
* Body double, someone who substitutes for the credited actor of a character
* Doppelgänger, ghostly double of a living person
* Polish Enigma doubles, replicatin ...

.
There is a natural relation of types to logical propositions. If "A" is a type representing a proposition, being able to create the function "A $\backslash to\; \backslash top$ " indicates that A has a proof and being able to create the function "A $\backslash to\; \backslash bot$" indicates that A does not have a proof. That is, inhabitable types are proven and uninhabitable types are disproven.
''WARNING: This interpretation can lead to a lot of confusion. A type theory may have ''terms'' "true" and "false" of type "bool", which act like a Boolean logic
In mathematics and mathematical logic, Boolean algebra is the branch of algebra in which the values of the variable (mathematics), variables are the truth values ''true'' and ''false'', usually denoted 1 and 0, respectively. Instead of elementary ...

, and at the same time have ''types'' $\backslash top$ and $\backslash bot$ to represent "true" (provable) and "false" (disproven), as part of a intuitionistic logic for proposition.''
Under this intuitionistic interpretation, there are common types that act as the logical operators:
But under this interpretation, there is no law of excluded middle. That is, there is no term of type Π A . A + (A $\backslash to\; \backslash bot$).
Likewise, there is no double negation. There is no term of type Π A . ((A $\backslash to\; \backslash bot$) $\backslash to\; \backslash bot$) $\backslash to$ A. (Note: Intuitionistic logic does allow $\backslash lnot\; \backslash lnot\; \backslash lnot\; A\; \backslash to\; \backslash lnot\; A$ and there is a term of type (((A $\backslash to\; \backslash bot$) $\backslash to\; \backslash bot$) $\backslash to\; \backslash bot$) $\backslash to$ (A $\backslash to\; \backslash bot$).)
Thus, the logic-of-types is an intuitionistic logic. Type theory is often cited as an implementation of the Brouwer–Heyting–Kolmogorov interpretationIn mathematical logic
Mathematical logic, also called formal logic, is a subfield of mathematics
Mathematics (from Ancient Greek, Greek: ) includes the study of such topics as quantity (number theory), mathematical structure, structure (algeb ...

.
It is possible to include the law of excluded middle and double negation into a type theory, by rule or assumption. However, terms may not compute down to canonical terms and it will interfere with the ability to determine if two terms are judgementally equal to each other.
Constructive Mathematics

Per Martin-Löf proposed his Intuitionistic Type Theory as a foundation forconstructive mathematics
In the philosophy of mathematics, constructivism asserts that it is necessary to find (or "construct") a mathematical object to prove that it exists. In classical mathematics, one can prove the existence of a mathematical object without "finding ...

. Constructive mathematics requires when proving "There exists an $x$ with property P($x$)", there must be a particular $x$ and a proof that it has property "P". In type theory, existence is accomplished using the dependent product type and, its proof, requires a term of that type. For the term $t$, "first $t$" will produce the $x$ and "second $t$" will produce the proof of P($x$).
An example of a non-constructive proof is a "proof by contradiction". The first step is assuming that $x$ does not exist and refuting it by contradiction. The conclusion from that step is "it is not the case that $x$ does not exist". The last step is, by double negation, concluding that $x$ exists. To be clear, constructive mathematics still allows "refute by contradiction". It can prove that "it is not the case that $x$ does not exist". But constructive mathematics does not allow the last step of removing the double negation to conclude that $x$ exists.
Constructive mathematics has often used intutionistic logic, as evidenced by the Brouwer–Heyting–Kolmogorov interpretationIn mathematical logic
Mathematical logic, also called formal logic, is a subfield of mathematics
Mathematics (from Ancient Greek, Greek: ) includes the study of such topics as quantity (number theory), mathematical structure, structure (algeb ...

.
Most of the type theories proposed as foundations are constructive. 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 (type theory), canonicity and parametricity.
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 category, 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 category, locally cartesian closed categories correspond to Martin-Löf type theory, 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
In mathematical logic
Mathematical logic, also called formal logic, is a subfield of mathematics
Mathematics (from Ancient Greek, Greek: ) includes the study of such topics as quantity (number theory), mathematical structure, structure (al ...

attempts to combine type theory and category theory. It focuses on equalities, especially equalities between types.
List of Type Theories

Major

* Simply typed lambda calculus which is ahigher-order logic
In mathematics
Mathematics (from Ancient Greek, Greek: ) includes the study of such topics as quantity (number theory), mathematical structure, structure (algebra), space (geometry), and calculus, change (mathematical analysis, analysis). It h ...

* calculus of constructions#REDIRECT Calculus of constructions
{{Redirect category shell, 1=
{{R from other capitalisation
...

and its derivatives
Minor

* Automath * ST type theory * UTT (Luo's Unified Theory of dependent Types) * some forms of combinatory logic * others defined in thelambda cube
In mathematical logic
Mathematical logic, also called formal logic, is a subfield of mathematics
Mathematics (from Ancient Greek, Greek: ) includes the study of such topics as quantity (number theory), mathematical structure, structure ( ...

(also known as pure type systems)
* others under the name typed lambda calculus
Active Research

*Homotopy type theory
In mathematical logic
Mathematical logic, also called formal logic, is a subfield of mathematics
Mathematics (from Ancient Greek, Greek: ) includes the study of such topics as quantity (number theory), mathematical structure, structure (al ...

explores equality of types
*nlab:cubical+type+theory, Cubical Type Theory is an implementation 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 developedhomotopy type theory
In mathematical logic
Mathematical logic, also called formal logic, is a subfield of mathematics
Mathematics (from Ancient Greek, Greek: ) includes the study of such topics as quantity (number theory), mathematical structure, structure (al ...

.
Mathematicians working in category theory already had difficulty working with the widely accepted foundation of Zermelo–Fraenkel set theory
In set theory
illustrating the intersection of two sets
Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set ...

. 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 Automated proof checking, proof checkers, interactive proof assistants, and Automated theorem proving, 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: * Logical framework, LF is used by Twelf, often to define other type theories; * many type theories which fall underhigher-order logic
In mathematics
Mathematics (from Ancient Greek, Greek: ) includes the study of such topics as quantity (number theory), mathematical structure, structure (algebra), space (geometry), and calculus, change (mathematical analysis, analysis). It h ...

are used by the HOL (proof assistant), HOL family of provers and Prototype Verification System, PVS;
* computational type theory is used by NuPRL;
* calculus of constructions#REDIRECT Calculus of constructions
{{Redirect category shell, 1=
{{R from other capitalisation
...

and its derivatives are used by Coq
Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps find formal proofs, and extracts a certified program from the constructive proo ...

, Matita, and Lean
Lean, leaning or LEAN may refer to:
Business practices
* Lean thinking, a business methodology adopted in various fields
** Lean construction, an adaption of lean manufacturing principles to the design and construction process
** Lean government, ...

;
* UTT (Luo's Unified Theory of dependent Types) is used by Agda (programming language), Agda which is both a programming language and proof assistant
Many type theories are supported by LEGO (proof assistant), LEGO and Isabelle (proof assistant), Isabelle. Isabelle also supports foundations besides type theories, such as Zermelo–Fraenkel set theory, ZFC. Mizar system, Mizar is an example of a proof system that only supports set theory.
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 (compilers), semantic analysis phase of compiler, has a connection to type theory. A prime example is Agda (programming language), Agda, a programming language which uses UTT (Luo's Unified Theory of dependent Types) for its type system. The programming language ML (programming language), ML was developed for manipulating type theories (see Logic for Computable Functions, LCF) and its own type system was heavily influenced by them.Linguistics

Type theory is also widely used in formal semantics (linguistics), 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 $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 $\backslash langle\; a,b\backslash rangle$; * nothing except the basic types, and what can be constructed from them by means of the previous clause are types. A complex type $\backslash langle\; a,b\backslash rangle$ is the type of Function (mathematics), functions from entities of type $a$ to entities of type $b$. Thus one has types like $\backslash langle\; e,t\backslash 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 $\backslash langle\backslash langle\; e,t\backslash rangle,t\backslash 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 Generalized quantifier, natural language quantifiers, like '' everybody'' or '' nobody'' (Richard Montague, Montague 1973, Jon Barwise, 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.See also

* Type system, which is a programming language feature to find/avoid bugs * Foundations of mathematicsExternal links

Introductory Material

Type Theory at nLab

which has articles on many topics.

Intuitionistic Type Theory

article at the Stanford Encyclopedia of Philosophy

Lambda Calculus with Types

book by Henk Barendregt

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. * [ftp://ftp.cs.cornell.edu/pub/nuprl/doc/book.ps.gz The Nuprl Book]:

Introduction to Type Theory.

of summer schools 2005–2008 ** Th

has introductory lectures

many lectures and some notes.

includin

Robert Harper's talks on YouTube

Further reading

* * * Covers type theory in depth, including polymorphic and dependent type extensions. Gives categorical semantics. * * Provides a historical survey of the developments of the theory of types with a focus on the decline of the theory as a foundation of mathematics over the four decades following the publication of the second edition of 'Principia Mathematica'. * Intended as a type theory counterpart of Paul Halmos's (1960) ''Naive Set Theory (book), Naïve Set Theory'' * * * A good introduction to simple type theory for computer scientists; the system described is not exactly Church's STT thoughBook review

* * *

References

{{DEFAULTSORT:Type Theory Type theory, Systems of formal logic Hierarchy