In
mathematics
Mathematics is an area of knowledge that includes the topics of numbers, formulas and related structures, shapes and the spaces in which they are contained, and quantities and their changes. These topics are represented in modern mathematics ...
,
logic
Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the science of deductively valid inferences or of logical truths. It is a formal science investigating how conclusions follow from premi ...
, and
computer science
Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to practical disciplines (includin ...
, a type theory is the
formal presentation of a specific
type system
In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type to every "term" (a word, phrase, or other set of symbols). Usually the terms are various constructs of a computer progr ...
, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to
set theory
Set theory is the branch of mathematical logic that studies sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, is mostly concer ...
as a
foundation of mathematics
Foundations of mathematics is the study of the philosophical and logical and/or algorithmic basis of mathematics, or, in a broader sense, the mathematical investigation of what underlies the philosophical theories concerning the nature of mathem ...
. Two influential type theories that were proposed as foundations are
Alonzo Church's
typed λ-calculus and
Per Martin-Löf
Per Erik Rutger Martin-Löf (; ; born 8 May 1942) is a Swedish logician, philosopher, and mathematical statistician. He is internationally renowned for his work on the foundations of probability, statistics, mathematical logic, and computer sc ...
's
intuitionistic type theory
Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory and an alternative foundation of mathematics.
Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician an ...
. Most
computerized proof-writing systems use a type theory for their foundation. A common one is
Thierry Coquand's
Calculus of Inductive Constructions.
History
Type theory was created to avoid a paradox in a mathematical foundation based on
naive set theory
Naive set theory is any of several theories of sets used in the discussion of the foundations of mathematics.
Unlike axiomatic set theories, which are defined using formal logic, naive set theory is defined informally, in natural language. It d ...
and
formal logic
Logic is the study of correct reasoning. It includes both Mathematical logic, formal and informal logic. Formal logic is the science of Validity (logic), deductively valid inferences or of logical truths. It is a formal science investigating h ...
.
Russell's paradox
In mathematical logic, Russell's paradox (also known as Russell's antinomy) is a set-theoretic paradox discovered by the British philosopher and mathematician Bertrand Russell in 1901. Russell's paradox shows that every set theory that contains a ...
, which was discovered by
Bertrand Russell
Bertrand Arthur William Russell, 3rd Earl Russell, (18 May 1872 – 2 February 1970) was a British mathematician, philosopher, logician, and public intellectual. He had a considerable influence on mathematics, logic, set theory, linguistics, ...
, existed because a set could be defined using "all possible sets", which included itself. Between 1902 and 1908, Bertrand Russell proposed various "theories of type" to fix the problem. By 1908 Russell arrived at a "ramified" theory of types together with an "
axiom of reducibility
The axiom of reducibility was introduced by Bertrand Russell in the early 20th century as part of his ramified theory of types. Russell devised and introduced the axiom in an attempt to manage the contradictions he had discovered in his analysis ...
" both of which featured prominently in
Whitehead and
Russell
Russell may refer to:
People
* Russell (given name)
* Russell (surname)
* Lady Russell (disambiguation)
* Lord Russell (disambiguation)
Places Australia
* Russell, Australian Capital Territory
* Russell Island, Queensland (disambiguation)
...
's ''
Principia Mathematica
The ''Principia Mathematica'' (often abbreviated ''PM'') is a three-volume work on the foundations of mathematics written by mathematician–philosophers Alfred North Whitehead and Bertrand Russell and published in 1910, 1912, and 1913. ...
'' 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, 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.
[''Stanford Encyclopedia of Philosophy']
(rev. Mon Oct 12, 2020) Russell’s Paradox
3. Early Responses to the Paradox Types did gain a hold when used with one particular logic,
Alonzo Church's
lambda calculus
Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation t ...
.
The most famous early example is Church's
simply typed lambda calculus
The simply typed lambda calculus (\lambda^\to), a form
of type theory, is a typed interpretation of the lambda calculus with only one type constructor (\to) that builds function types. It is the canonical and simplest example of a typed lambda c ...
. Church's theory of types
helped the formal system avoid the
Kleene–Rosser paradox
In mathematics, the Kleene–Rosser paradox is a paradox that shows that certain systems of formal logic are inconsistent, in particular the version of Haskell Curry's combinatory logic introduced in 1930, and Alonzo Church's original lambda ...
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
mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are more express ...
.
The phrase "type theory" now generally refers to a typed system based around lambda calculus. One influential system is
Per Martin-Löf
Per Erik Rutger Martin-Löf (; ; born 8 May 1942) is a Swedish logician, philosopher, and mathematical statistician. He is internationally renowned for his work on the foundations of probability, statistics, mathematical logic, and computer sc ...
's
intuitionistic type theory
Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory and an alternative foundation of mathematics.
Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician an ...
, which was proposed as a foundation for
constructive mathematics
In the philosophy of mathematics, constructivism asserts that it is necessary to find (or "construct") a specific example of a mathematical object in order to prove that an example exists. Contrastingly, in classical mathematics, one can prove t ...
. 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
In mathematical logic and computer science, homotopy type theory (HoTT ) refers to various lines of development of intuitionistic type theory, based on the interpretation of types as objects to which the intuition of (abstract) homotopy theory a ...
.
Introduction
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
Terms and types
In type theory, every term has a type. A term and its type are often written together as "''term'' : ''type''". A common type to include in a type theory is the
Natural numbers
In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country").
Numbers used for counting are called ''cardinal n ...
, often written as "
" 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 "
" instead of "add
". So, the above terms might be rewritten as:
* 0 + 0 : nat
* 2 + 3 : nat
* 1 + (1 + (1 + 0)) : nat
Terms may also contain variables. Variables always have a type. So, assuming "x" and "y" are variables of type "nat", the following are also valid terms:
* x : nat
* x + 2 : nat
* x + (x + y) : nat
There are more types than "nat" and "bool". We have already seen the term "add", which is not a "nat", but a function that, when applied to two "nat"s, computes to a "nat". The type of "add" will be covered later. First, we need to describe "computes to".
Computation
Type theory has a built-in notation of computation. The following terms are all different:
* 1 + 4 : nat
* 3 + 2 : nat
* 0 + 5 : nat
but they all compute to the term "5 : nat". In type theory, we use the words "reduction" and "reduce" to refer to computation. So, we say "0 + 5 : nat" reduces to "5 : nat". It can be written "0 + 5 : nat
5 : nat". The computation is mechanical, accomplished by
rewriting
In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems (also known as rewrite systems, rewrite engines, or red ...
the term's syntax.
Terms that contain variables can be reduced too. So the term "x + (1 + 4) : nat" reduces to "x + 5 : nat". (We can reduce any sub-term within a term, thanks to the
Church-Rosser theorem.)
A term without any variables that cannot be reduced further is a "canonical term". All the terms above reduce to "5 : nat", which is a canonical term. The canonical terms of the natural numbers are:
* 0 : nat
* 1 : nat
* 2 : nat
* etc.
Obviously, terms that compute to the same term are equal. So, assuming "x : nat", the terms "x + (1 + 4) : nat" and "x + (4 + 1) : nat" are equal because they both reduce to "x + 5 : nat". When two terms are equal, they can be substituted for each other. Equality is a complex topic in type theory and there are many kinds of equality. This kind of equality, where two terms compute to the same term, is called "judgemental equality".
Functions
In type theory, functions are terms. Functions can either be lambda terms or defined "by rule".
Lambda terms
A lambda term looks like "(λ ''variablename'' : ''type1'' . ''term'')" and has type "''type1''
''type2''". The type "''type1''
''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
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
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
A substitution reaction (also known as single displacement reaction or single substitution reaction) is a chemical reaction during which one functional group in a chemical compound is replaced by another functional group. Substitution reactions ar ...
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
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
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
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
C
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
such that
is prime" or "there exists a number
such that property
holds", it can be expressed as a dependent type. That is, the property is proven for the specific "
" 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
In mathematical logic and type theory, the λ-cube (also written lambda cube) is a framework introduced by Henk Barendregt to investigate the different dimensions in which the calculus of constructions is a generalization of the simply typed � ...
for more information.
Universes
Π-terms return a type. So what is the type of their return value? Well, there must be a type that contains types. A type that contains other types is called a "
universe
The universe is all of space and time and their contents, including planets, stars, galaxies, and all other forms of matter and energy. The Big Bang theory is the prevailing cosmological description of the development of the universe. A ...
". It is often written with the symbol
. Sometimes there is a hierarchy of universes, with "
:
", "
:
", etc..
If a universe contains itself, it can lead to paradoxes like
Girard's Paradox.
For example:
Common "by rule" types and terms
Type theories are defined by their
rules of inference
In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions). For example, the rule of ...
. 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
The
empty type In type theory, the empty type or absurd type, typically denoted \mathbb 0 is a type with no terms. Such a type may be defined as the nullary coproduct (i.e. disjoint sum of no types). It may also be defined as the polymorphic type \forall t.t
For ...
has no terms. The type is usually written "
" or "
".
It is used to show that something is uncomputable. If for a type "A", you can create a function of type "A
", you know that "A" has no terms. An example for the type "A" might be "there exists a number
such that both
is even and
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
The
unit type
In the area of mathematical logic and computer science known as type theory, a unit type is a type that allows only one value (and thus can hold no information). The carrier (underlying set) associated with a unit type can be any singleton s ...
has exactly 1 canonical term. The type is written "
" or "
" and the single canonical term is written "*".
The unit type is used to show that something exists or is computable. If for a type "A", you can create a function of type "
A", you know that "A" has one or more terms. When a type has at least 1 term, we say it is "inhabited".
Boolean type
The Boolean type has exactly 2 canonical terms. The type is usually written "bool" or "
" or "
". The canonical terms are usually "true" and "false".
The Boolean type is defined with an eliminator function "if" such that:
* if true b c
b
* if false b c
c
Product type
The
product type
In programming languages and type theory, a product of ''types'' is another, compounded, type in a structure. The "operands" of the product are types, and the structure of a product type is determined by the fixed order of the operands in the prod ...
has terms that are
ordered pairs
In mathematics, an ordered pair (''a'', ''b'') is a pair of objects. The order in which the objects appear in the pair is significant: the ordered pair (''a'', ''b'') is different from the ordered pair (''b'', ''a'') unless ''a'' = ''b''. (In con ...
. For types "A" and "B", the product type is written "A
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)
a
* second (pair a b)
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
In mathematics, the intersection of two or more objects is another object consisting of everything that is contained in all of the objects simultaneously. For example, in Euclidean geometry, when two lines in a plane are not parallel, their ...
, 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 "
a:A . B(a)" where "B" has type "A
U". It is useful when showing
existence
Existence is the ability of an entity to interact with reality. In philosophy, it refers to the ontological property of being.
Etymology
The term ''existence'' comes from Old French ''existence'', from Medieval Latin ''existentia/exsistentia ...
of an "a" with property "B(a)".
Sum type
The
sum type
In computer science, a tagged union, also called a variant, variant record, choice type, discriminated union, disjoint union, sum type or coproduct, is a data structure used to hold a value that could take on several different, but fixed, types. O ...
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
C" and "g : B
C":
* match (injectionLeft a) C f g
(f a)
* match (injectionRight b) C f g
(g b)
The sum type is used for
logical or
In logic, disjunction is a logical connective typically notated as \lor and read aloud as "or". For instance, the English language sentence "it is raining or it is snowing" can be represented in logic using the disjunctive formula R \lor S ...
and for
union.
Natural numbers
The natural numbers are usually implemented in the style of
Peano Arithmetic
In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly ...
. There is a canonical term, "0 : nat" for zero. Canonical values larger than zero use the constructor function "S : nat
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
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
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
PZ
* R P PZ PS (S
)
PS (R P PZ PS
)
The function "add", that was used earlier, can be defined using "R".
* add : nat
nat
nat ::= R (λ n:nat . nat
nat) (λ n:nat . n) (λ g:nat
nat . (λ m:nat . S (g m)))
Identity type
The
identity type
In type theory, the identity type represents the concept of equality. It is also known as propositional equality to differentiate it from "judgemental equality". Equality in type theory is a complex topic and has been the subject of research, s ...
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
Symmetry (from grc, συμμετρία "agreement in dimensions, due proportion, arrangement") in everyday language refers to a sense of harmonious and beautiful proportion and balance. In mathematics, "symmetry" has a more precise definiti ...
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
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
x+1 = 1+x". We can use it and the function "J" to substituted "1+x" for "x+1" in any term. In this way, the identity type is able to capture equalities that are not possible with judgemental equality.
To be clear, it is possible to create the type "0 = 1", but there will not be a way to create terms of that type. Without a term of type "0 = 1", it will not be possible to use the function "J" to substitute "0" for "1" in another term.
The complexities of equality in type theory make it an active research area, see
homotopy type theory
In mathematical logic and computer science, homotopy type theory (HoTT ) refers to various lines of development of intuitionistic type theory, based on the interpretation of types as objects to which the intuition of (abstract) homotopy theory a ...
.
Inductive types
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 Structural induction is a proof method that is used in mathematical logic (e.g., in the proof of Łoś' theorem), computer science, graph theory, and some other mathematical fields. It is a generalization of mathematical induction over natural nu ...
.
There are similar, more powerful ways to create types. These include
induction-recursion and
induction-induction. There is also a way to create similar types using only lambda terms, called
Scott encoding.
(NOTE: Type theories do not usually include
coinductive types. They represent an infinite data type and most type theories limit themselves to functions that can be proven to halt.)
Differences from set theory
The traditional foundation for mathematics has been set theory paired with a logic. The most common one cited is
Zermelo–Fraenkel set theory
In set theory, Zermelo–Fraenkel set theory, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes such a ...
, known as "ZF" or, with the
Axiom of choice
In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collection ...
, "ZFC". Type theories differ from this foundation in a number of ways.
* Set theory has both
rules
Rule or ruling may refer to:
Education
* Royal University of Law and Economics (RULE), a university in Cambodia
Human activity
* The exercise of political or personal control by someone with authority or power
* Business rule, a rule per ...
and
axioms
An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy or ...
, 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
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quant ...
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
In logic, the law of excluded middle (or the principle of excluded middle) states that for every proposition, either this proposition or its negation is true. It is one of the so-called three laws of thought, along with the law of noncontrad ...
. That is, every theorem is true or false. When a type theory defines the concepts of "and" and "or" as types, it leads to
intuitionistic logic
Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems o ...
, 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
is paired with a proof that the subset's property holds for
. 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 In set theory, several ways have been proposed to construct the natural numbers. These include the representation via von Neumann ordinals, commonly employed in axiomatic set theory, and a system based on equinumerosity that was proposed by Gottlo ...
.) Type theory can encode numbers as functions using
Church encoding
In mathematics, Church encoding is a means of representing data and operators in the lambda calculus. The Church numerals are a representation of the natural numbers using lambda notation. The method is named for Alonzo Church, who first encoded ...
or more naturally as
inductive types. The constructors "0" and "S" created by the inductive type closely resemble
Peano's axioms
In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly ...
.
* Set theory has
set-builder notation
In set theory and its applications to logic, mathematics, and computer science, set-builder notation is a mathematical notation for describing a set by enumerating its elements, or stating the properties that its members must satisfy.
Definin ...
. It can create any set that can be defined. This allows it to create
Uncountable set
In mathematics, an uncountable set (or uncountably infinite set) is an infinite set that contains too many elements to be countable. The uncountability of a set is closely related to its cardinal number: a set is uncountable if its cardinal num ...
s. Type theories are syntactic, which limits them to a
countably infinite
In mathematics, a set is countable if either it is finite or it can be made in one to one correspondence with the set of natural numbers. Equivalently, a set is ''countable'' if there exists an injective function from it into the natural numbe ...
terms. Additionally, most type theories require computation to always halt and limit themselves to
recursively generable terms. As a result, most type theories do not use the
Real number
In mathematics, a real number is a number that can be used to measure a ''continuous'' one- dimensional quantity such as a distance, duration or temperature. Here, ''continuous'' means that values can have arbitrarily small variations. Ever ...
s but the
Computable number
In mathematics, computable numbers are the real numbers that can be computed to within any desired precision by a finite, terminating algorithm. They are also known as the recursive numbers, effective numbers or the computable reals or recursive ...
s.
* In set theory, the
Axiom of Choice
In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collection ...
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 BHK is a three-letter abbreviation that may refer to:
* BHK interpretation of intuitionistic predicate logic
* Baby hamster kidney cells used in molecular biology
* Bachelor of Human Kinetics (BHk) degree.
* Baltische Historische Kommission, or ...
, its connected to logic by the
Curry–Howard isomorphism, and its connections to
Category theory
Category theory is a general theory of mathematical structures and their relations that was introduced by Samuel Eilenberg and Saunders Mac Lane in the middle of the 20th century in their foundational work on algebraic topology. Nowadays, cat ...
.
Technical details
A type theory is a
mathematical logic
Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal s ...
. It is a collection of
rules of inference
In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions). For example, the rule of ...
that result in
judgements. Most logics have judgements meaning "The term
is true." or "The term
is a
well-formed formula
In mathematical logic, propositional logic and predicate logic, a well-formed formula, abbreviated WFF or wff, often simply formula, is a finite sequence of symbols from a given alphabet that is part of a formal language. A formal language can be ...
.". A type theory has additional judgements that define types and relate terms to types.
Terms
A
term in logic is recursively defined as a constant symbol, variable, or a function application, where a term is applied to another term. Some constant symbols will be "0" of the natural numbers, "true" of the Booleans, and functions like "S" and "if". Thus some terms are "0", "(S 0)", "(S (S x))", and "if true 0 (S 0)".
Judgements
Most type theories have 4 judgements:
* "
is a type."
* "
is a term of type
."
* "Type
is equal to type
."
* "Terms
and
are both of type
and are equal."
The judgements can be made under an assumption. Thus, we might say, "assuming
is a term of type "bool" and
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 '
'. Thus, the example statement is formally written:
* x:bool, y:nat
(if x y y) : nat
If there are no assumptions, there will be nothing to the left of the turnstile.
*
S : nat
nat
The list of assumptions is called the "context". It is very common to see the symbol '
' used to represent some or all of the assumptions. Thus, the formal notation for the 4 different judgements is usually:
(NOTE: The judgement of equality of terms is where the phrase "judgemental equality" comes from. )
The judgements enforce that every term has a type. The type will restrict which rules can be applied to a term.
Rules
A type theory's
rules
Rule or ruling may refer to:
Education
* Royal University of Law and Economics (RULE), a university in Cambodia
Human activity
* The exercise of political or personal control by someone with authority or power
* Business rule, a rule per ...
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:
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 "
". (Note: "
" "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
B" under the other assumptions
.
The rules are syntactic and work by
rewriting
In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems (also known as rewrite systems, rewrite engines, or red ...
. Thus, the metavariables like "
", "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, 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":
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 o
Homotopy Type Theorybook
Properties of type theories
Terms usually belong to a single type. However, there are set theories that define "subtyping".
Computation takes place by repeated application of rules. Many type theories are
strongly normalizing
In abstract rewriting, an object is in normal form if it cannot be rewritten any further, i.e. it is irreducible. Depending on the rewriting system, an object may rewrite to several normal forms or none at all. Many properties of rewriting systems ...
, 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. Thus,
,
,
,
,
.
Axioms
Most type theories do not have
axioms
An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word (), meaning 'that which is thought worthy or ...
. This is because a type theory is defined by its rules of inference. (See "
Rules
Rule or ruling may refer to:
Education
* Royal University of Law and Economics (RULE), a university in Cambodia
Human activity
* The exercise of political or personal control by someone with authority or power
* Business rule, a rule per ...
" 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
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quant ...
) 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.
Some commonly encountered axioms are:
* "Axiom K" ensures "uniqueness of identity proofs". That is, that every term of an identity type is equal to reflexivity.
* "Univalence Axiom" holds that equivalence of types is equality of types. The research into this property led to
cubical type theory, where the property holds without needing an axiom.
* "Law of Excluded Middle" is often added to satisfy users who want
classical logic
Classical logic (or standard logic or Frege-Russell logic) is the intensively studied and most widely used class of deductive logic. Classical logic has had much influence on analytic philosophy.
Characteristics
Each logical system in this class ...
, instead of intuitionistic logic.
The
Axiom of Choice
In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collection ...
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 .)
Decision problems
A type theory is naturally associated with the
decision problem
In computability theory and computational complexity theory, a decision problem is a computational problem that can be posed as a yes–no question of the input values. An example of a decision problem is deciding by means of an algorithm wheth ...
of
type inhabitation In type theory, a branch of mathematical logic, in a given typed calculus, the type inhabitation problem for this calculus is the following problem: given a type \tau and a typing environment \Gamma, does there exist a \lambda-term M such that \Gam ...
.
Type inhabitation
The decision problem of ''type inhabitation'' (abbreviated by
) is:
:Given a type environment
and a type
, decide whether there exists a term
that can be assigned the type
in the type environment
.
Girard's paradox shows that type inhabitation is strongly related to the consistency of a type system with Curry–Howard correspondence. To be sound, such a system must have uninhabited types.
The opposition of terms and types can also be views as one of ''implementation'' and ''specification''. By
program synthesis In computer science, program synthesis is the task to construct a program that provably satisfies a given high-level formal specification. In contrast to program verification, the program is to be constructed rather than given; however, both field ...
(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.
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
Homotopy type theory
In mathematical logic and computer science, homotopy type theory (HoTT ) refers to various lines of development of intuitionistic type theory, based on the interpretation of types as objects to which the intuition of (abstract) homotopy theory a ...
differs from
intuitionistic type theory
Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory and an alternative foundation of mathematics.
Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician an ...
mostly by its handling of the equality type. In 2016
cubical type theory was proposed, which is a homotopy type theory with normalization.
Interpretations
Type theory has connections to other areas of mathematics. Proponents of type theory as a foundation often mention these connections as justification for its use.
Types are propositions; terms are proofs
When used as a foundation, certain types are interpreted as
propositions
In logic and linguistics, a proposition is the meaning of a declarative sentence. In philosophy, " meaning" is understood to be a non-linguistic entity which is shared by all sentences with the same meaning. Equivalently, a proposition is the no ...
(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
The
Curry–Howard correspondence
In programming language theory and proof theory, the Curry–Howard correspondence (also known as the Curry–Howard isomorphism or equivalence, or the proofs-as-programs and propositions- or formulae-as-types interpretation) is the direct relati ...
is the observed similarity between logics and programming languages. The implication in logic, "A
B" resembles a function from type "A" to type "B". For a variety of logics, the rules are a similar to expression in a programming language's types. The similarity goes farther, as applications of the rules resemble programs in the programming languages. Thus, the correspondence is often summarized as "proofs as programs".
The logic operators "
for all
In mathematical logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as "given any" or "for all". It expresses that a predicate can be satisfied by every member of a domain of discourse. In other ...
" and "
exists" led Per Martin-Löf to invent dependent type theory.
Intuitionistic logic
When some types are interpreted as propositions, there is a set of common types that can be used to connect them to make a logic out of types. However, that logic is not
classical logic
Classical logic (or standard logic or Frege-Russell logic) is the intensively studied and most widely used class of deductive logic. Classical logic has had much influence on analytic philosophy.
Characteristics
Each logical system in this class ...
but
intuitionistic logic
Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems o ...
. That is, it does not have the
law of excluded middle
In logic, the law of excluded middle (or the principle of excluded middle) states that for every proposition, either this proposition or its negation is true. It is one of the so-called three laws of thought, along with the law of noncontrad ...
nor
double negation
In propositional logic, double negation is the theorem that states that "If a statement is true, then it is not the case that the statement is not true." This is expressed by saying that a proposition ''A'' is logically equivalent to ''not (not ...
.
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 "
A" indicates that A has a proof and being able to create the function "A
" 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''
and
to represent "true" (provable) and "false" (disproven), as part of a intuitionistic logic for proposition.''
Under this intuitionistic interpretation, there are common types that act as the logical operators:
But under this interpretation, there is no law of excluded middle. That is, there is no term of type Π A . A + (A
).
Likewise, there is no double negation. There is no term of type Π A . ((A
)
)
A. (Note: Intuitionistic logic does allow
and there is a term of type (((A
)
)
)
(A
).)
Thus, the logic-of-types is an intuitionistic logic. Type theory is often cited as an implementation of the
Brouwer–Heyting–Kolmogorov interpretation In mathematical logic, the Brouwer–Heyting–Kolmogorov interpretation, or BHK interpretation, of intuitionistic logic was proposed by L. E. J. Brouwer and Arend Heyting, and independently by Andrey Kolmogorov. It is also sometimes called the re ...
.
It is possible to include the law of excluded middle and double negation into a type theory, by rule or assumption. However, terms may not compute down to canonical terms and it will interfere with the ability to determine if two terms are judgementally equal to each other.
Constructive mathematics
Per Martin-Löf proposed his intuitionistic type theory as a foundation for
constructive mathematics
In the philosophy of mathematics, constructivism asserts that it is necessary to find (or "construct") a specific example of a mathematical object in order to prove that an example exists. Contrastingly, in classical mathematics, one can prove t ...
. Constructive mathematics requires when proving "There exists an
with property P(
)", there must be a particular
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
, "first
" will produce the
and "second
" will produce the proof of P(
).
An example of a non-constructive proof is a "proof by contradiction". The first step is assuming that
does not exist and refuting it by contradiction. The conclusion from that step is "it is not the case that
does not exist". The last step is, by double negation, concluding that
exists. To be clear, constructive mathematics still allows "refute by contradiction". It can prove that "it is not the case that
does not exist". But constructive mathematics does not allow the last step of removing the double negation to conclude that
exists.
Constructive mathematics has often used intutionistic logic, as evidenced by the
Brouwer–Heyting–Kolmogorov interpretation In mathematical logic, the Brouwer–Heyting–Kolmogorov interpretation, or BHK interpretation, of intuitionistic logic was proposed by L. E. J. Brouwer and Arend Heyting, and independently by Andrey Kolmogorov. It is also sometimes called the re ...
.
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 In programming language theory, parametricity is an abstract uniformity property enjoyed by parametrically polymorphic functions, which captures the intuition that all instances of a polymorphic function act the same way.
Idea
Consider this exa ...
.
Category theory
Although the initial motivation for
category theory
Category theory is a general theory of mathematical structures and their relations that was introduced by Samuel Eilenberg and Saunders Mac Lane in the middle of the 20th century in their foundational work on algebraic topology. Nowadays, cat ...
was far removed from foundationalism, the two fields turned out to have deep connections. As
John Lane Bell
John Lane Bell (born March 25, 1945) is an Anglo-Canadian philosopher, mathematician and logician. He is Professor Emeritus of Philosophy at the University of Western Ontario in Canada. His research includes such topics as set theory, model theor ...
writes: "In fact categories can ''themselves'' be viewed as type theories of a certain kind; this fact alone indicates that type theory is much more closely related to category theory than it is to set theory." In brief, a category can be viewed as a type theory by regarding its objects as types (or sorts), i.e. "Roughly speaking, a category may be thought of as a type theory shorn of its syntax." A number of significant results follow in this way:
*
cartesian closed categories
In category theory, a category is Cartesian closed if, roughly speaking, any morphism defined on a product of two objects can be naturally identified with a morphism defined on one of the factors. These categories are particularly important in ma ...
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
Dana Stewart Scott (born October 11, 1932) is an American logician who is the emeritus Hillman University Professor of Computer Science, Philosophy, and Mathematical Logic at Carnegie Mellon University; he is now retired and lives in Berkeley, Ca ...
around 1980);
*
locally cartesian closed categories correspond to
Martin-Löf type theories (Seely, 1984).
The interplay, known as
categorical logic
__NOTOC__
Categorical logic is the branch of mathematics in which tools and concepts from category theory are applied to the study of mathematical logic. It is also notable for its connections to theoretical computer science.
In broad terms, categ ...
, has been a subject of active research since then; see the monograph of Jacobs (1999) for instance.
Homotopy type theory
In mathematical logic and computer science, homotopy type theory (HoTT ) refers to various lines of development of intuitionistic type theory, based on the interpretation of types as objects to which the intuition of (abstract) homotopy theory a ...
attempts to combine type theory and category theory. It focuses on equalities, especially equalities between types.
List of type theories
Major
*
Simply typed lambda calculus
The simply typed lambda calculus (\lambda^\to), a form
of type theory, is a typed interpretation of the lambda calculus with only one type constructor (\to) that builds function types. It is the canonical and simplest example of a typed lambda c ...
which is a
higher-order logic
mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are more express ...
*
intuitionistic type theory
Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory and an alternative foundation of mathematics.
Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician an ...
*
system F
System F (also polymorphic lambda calculus or second-order lambda calculus) is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorphi ...
*
LF is often used to define other type theories
*
calculus of constructions and its derivatives
Minor
*
Automath
*
ST type theory
* UTT (Luo's Unified Theory of dependent Types)
* some forms of
combinatory logic
Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry, and has more recently been used in computer science as a theoretical model of comp ...
* others defined in the
lambda cube
In mathematical logic and type theory, the λ-cube (also written lambda cube) is a framework introduced by Henk Barendregt to investigate the different dimensions in which the calculus of constructions is a generalization of the simply typed � ...
(also known as
pure type system __NOTOC__
In the branches of mathematical logic known as proof theory and type theory, a pure type system (PTS), previously known as a generalized type system (GTS), is a form of typed lambda calculus that allows an arbitrary number of sorts and d ...
s)
* others under the name
typed lambda calculus
A typed lambda calculus is a typed formalism that uses the lambda-symbol (\lambda) to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of ...
Active research
*
Homotopy type theory
In mathematical logic and computer science, homotopy type theory (HoTT ) refers to various lines of development of intuitionistic type theory, based on the interpretation of types as objects to which the intuition of (abstract) homotopy theory a ...
explores equality of types
*
Cubical Type Theory is an implementation of homotopy type theory
Applications
Mathematical foundations
The first computer proof assistant, called
Automath, used type theory to encode mathematics on a computer. Martin-Löf specifically developed
intuitionistic type theory
Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory and an alternative foundation of mathematics.
Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician an ...
to encode ''all'' mathematics to serve as a new foundation for mathematics. There is ongoing research into mathematical foundations using
homotopy type theory
In mathematical logic and computer science, homotopy type theory (HoTT ) refers to various lines of development of intuitionistic type theory, based on the interpretation of types as objects to which the intuition of (abstract) homotopy theory a ...
.
Mathematicians working in
category theory
Category theory is a general theory of mathematical structures and their relations that was introduced by Samuel Eilenberg and Saunders Mac Lane in the middle of the 20th century in their foundational work on algebraic topology. Nowadays, cat ...
already had difficulty working with the widely accepted foundation of
Zermelo–Fraenkel set theory
In set theory, Zermelo–Fraenkel set theory, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes such a ...
. This led to proposals such as Lawvere's Elementary Theory of the Category of Sets (ETCS). Homotopy type theory continues in this line using type theory. Researchers are exploring connections between dependent types (especially the identity type) and
algebraic topology
Algebraic topology is a branch of mathematics that uses tools from abstract algebra to study topological spaces. The basic goal is to find algebraic invariants that classify topological spaces up to homeomorphism, though usually most classify u ...
(specifically
homotopy
In topology, a branch of mathematics, two continuous functions from one topological space to another are called homotopic (from grc, ὁμός "same, similar" and "place") if one can be "continuously deformed" into the other, such a deforma ...
).
Proof assistants
Much of the current research into type theory is driven by
proof checkers, interactive
proof assistant
In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor ...
s, 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
mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are more express ...
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
Matita
is an experimental proof assistant under development at the Computer Science Department of the University of Bologna. It is a tool aiding the development of formal proofs by man-machine collaboration, providing a programming environment wh ...
, 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
Lego ( , ; stylized as LEGO) is a line of plastic construction toys that are manufactured by The Lego Group, a privately held company based in Billund, Denmark. The company's flagship product, Lego, consists of variously colored interlocki ...
and
Isabelle. Isabelle also supports foundations besides type theories, such as
ZFC.
Mizar is an example of a proof system that only supports set theory.
Programming languages
Any
static program analysis
In computer science, static program analysis (or static analysis) is the program analysis, analysis of computer programs performed without executing them, in contrast with dynamic program analysis, which is performed on programs during their execu ...
, such as the type checking algorithms in the
semantic analysis phase of
compiler
In computing, a compiler is a computer program that translates computer code written in one programming language (the ''source'' language) into another language (the ''target'' language). The name "compiler" is primarily used for programs tha ...
, 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
Type theory is also widely used in
formal theories of semantics of
natural language
In neuropsychology, linguistics, and philosophy of language, a natural language or ordinary language is any language that has evolved naturally in humans through use and repetition without conscious planning or premeditation. Natural languages ...
s, especially
Montague grammar __notoc__
Montague grammar is an approach to natural language semantics, named after American logician Richard Montague. The Montague grammar is based on mathematical logic, especially higher-order predicate logic and lambda calculus, and makes us ...
[Cooper, Robin.]
Type theory and semantics in flux
" Handbook of the Philosophy of Science 14 (2012): 271-323. 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
and
for individuals and
truth-value
In logic and mathematics, a truth value, sometimes called a logical value, is a value indicating the relation of a proposition to truth, which in classical logic has only two possible values (''true'' or '' false'').
Computing
In some progra ...
s, respectively, and defines the set of types recursively as follows:
* if
and
are types, then so is
;
* nothing except the basic types, and what can be constructed from them by means of the previous clause are types.
A complex type
is the type of
functions from entities of type
to entities of type
. Thus one has types like
which are interpreted as elements of the set of functions from entities to truth-values, i.e.
indicator function
In mathematics, an indicator function or a characteristic function of a subset of a set is a function that maps elements of the subset to one, and all other elements to zero. That is, if is a subset of some set , one has \mathbf_(x)=1 if x\i ...
s of sets of entities. An expression of type
is a function from sets of entities to truth-values, i.e. a (indicator function of a) set of sets. This latter type is standardly taken to be the type of
natural language quantifiers, like '' everybody'' or '' nobody'' (
Montague 1973,
Barwise and Cooper 1981).
Social sciences
Gregory Bateson
Gregory Bateson (9 May 1904 – 4 July 1980) was an English anthropologist, social scientist, linguist, visual anthropologist, semiotician, and cyberneticist whose work intersected that of many other fields. His writings include '' Steps to an ...
introduced a theory of logical types into the social sciences; his notions of
double bind
A double bind is a dilemma in communication in which an individual (or group) receives two or more reciprocally conflicting messages. In some scenarios (e.g. within families or romantic relationships) this can be emotionally distressing, creating ...
and
logical levels are based on Russell's theory of types.
See also
*
Foundations of mathematics
Foundations of mathematics is the study of the philosophical and logical and/or algorithmic basis of mathematics, or, in a broader sense, the mathematical investigation of what underlies the philosophical theories concerning the nature of mathem ...
Further reading
*
*
* Covers type theory in depth, including polymorphic and dependent type extensions. Gives
categorical semantics.
*
* Provides a historical survey of the developments of the theory of types with a focus on the decline of the theory as a foundation of mathematics over the four decades following the publication of the second edition of 'Principia Mathematica'.
* Intended as a type theory counterpart of
Paul Halmos
Paul Richard Halmos ( hu, Halmos Pál; March 3, 1916 – October 2, 2006) was a Hungarian-born American mathematician and statistician who made fundamental advances in the areas of mathematical logic, probability theory, statistics, operator ...
's (1960) ''
Naïve Set Theory''
*
*
* A good introduction to simple type theory for computer scientists; the system described is not exactly Church's STT though
Book review*
*
*
Notes
References
External links
Introductory material
Type Theory at nLab which has articles on many topics.
Intuitionistic Type Theoryarticle at the Stanford Encyclopedia of Philosophy
Lambda Calculus with Typesbook by Henk Barendregt
Calculus of Constructions / Typed Lambda Calculustextbook style paper by Helmut Brandl
Intuitionistic Type Theorynotes by Per Martin-Löf
Programming in Martin-Löf ’s Type Theorybook
Homotopy Type Theorybook, which proposed homotopy type theory as a mathematical foundation.
Advanced material
*
The TYPES Forum— moderated e-mail forum focusing on type theory in computer science, operating since 1987.
*
tp://ftp.cs.cornell.edu/pub/nuprl/doc/book.ps.gz The Nuprl BookIntroduction to Type Theory.
of summer schools 2005–2008
** Th
has introductory lectures
many lectures and some notes.
includin
Robert Harper's talks on YouTubeAndrej Bauer's blog
{{DEFAULTSORT:Type Theory
Systems of formal logic
Hierarchy