Type theory

Concept in mathematical logic

In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a foundation of mathematics. Two influential type theories that were proposed as foundations are Alonzo Church's typed λ-calculus and Per Martin-Löf's intuitionistic type theory. Most computerized proof-writing systems use a type theory for their foundation. A common one is Thierry Coquand's Calculus of Inductive Constructions.

## Contents

* 1 History
* 2 Introduction
* 2.1 Basics
* 2.1.1 Terms and types
* 2.1.2 Computation
* 2.2 Functions
* 2.2.1 Lambda terms
* 2.2.2 Dependent typing
* 2.2.3 Universes
* 2.3 Common "by rule" types and terms
* 2.3.1 Empty type
* 2.3.2 Unit type
* 2.3.3 Boolean type
* 2.3.4 Product type
* 2.3.5 Sum type
* 2.3.6 Natural numbers
* 2.3.7 Identity type
* 2.3.8 Inductive types
* 3 Differences from set theory
* 4 Technical details
* 4.1 Terms
* 4.2 Judgements
* 4.3 Rules
* 4.4 Properties of type theories
* 4.5 Axioms
* 4.6 Decision problems
* 4.6.1 Type inhabitation
* 4.6.2 Type inference
* 4.7 Research areas
* 5 Interpretations
* 5.1 Types are propositions; terms are proofs
* 5.2 Curry-Howard correspondence
* 5.3 Intuitionistic logic
* 5.4 Constructive mathematics
* 5.5 Category theory
* 6 List of type theories
* 6.1 Major
* 6.2 Minor
* 6.3 Active research
* 7 Applications
* 7.1 Mathematical foundations
* 7.2 Proof assistants
* 7.3 Programming languages
* 7.4 Linguistics
* 7.5 Social sciences
* 8 See also
* 9 Further reading
* 10 Notes
* 11 References
* 12 External links
* 12.1 Introductory material
* 12.2 Advanced material

## History[edit | edit source]

Main article: History of type theory

Type theory was created to avoid a paradox in a mathematical foundation based on naive set theory and formal logic. Russell's paradox, which was discovered by Bertrand Russell, 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" both of which featured prominently in Whitehead and Russell's Principia Mathematica published between 1910 and 1913. This system avoided Russell's paradox by creating a hierarchy of types and then assigning each concrete mathematical entity to a type. Entities of a given type are built exclusively of subtypes of that type,[a] thus preventing an entity from being defined using itself. Russell's theory of types ruled out the possibility of a set being a member of itself.

Types were not always used in logic. There were other techniques to avoid Russell's paradox.[3] Types did gain a hold when used with one particular logic, Alonzo Church's lambda calculus.

The most famous early example is Church's simply typed lambda calculus. Church's theory of types[4] 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.

The phrase "type theory" now generally refers to a typed system based around lambda calculus. One influential system is Per Martin-Löf's intuitionistic type theory, which was proposed as a foundation for constructive mathematics. Another is Thierry Coquand's calculus of constructions, which is used as the foundation by Coq, Lean, and other "proof assistants" (computerized proof writing programs). Type theories are an area of active research, as demonstrated by homotopy type theory.

## Introduction[edit | edit source]

There are many type theories, which makes it difficult to produce a comprehensive taxonomy; this article is not an exhaustive categorization. What follows is an introduction for those unfamiliar with type theory, covering some of the major approaches.

### Basics[edit | edit source]

#### Terms and types[edit | edit source]

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 the Natural numbers, often written as "Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbb N} " or "nat". Another is Boolean logic 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 takes 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 "Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x + y} " instead of "add Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x} Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle 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[edit | edit source]

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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \twoheadrightarrow} 5 : nat". The computation is mechanical, accomplished by rewriting 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[edit | edit source]

In type theory, functions are terms. Functions can either be lambda terms or defined "by rule".

#### Lambda terms[edit | edit source]

A lambda term looks like "(λ variablename : type1 . term)" and has type "type1 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \to} type2". The type "type1 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \to} type2" indicates that the lambda term is a function that 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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \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 : nat

#### Dependent typing[edit | edit source]

Dependent typing is when the type returned by a function depends on the value of its argument. For example, when a type theory has a rule that defines the type "bool", it also 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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \to} C Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \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. In actuality, "if a B C" isn't defined using "if", but that gets into details too complicated for this introduction.

Because the type can contain computation, dependent typing is amazingly powerful. When mathematicians say "there exists a number Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x} such that Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x} is prime" or "there exists a number Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x} such that property Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle P(x)} holds", it can be expressed as a dependent type. That is, the property is proven for the specific "Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle 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 on dependent typing and the lambda cube for more information.

#### Universes[edit | edit source]

Π-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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle U} . Sometimes there is a hierarchy of universes, with "Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle U_0} : Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle U_1} ", "Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle U_1} : Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle U_2} ", etc..

If a universe contains itself, it can lead to paradoxes like Girard's Paradox.

For example:[5]

> The openendedness of Martin-Löf type theory is particularly manifest in the introduction of so-called universes. Type universes encapsulate the informal notion of reflection whose role may be explained as follows. During the course of developing a particular formalization of type theory, the type theorist may look back over the rules for types, say C, which have been introduced hitherto and perform the step of recognizing that they are valid according to Martin-Löf’s informal semantics of meaning explanation. This act of ‘introspection’ is an attempt to become aware of the conceptions which have governed our constructions in the past. It gives rise to a “reflection principle which roughly speaking says whatever we are used to doing with types can be done inside a universe” (Martin-Löf 1975, 83). On the formal level, this leads to an extension of the existing formalization of type theory in that the type forming capacities of C become enshrined in a type universe UC mirroring C.

### Common "by rule" types and terms[edit | edit source]

Type theories are defined by their rules of inference. There are rules for a "functional core", described above, and rules that create types and terms. Below is a non-exhaustive list of common types and their associated terms.

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[edit | edit source]

The empty type has no terms. The type is usually written "Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \bot} " or "Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbb 0} ".

It is used to show that something is uncomputable. If for a type "A", you can create a function of type "A Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \to \bot} ", you know that "A" has no terms. An example for the type "A" might be "there exists a number Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x} such that both Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x} is even and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle 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[edit | edit source]

The unit type has exactly 1 canonical term. The type is written "Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \top} " or "Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \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 "Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \top \to} A", you know that "A" has one or more terms. When a type has at least 1 term, we say it is "inhabited".

#### Boolean type[edit | edit source]

The Boolean type has exactly 2 canonical terms. The type is usually written "bool" or "Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbb B} " or "Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbb 2} ". The canonical terms are usually "true" and "false".

The Boolean type is defined with an eliminator function "if" such that:

* if true b c Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \twoheadrightarrow} b
* if false b c Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \twoheadrightarrow} c

#### Product type[edit | edit source]

The product type has terms that are ordered pairs. For types "A" and "B", the product type is written "A Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \times} B". Canonical terms are created by the constructor 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 eliminator functions "first" and "second" such that:

* first (pair a b) Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \twoheadrightarrow} a
* second (pair a b) Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \twoheadrightarrow} b

Besides ordered pairs, this type is used for the logical operator "and", because it holds an "A" and a "B". It is also used for intersection, 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 "Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Sigma} a:A . B(a)" where "B" has type "A Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \to} U". It is useful when showing existence of an "a" with property "B(a)".

#### Sum type[edit | edit source]

The sum type 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 an eliminator function "match" such that for a type "C" and functions "f : A Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \to} C" and "g : B Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \to} C":

* match (injectionLeft a) C f g Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \twoheadrightarrow} (f a)
* match (injectionRight b) C f g Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \twoheadrightarrow} (g b)

The sum type is used for logical or and for union.

#### Natural numbers[edit | edit source]

The natural numbers are usually implemented in the style of Peano Arithmetic. There is a canonical term, "0 : nat" for zero. Canonical values larger than zero use the constructor function "S : nat Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \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 are defined with an eliminator function "R" that uses recursion to define a function for all nats. It takes a function "P : nat Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \twoheadrightarrow} PZ
* R P PZ PS (S Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle n} ) Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \twoheadrightarrow} PS (R P PZ PS Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle n} )

The function "add", that was used earlier, can be defined using "R".

* add : natFailed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \to} natFailed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \to} nat ::= R (λ n:nat . natFailed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \to} nat) (λ n:nat . n) (λ g:natFailed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \to} nat . (λ m:nat . S (g m)))

#### Identity type[edit | edit source]

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 eliminator 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 and transitive.

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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \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.

#### Inductive types[edit | edit source]

Inductive types is a way to create a large variety of types. In fact, all the types described above and more can be defined using the rules of inductive types. Once the type's constructors are specified, the eliminator functions and 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[edit | edit source]

The traditional foundation for mathematics has been set theory paired with a logic. The most common one cited is Zermelo–Fraenkel set theory, known as "ZF" or, with the Axiom of choice, "ZFC". Type theories differ from this foundation in a number of ways.

* Set theory has both rules and axioms, while type theories only have rules. Set theories are built on top of logic. Thus, ZFC is defined by both the rules of first-order logic and its own axioms. (An axiom is a logical statement accepted as true without a logical derivation.) Type theories, in general, do not have axioms and are defined by their rules of inference.
* Set theory and logic have the law of excluded middle. 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, 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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x} is paired with a proof that the subset's property holds for Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle 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 numbers.) Type theory can encode numbers as functions using Church encoding or more naturally as inductive types. The constructors "0" and "S" created by the inductive type closely resemble Peano's axioms.
* Set theory has set-builder notation. It can create any set that can be defined. This allows it to create Uncountable sets. Type theories are syntactic, which limits them to a countably infinite 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 numbers but the Computable numbers.
* In set theory, the Axiom of Choice 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 interpretation, its connected to logic by the Curry–Howard isomorphism, and its connections to Category theory.

## Technical details[edit | edit source]

A type theory is a mathematical logic. It is a collection of rules of inference that result in judgements. Most logics have judgements meaning "The term Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x} is true." or "The term Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x} is a well-formed formula."[6]. A type theory has additional judgements that define types and relate terms to types.

### Terms[edit | edit source]

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 functions like "S" and "if". Thus some terms are "0", "(S 0)", "(S (S x))", and "if true 0 (S 0)".

### Judgements[edit | edit source]

Most type theories have 4 judgements:

* "Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle T} is a type."
* "Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t} is a term of type Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle T} ."
* "Type Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle T_1} is equal to type Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle T_2} ."
* "Terms Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t_1} and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t_2} are both of type Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle T} and are equal."

The judgements can be made under an assumption. Thus, we might say, "assuming Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x} is a term of type "bool" and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle 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 'Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \vdash} '. Thus, the example statement is formally written:

* x:bool, y:nat Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \vdash} (if x y y) : nat

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

* Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \vdash} S : nat Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \to} nat

The list of assumptions is called the "context". It is very common to see the symbol 'Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Gamma} ' used to represent some or all of the assumptions. Thus, the formal notation for the 4 different judgements is usually:

Formal notation for judgements | Description

|

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Gamma \vdash T} Type | Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle T} is a type (under assumptions Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Gamma} ).
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Gamma \vdash t : T} | Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t} is a term of type Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle T} (under assumptions Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Gamma} ).
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Gamma \vdash T_1 = T_2 } | Type Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle T_1} is equal to type Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle T_2} (under assumptions Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Gamma} ).
Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Gamma \vdash t_1 = t_2 : T } | Terms Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t_1} and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t_2} are both of type Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle T} and are equal (under assumptions Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Gamma} ).

(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[edit | edit source]

A type theory's rules say what judgements can be made, based on the existence of other judgements. The rules 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: Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \begin{array}{c} \Gamma , a:A \vdash b : B \\\ \hline \Gamma \vdash ( \lambda a:A . b ) : A \to B \\\ \end{array} }

The judgements required to create the lambda term go above the line. In this case, only one judgement is 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 "Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Gamma} ". (Note: "Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Gamma} " "a", "A", "b", and "B" are all metavariables in the rule.) The resulting judgement goes below the line. This rule's resulting judgement states that the new lambda term has type "A Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \to} B" under the other assumptions Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Gamma} .

The rules are syntactic and work by rewriting. Thus, the metavariables like "Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Gamma} ", "a", "A", etc. may actually consist of complex terms that contain many function applications, not just single symbols.

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,[7] where the target judgement (root) is at the bottom and rules that do not require any inputs (leaves) at the top. (See 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":

Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \begin{array}{c} \hline \vdash 0 : nat \\\ \end{array} }

A type theory usually has a number of rules, including ones to:

* create a context
* add an assumption to the context ("weakening")
* rearrange the assumptions
* use an assumption to create a variable
* define reflexivity, symmetry and transitivity for judgemental equality
* define substitution for application of lambda terms
* all the interactions of equality, substitution, etc.
* define universes

Also, for each "by rule" type, there are 4 different kinds of rules

* "type formation" rules say how to create the type
* "term introduction" rules define the canonical terms and constructor functions, like "pair" and "S".
* "term elimination" rules define the other functions like "first", "second", and "R".
* "computation" rules specify how computation is performed with the type-specific functions.

Examples of rules:

* Rules to Martin-Löf's Intuitionistic Type Theory
* Appendix A.2 of Homotopy Type Theory book

### Properties of type theories[edit | edit source]

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 order of applying the rules will always end 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".

Some combinations of types are equivalent to other combinations of types. When functions are considered "exponentiation", the combinations of types can be written similar to algebraic identities.[8] Thus, Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle {\mathbb 0} + A \cong A} , Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle {\mathbb 1} \times A \cong A} , Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle {\mathbb 1} + {\mathbb 1} \cong {\mathbb 2}} , Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A^{B+C} \cong A^B \times A^C} , Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A^{B\times C} \cong (A^B)^C} .

### Axioms[edit | edit source]

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

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

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

Some commonly encountered axioms are:

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

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

### Decision problems[edit | edit source]

A type theory is naturally associated with the decision problem of type inhabitation.[12]

#### Type inhabitation[edit | edit source]

Main article: Type inhabitation

The decision problem of type inhabitation (abbreviated by Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \exists e.\Gamma \vdash e : \tau?} ) is:

Given a type environment Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Gamma} and a type Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \tau} , decide whether there exists a term Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle e} that can be assigned the type Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \tau} in the type environment Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Gamma} .

Girard's paradox shows that type inhabitation is strongly related to the consistency of a type system with Curry–Howard correspondence. To be sound, such a system must have uninhabited types.

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

#### Type inference[edit | edit source]

Main article: Type inference

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

### Research areas[edit | edit source]

Homotopy type theory differs from intuitionistic type theory mostly by its handling of the equality type. In 2016 cubical type theory was proposed, which is a homotopy type theory with normalization.[14][11]

## Interpretations[edit | edit source]

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[edit | edit source]

When used as a foundation, certain types are interpreted as propositions (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[edit | edit source]

The Curry–Howard correspondence is the observed similarity between logics and programming languages. The implication in logic, "A Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \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" and "exists" led Per Martin-Löf to invent dependent type theory.

### Intuitionistic logic[edit | edit source]

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 not classical logic but intuitionistic logic. That is, it does not have the law of excluded middle nor double negation.

There is a natural relation of types to logical propositions. If "A" is a type representing a proposition, being able to create a function of type "Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \top \to } A" indicates that A has a proof and being able to create the function "A Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \to \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, and at the same time have types Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \top} and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \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:

Logic Name | Logic Notation | Type Notation | Type Name

|
|
|

True | Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \top} | Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \top} | Unit Type
False | Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \bot} | Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \bot} | Empty Type
Not | Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \neg A} | Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A \to \bot} | Function to Empty Type
Implication | Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A \to B} | Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A \to B} | Function
And | Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A \land B} | Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A \times B} | Product Type
Or | Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A \lor B} | Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A + B} | Sum Type
For All | Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \forall a \in A, P(a)} | Π a : A . P(a) | Dependent Function
Exists | Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \exists a \in A, P(a)} | Σ a : A . P(a) | Dependent Product Type

But under this interpretation, there is no law of excluded middle. That is, there is no term of type Π A . A + (A Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \to \bot} ).

Likewise, there is no double negation. There is no term of type Π A . ((A Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \to \bot} ) Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \to \bot} ) Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \to } A. (Note: Intuitionistic logic does allow Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \lnot \lnot \lnot A \to \lnot A} and there is a term of type (((A Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \to \bot} ) Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \to \bot} ) Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \to \bot} ) Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \to } (A Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \to \bot} ).)

Thus, the logic-of-types is an intuitionistic logic. Type theory is often cited as an implementation of the Brouwer–Heyting–Kolmogorov interpretation.

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[edit | edit source]

Per Martin-Löf proposed his intuitionistic type theory as a foundation for constructive mathematics. Constructive mathematics requires when proving "There exists an Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x} with property P(Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x} )", there must be a particular Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle 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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t} , "first Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t} " will produce the Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x} and "second Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t} " will produce the proof of P(Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x} ).

An example of a non-constructive proof is a "proof by contradiction". The first step is assuming that Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x} does not exist and refuting it by contradiction. The conclusion from that step is "it is not the case that Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x} does not exist". The last step is, by double negation, concluding that Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x} exists. To be clear, constructive mathematics still allows "refute by contradiction". It can prove that "it is not the case that Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x} does not exist". But constructive mathematics does not allow the last step of removing the double negation to conclude that Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x} exists.[15]

Constructive mathematics has often used intutionistic logic, as evidenced by the Brouwer–Heyting–Kolmogorov interpretation.

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 and parametricity.

### Category theory[edit | edit source]

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:[16]

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

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

Homotopy type theory attempts to combine type theory and category theory. It focuses on equalities, especially equalities between types.

## List of type theories[edit | edit source]

### Major[edit | edit source]

* 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[edit | edit source]

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

### Active research[edit | edit source]

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

## Applications[edit | edit source]

### Mathematical foundations[edit | edit source]

This section needs expansion. You can help by adding to it. (May 2008)

|

The first computer proof assistant, called Automath, used type theory to encode mathematics on a computer. Martin-Löf specifically developed intuitionistic type theory to encode all mathematics to serve as a new foundation for mathematics. There is ongoing research into mathematical foundations using homotopy type theory.

Mathematicians working in category theory already had difficulty working with the widely accepted foundation of Zermelo–Fraenkel set theory. This led to proposals such as Lawvere's Elementary Theory of the Category of Sets (ETCS).[17] 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[edit | edit source]

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

* LF is used by Twelf, often to define other type theories;
* many type theories which fall under higher-order logic are used by the HOL family of provers and PVS;
* computational type theory is used by NuPRL;
* calculus of constructions and its derivatives are used by Coq, Matita, and Lean;
* UTT (Luo's Unified Theory of dependent Types) is used by Agda which is both a programming language and proof assistant

Many type theories are supported by LEGO and Isabelle. Isabelle also supports foundations besides type theories, such as ZFC. Mizar is an example of a proof system that only supports set theory.

### Programming languages[edit | edit source]

Any static program analysis, such as the type checking algorithms in the semantic analysis phase of compiler, has a connection to type theory. A prime example is Agda, a programming language which uses UTT (Luo's Unified Theory of dependent Types) for its type system.

The programming language ML was developed for manipulating type theories (see LCF) and its own type system was heavily influenced by them.

### Linguistics[edit | edit source]

Type theory is also widely used in formal theories of semantics of natural languages,[18][19] especially Montague grammar[20] 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 Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle e} and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle t} for individuals and truth-values, respectively, and defines the set of types recursively as follows:

* if Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle a} and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle b} are types, then so is Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \langle a,b\rangle} ;
* nothing except the basic types, and what can be constructed from them by means of the previous clause are types.

A complex type Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \langle a,b\rangle} is the type of functions from entities of type Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle a} to entities of type Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle b} . Thus one has types like Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \langle e,t\rangle} which are interpreted as elements of the set of functions from entities to truth-values, i.e. indicator functions of sets of entities. An expression of type Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \langle\langle e,t\rangle,t\rangle} is a function from sets of entities to truth-values, i.e. a (indicator function of a) set of sets. This latter type is standardly taken to be the type of natural language quantifiers, like  everybody or  nobody (Montague 1973, Barwise and Cooper 1981).[full citation needed]

### Social sciences[edit | edit source]

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[edit | edit source]

* Foundations of mathematics

## Further reading[edit | edit source]

* Aarts, C.; Backhouse, R.; Hoogendijk, P.; Voermans, E.; van der Woude, J. (December 1992). "A Relational Theory of Datatypes". Technische Universiteit Eindhoven.
* Andrews B., Peter (2002). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof (2nd ed.). Kluwer. ISBN 978-1-4020-0763-7.
* Jacobs, Bart (1999). Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics. Vol. 141\. Elsevier. ISBN 978-0-444-50170-7. Covers type theory in depth, including polymorphic and dependent type extensions. Gives categorical semantics.
* Cardelli, Luca (1996). "Type Systems". In Tucker, Allen B. (ed.). The Computer Science and Engineering Handbook. CRC Press. pp. 2208–36. ISBN 9780849329098.
* Collins, Jordan E. (2012). A History of the Theory of Types: Developments After the Second Edition of 'Principia Mathematica'. Lambert Academic Publishing. hdl:11375/12315. ISBN 978-3-8473-2963-3. 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'.
* Constable, Robert L. (2012) [2002]. "Naïve Computational Type Theory" (PDF). In Schwichtenberg, H.; Steinbruggen, R. (eds.). Proof and System-Reliability. Nato Science Series II. Vol. 62\. Springer. pp. 213–259. ISBN 9789401004138. Archived (PDF) from the original on 2022-10-09. Intended as a type theory counterpart of Paul Halmos's (1960) Naïve Set Theory
* Coquand, Thierry (2018) [2006]. "Type Theory". Stanford Encyclopedia of Philosophy.
* Thompson, Simon (1991). Type Theory and Functional Programming. Addison–Wesley. ISBN 0-201-41667-0.
* Hindley, J. Roger (2008) [1995]. Basic Simple Type Theory. Cambridge University Press. ISBN 978-0-521-05422-5. A good introduction to simple type theory for computer scientists; the system described is not exactly Church's STT though. Book review
* Kamareddine, Fairouz D.; Laan, Twan; Nederpelt, Rob P. (2004). A modern perspective on type theory: from its origins until today. Springer. ISBN 1-4020-2334-0.
* Ferreirós, José; Domínguez, José Ferreirós (2007). "X. Logic and Type Theory in the Interwar Period". Labyrinth of thought: a history of set theory and its role in modern mathematics (2nd ed.). Springer. ISBN 978-3-7643-8349-7.
* Laan, T.D.L. (1997). The evolution of type theory in logic and mathematics (PDF) (PhD). Eindhoven University of Technology. doi:10.6100/IR498552. ISBN 90-386-0531-5. Archived (PDF) from the original on 2022-10-09.

## Notes[edit | edit source]

1. ^ In Julia's type system, for example, abstract types have no subtype[1]: 110 but concrete types are provided for "documentation, optimization, and dispatch".[2]

## References[edit | edit source]

1. ^ Balbaert, Ivo (2015) Getting Started With Julia Programming ISBN 978-1-78328-479-5
2. ^ docs.julialang.org v.1 Types
3. ^ Stanford Encyclopedia of Philosophy (rev. Mon Oct 12, 2020) Russell’s Paradox 3\. Early Responses to the Paradox
4. ^ Church, Alonzo (1940). "A formulation of the simple theory of types". The Journal of Symbolic Logic. 5 (2): 56–68. doi:10.2307/2266170. JSTOR 2266170. S2CID 15889861.
5. ^ Rathjen, Michael (October 2005). "The Constructive Hilbert Program and the Limits of Martin-Löf Type Theory". Synthese. 147: 81–120. doi:10.1007/s11229-004-6208-4. Retrieved September 21, 2022.
6. ^ Bauer, Andrej. "What exactly is a judgement?". mathoverflow. Retrieved 29 December 2021.
7. ^ Smith, Peter. "Types of proof system" (PDF). logicmatters.net. Archived (PDF) from the original on 2022-10-09. Retrieved 29 December 2021.
8. ^ Milewski, Bartosz. "Programming with Math (Exploring Type Theory)". YouTube.
9. ^ "Axioms and Computation". Theorem Proving in Lean. Retrieved 21 January 2022.
10. ^ "Axiom K". nLab.
11. ^ a b Cohen, Cyril; Coquand, Thierry; Huber, Simon; Mörtberg, Anders (2016). "Cubical Type Theory: a constructive interpretation of the univalence axiom" (PDF). 21st International Conference on Types for Proofs and Programs (TYPES 2015). arXiv:1611.02108. doi:10.4230/LIPIcs.CVIT.2016.23 (inactive 31 July 2022). Archived (PDF) from the original on 2022-10-09.`{{cite journal}}`: CS1 maint: DOI inactive as of July 2022 (link)
12. ^ Henk Barendregt; Wil Dekkers; Richard Statman (20 June 2013). Lambda Calculus with Types. Cambridge University Press. p. 66\. ISBN 978-0-521-76614-2.
13. ^ Heineman, George T.; Bessai, Jan; Düdder, Boris; Rehof, Jakob (2016). "A long and winding road towards modular synthesis". Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. ISoLA 2016. Lecture Notes in Computer Science. Vol. 9952\. Springer. pp. 303–317. doi:10.1007/978-3-319-47166-2_21. ISBN 978-3-319-47165-5.
14. ^ Sterling, Jonathan; Angiuli, Carlo (2021-06-29). "Normalization for Cubical Type Theory". 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Rome, Italy: IEEE: 1–15. arXiv:2101.11479. doi:10.1109/LICS52264.2021.9470719. ISBN 978-1-6654-4895-6. S2CID 231719089.
15. ^ "proof by contradiction". nlab. Retrieved 29 December 2021.
16. ^ Bell, John L. (2012). "Types, Sets and Categories" (PDF). In Kanamory, Akihiro (ed.). Sets and Extensions in the Twentieth Century. Handbook of the History of Logic. Vol. 6\. Elsevier. ISBN 978-0-08-093066-4.
17. ^ ETCS at the nLab
18. ^ Chatzikyriakidis, Stergios; Luo, Zhaohui (2017-02-07). Modern Perspectives in Type-Theoretical Semantics. Springer. ISBN 978-3-319-50422-3.
19. ^ Winter, Yoad (2016-04-08). Elements of Formal Semantics: An Introduction to the Mathematical Theory of Meaning in Natural Language. Edinburgh University Press. ISBN 978-0-7486-7777-1.
20. ^ Cooper, Robin. "Type theory and semantics in flux." Handbook of the Philosophy of Science 14 (2012): 271-323.

## External links[edit | edit source]

### Introductory material[edit | edit source]

* 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
* Calculus of Constructions / Typed Lambda Calculus textbook style paper by Helmut Brandl
* Intuitionistic Type Theory notes by Per Martin-Löf
* Programming in Martin-Löf ’s Type Theory book
* Homotopy Type Theory book, which proposed homotopy type theory as a mathematical foundation.

### Advanced material[edit | edit source]

* Robert L. Constable (ed.). "Computational type theory". Scholarpedia.
* 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
* Oregon Programming Languages Summer School, many lectures and some notes.
* Summer 2013 lectures including Robert Harper's talks on YouTube
* Summer 2015 Types, Logic, Semantics, and Verification
* Andrej Bauer's blog

* v
* t
* e

Computer science

Note: This template roughly follows the 2012 ACM Computing Classification System.

Hardware|

* Printed circuit board
* Peripheral
* Integrated circuit
* Very Large Scale Integration
* Systems on Chip (SoCs)
* Energy consumption (Green computing)
* Electronic design automation
* Hardware acceleration

File:Computer Retro.svg

Computer systems organization|

* Computer architecture
* Embedded system
* Real-time computing
* Dependability

Networks|

* Network architecture
* Network protocol
* Network components
* Network scheduler
* Network performance evaluation
* Network service

Software organization|

* Interpreter
* Middleware
* Virtual machine
* Operating system
* Software quality

Software notations and tools|

* Programming paradigm
* Programming language
* Compiler
* Domain-specific language
* Modeling language
* Software framework
* Integrated development environment
* Software configuration management
* Software library
* Software repository

Software development|

* Control variable
* Software development process
* Requirements analysis
* Software design
* Software construction
* Software deployment
* Software engineering
* Software maintenance
* Programming team
* Open-source model

Theory of computation|

* Model of computation
* Formal language
* Automata theory
* Computability theory
* Computational complexity theory
* Logic
* Semantics

Algorithms|

* Algorithm design
* Analysis of algorithms
* Algorithmic efficiency
* Randomized algorithm
* Computational geometry

Mathematics of computing|

* Discrete mathematics
* Probability
* Statistics
* Mathematical software
* Information theory
* Mathematical analysis
* Numerical analysis
* Theoretical computer science

Information systems|

* Database management system
* Information storage systems
* Enterprise information system
* Social information systems
* Geographic information system
* Decision support system
* Process control system
* Multimedia information system
* Data mining
* Digital library
* Computing platform
* Digital marketing
* World Wide Web
* Information retrieval

Security|

* Cryptography
* Formal methods
* Security services
* Intrusion detection system
* Hardware security
* Network security
* Information security
* Application security

Human–computer interaction|

* Interaction design
* Social computing
* Ubiquitous computing
* Visualization
* Accessibility

Concurrency|

* Concurrent computing
* Parallel computing
* Distributed computing
* Multithreading
* Multiprocessing

Artificial intelligence|

* Natural language processing
* Knowledge representation and reasoning
* Computer vision
* Automated planning and scheduling
* Search methodology
* Control method
* Philosophy of artificial intelligence
* Distributed artificial intelligence

Machine learning|

* Supervised learning
* Unsupervised learning
* Reinforcement learning
* Multi-task learning
* Cross-validation

Graphics|

* Animation
* Rendering
* Image manipulation
* Graphics processing unit
* Mixed reality
* Virtual reality
* Image compression
* Solid modeling

Applied computing|

* E-commerce
* Enterprise software
* Computational mathematics
* Computational physics
* Computational chemistry
* Computational biology
* Computational social science
* Computational engineering
* Computational healthcare
* Digital art
* Electronic publishing
* Cyberwarfare
* Electronic voting
* Video games
* Word processing
* Operations research
* Educational technology
* Document management

* Category
* Outline Outline
* Project pageProject
* Commons page Commons

* v
* t
* e

Mathematical logic

General|

* Axiom
* list
* Cardinality
* First-order logic
* Formal proof
* Formal semantics
* Foundations of mathematics
* Information theory
* Logical consequence
* Model
* Set
* Theorem
* Theory
* Type theory

Theorems (list)
& Paradoxes|

* Gödel's completeness and incompleteness theorems
* Tarski's undefinability
* Banach–Tarski paradox
* Cantor's theorem, paradox and diagonal argument
* Compactness
* Halting problem
* Lindström's
* Löwenheim–Skolem
* Russell's paradox

Logics|

| Traditional|

* Classical logic
* Logical truth
* Tautology
* Proposition
* Inference
* Logical equivalence
* Consistency
* Equiconsistency
* Argument
* Soundness
* Validity
* Syllogism
* Square of opposition
* Venn diagram

|

Propositional|

* Boolean algebra
* Boolean functions
* Logical connectives
* Propositional calculus
* Propositional formula
* Truth tables
* Many-valued logic
* 3
* Finite
* ∞

Predicate|

* First-order
* Second-order
* Monadic
* Higher-order
* Free
* Quantifiers
* Predicate
* Monadic predicate calculus

Set theory|

* Set
* Hereditary
* Class
* (Ur-)Element
* Ordered pair
* Ordinal number
* Subset
* Equality
* Extensionality
* Forcing
* Relation
* Equivalence
* Partition
* Set operations:
* Intersection
* Union
* Complement
* Cartesian product
* Power set
* Identities

Types of Sets|

* Countable
* Uncountable
* Empty
* Inhabited
* Singleton
* Finite
* Infinite
* Transitive
* Ultrafilter
* Recursive
* Fuzzy
* Universal
* Universe
* Constructible
* Grothendieck
* Von Neumann

Maps & Cardinality|

* Function/Map
* Domain
* Codomain
* Image
* In/Sur/Bi-jection
* Schröder–Bernstein theorem
* Isomorphism
* Gödel numbering
* Enumeration
* Large cardinal
* Inaccessible
* Aleph number
* Operation
* Binary

Set theories|

* Zermelo–Fraenkel
* Axiom of choice
* Continuum hypothesis
* General
* Kripke–Platek
* Morse–Kelley
* Naive
* New Foundations
* Tarski–Grothendieck
* Von Neumann–Bernays–Gödel
* Constructive

Syntax & Language|

* Alphabet
* Arity
* Automata
* Axiom schema
* Expression
* Ground
* Extension
* by definition
* Conservative
* Relation
* Formal
* Grammar
* Language
* Proof
* System
* Theory
* Formation rule
* Formula
* Atomic
* Closed
* Ground
* Open
* Free/bound variable
* Metalanguage
* Logical connective
* ¬
* ∨
* ∧
* →
* ↔
* =
* Predicate
* Functional
* Variable
* Propositional variable
* Quantifier
* ∃
* !
* ∀
* rank
* Sentence
* Atomic
* Spectrum
* Signature
* String
* Substitution
* Symbol
* Function
* Logical/Constant
* Non-logical
* Variable
* Term

Example axiomatic
systems (list)|

* of arithmetic:
* Peano
* second-order
* elementary function
* primitive recursive
* Robinson
* Skolem
* of the real numbers
* Tarski's axiomatization
* of Boolean algebras
* canonical
* minimal axioms
* of geometry:
* Euclidean
* Elements
* Hilbert's
* non-Euclidean
* Tarski's
* Principia Mathematica

Proof theory|

* Formal proof
* Natural deduction
* Logical consequence
* Rule of inference
* Sequent calculus
* Theorem
* Systems
* Formal
* Axiomatic
* Deductive
* Hilbert
* list
* Complete theory
* Independence (from ZFC)
* Proof of impossibility
* Ordinal analysis
* Reverse mathematics
* Self-verifying theories

Model theory|

* Interpretation
* Model
* Equivalence
* Finite
* Saturated
* Spectrum
* Substructure
* Non-standard model
* of arithmetic
* Diagram
* Elementary
* Categorical theory
* Model complete theory
* Satisfiability
* Semantics of logic
* Strength
* Theories of truth
* Semantic
* Tarski's
* Kripke's
* T-schema
* Transfer principle
* Truth predicate
* Truth value
* Type
* Ultraproduct
* Validity

Computability theory|

* Church encoding
* Church–Turing thesis
* Computably enumerable
* Computable function
* Computable set
* Decision problem
* Decidable
* Undecidable
* P
* NP
* P versus NP problem
* Kolmogorov complexity
* Lambda calculus
* Primitive recursive function
* Recursion
* Recursive set
* Turing machine
* Type theory

Related|

* Abstract logic
* Category theory
* Concrete/Abstract Category
* Category of sets
* History of logic
* History of mathematical logic
* timeline
* Logicism
* Mathematical object
* Philosophy of mathematics
* Supertask

* v
* t
* e

Formal semantics (natural language)

Central concepts|

* Compositionality
* Denotation
* Entailment
* Extension
* Generalized quantifier
* Intension
* Logical form
* Presupposition
* Proposition
* Reference
* Scope
* Speech act
* Syntax–semantics interface
* Truth conditions

Topics|

| Areas|

* Anaphora
* Ambiguity
* Binding
* Conditionals
* Definiteness
* Disjunction
* Evidentiality
* Focus
* Indexicality
* Lexical semantics
* Modality
* Negation
* Propositional attitudes
* Tense–aspect–mood
* Quantification
* Vagueness

|

Phenomena|

* Antecedent-contained deletion
* Cataphora
* Coercion
* Conservativity
* Counterfactuals
* Cumulativity
* De dicto and de re
* De se
* Deontic modality
* Discourse relations
* Donkey anaphora
* Epistemic modality
* Faultless disagreement
* Free choice inferences
* Givenness
* Crossover effects
* Hurford disjunction
* Inalienable possession
* Intersective modification
* Logophoricity
* Mirativity
* Modal subordination
* Negative polarity items
* Opaque contexts
* Performatives
* Privative adjectives
* Quantificational variability effect
* Responsive predicate
* Rising declaratives
* Scalar implicature
* Sloppy identity
* Subsective modification
* Subtrigging
* Telicity
* Temperature paradox
* Veridicality

Formalism|

| Formal systems|

* Alternative semantics
* Categorial grammar
* Combinatory categorial grammar
* Discourse representation theory
* Dynamic semantics
* Frame semantics
* Generative grammar
* Glue semantics
* Inquisitive semantics
* Intensional logic
* Lambda calculus
* Mereology
* Montague grammar
* Segmented discourse representation theory
* Situation semantics
* Supervaluationism
* Type theory
* TTR

|

Concepts|

* Autonomy of syntax
* Context set
* Continuation
* Conversational scoreboard
* Existential closure
* Function application
* Meaning postulate
* Monads
* Possible world
* Quantifier raising
* Quantization
* Question under discussion
* Squiggle operator
* Strict conditional
* Type shifter
* Universal grinder

See also|

* Cognitive semantics
* Computational semantics
* Distributional semantics
* Formal grammar
* Inferentialism
* Linguistics wars
* Term logic
* Philosophy of language
* Pragmatics
* Context
* Deixis
* Semantics of logic

*[v]: View this template
*[t]: Discuss this template
*[e]: Edit this template