In
mathematics
Mathematics is a field of study that discovers and organizes methods, Mathematical theory, theories and theorems that are developed and Mathematical proof, proved for the needs of empirical sciences and mathematics itself. There are many ar ...
and
theoretical computer science
Theoretical computer science is a subfield of computer science and mathematics that focuses on the Abstraction, abstract and mathematical foundations of computation.
It is difficult to circumscribe the theoretical areas precisely. The Associati ...
, a type theory is the
formal presentation of a specific
type system. 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 Set (mathematics), 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 mathema ...
as a
foundation of mathematics. Two influential type theories that have been proposed as foundations are:
*
Typed λ-calculus of
Alonzo Church
Alonzo Church (June 14, 1903 – August 11, 1995) was an American computer scientist, mathematician, logician, and philosopher who made major contributions to mathematical logic and the foundations of theoretical computer science. He is bes ...
*
Intuitionistic type theory of
Per Martin-Löf
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
paradoxes in
naive set theory and
formal logic, such as
Russell's paradox which demonstrates that, without proper axioms, it is possible to define the set of all sets that are not members of themselves; this set both contains itself and does not contain itself. Between 1902 and 1908,
Bertrand Russell
Bertrand Arthur William Russell, 3rd Earl Russell, (18 May 1872 – 2 February 1970) was a British philosopher, logician, mathematician, and public intellectual. He had influence on mathematics, logic, set theory, and various areas of analytic ...
proposed various solutions to this problem.
By 1908, Russell arrived at a
ramified theory of types together with an
axiom of reducibility, both of which appeared in
Whitehead and
Russell's ''
Principia Mathematica'' published in 1910, 1912, and 1913. This system avoided contradictions suggested in Russell's paradox by creating a hierarchy of types and then assigning each concrete mathematical entity to a specific type. Entities of a given type were built exclusively of
subtypes of that type, thus preventing an entity from being defined using itself. This resolution of Russell's paradox is similar to approaches taken in other formal systems, such as
Zermelo-Fraenkel set theory.
[''Stanford Encyclopedia of Philosophy']
(rev. Mon Oct 12, 2020) Russell’s Paradox
3. Early Responses to the Paradox
Type theory is particularly popular in conjunction with
Alonzo Church
Alonzo Church (June 14, 1903 – August 11, 1995) was an American computer scientist, mathematician, logician, and philosopher who made major contributions to mathematical logic and the foundations of theoretical computer science. He is bes ...
's
lambda calculus
In mathematical logic, the lambda calculus (also written as ''λ''-calculus) is a formal system for expressing computability, computation based on function Abstraction (computer science), abstraction and function application, application using var ...
. One notable early example of type theory is Church's
simply typed lambda calculus. Church's theory of types
helped the formal system avoid the
Kleene–Rosser paradox that afflicted the original untyped lambda calculus. Church demonstrated that it could serve as a
foundation of mathematics and it was referred to as a
higher-order logic.
In the modern literature, "type theory" 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
Rocq (previously known as ''Coq''),
Lean, and other computer
proof assistants. Type theory is an active area of research, one direction being the development 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 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
Category theory is a general theory of mathematical structures and their relations. It was introduced by Samuel Eilenberg and Saunders Mac Lane in the middle of the 20th century in their foundational work on algebraic topology. Category theory ...
already had difficulty working with the widely accepted foundation of
Zermelo–Fraenkel set theory. This led to proposals such as Lawvere's
Elementary Theory of the Category of Sets (ETCS). Homotopy type theory continues in this line using type theory. Researchers are exploring connections between dependent types (especially the identity type) and
algebraic topology (specifically
homotopy).
Proof assistants
Much of the current research into type theory is driven by
proof checkers, interactive
proof assistants, and
automated theorem provers. Most of these systems use a type theory as the mathematical foundation for encoding proofs, which is not surprising, given the close connection between type theory and programming languages:
*
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
Rocq (previously known as ''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
Any
static program analysis, such as the type checking algorithms in the
semantic analysis phase of
compiler
In computing, a compiler is a computer program that Translator (computing), translates computer code written in one programming language (the ''source'' language) into another language (the ''target'' language). The name "compiler" is primaril ...
, 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 languages, especially
Montague grammar and its descendants. In particular,
categorial grammars and
pregroup grammars extensively use type constructors to define the types (''noun'', ''verb'', etc.) of words.
The most common construction takes the basic types
and
for individuals and
truth-values, 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 , then the indicator functio ...
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).
Type theory with records is a
formal semantics representation framework, using ''
records'' to express ''type theory types''. It has been used in
natural language processing
Natural language processing (NLP) is a subfield of computer science and especially artificial intelligence. It is primarily concerned with providing computers with the ability to process data encoded in natural language and is thus closely related ...
, principally
computational semantics
Computational semantics is the study of how to automate the process of constructing and reasoning with semantics, meaning representations of natural language expressions. It consequently plays an important role in natural language processing, nat ...
and
dialogue systems.
Social sciences
Gregory Bateson introduced a theory of logical types into the social sciences; his notions of
double bind and logical levels are based on Russell's theory of types.
Logic
A type theory is a
mathematical logic
Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
, which is to say it is a collection of
rules of inference that result in
judgments. Most logics have judgments asserting "The
proposition
A proposition is a statement that can be either true or false. It is a central concept in the philosophy of language, semantics, logic, and related fields. Propositions are the object s denoted by declarative sentences; for example, "The sky ...
is true", or "The
formula is a
well-formed formula".
A type theory has judgments that define types and assign them to a collection of formal objects, known as terms. A term and its type are often written together as
.
Terms
A
term in logic is
recursively defined as a
constant symbol,
variable, or a
function application
In mathematics, function application is the act of applying a function to an argument from its domain so as to obtain the corresponding value from its range. In this sense, function application can be thought of as the opposite of function abs ...
, where a term is applied to another term. Constant symbols could include the natural number
, the Boolean value
, and functions such as the
successor function and
conditional operator . Thus some terms could be
,
,
, and
.
Judgments
Most type theories have 4 judgments:
* "
is a type"
* "
is a term of type
"
* "Type
is equal to type
"
* "Terms
and
both of type
are equal"
Judgments may follow from assumptions. For example, one might say "assuming
is a term of type
and
is a term of type
, it follows that
is a term of type
". Such judgments are formally written with the
turnstile symbol .
If there are no assumptions, there will be nothing to the left of the turnstile.
The list of assumptions on the left is the ''context'' of the judgment. Capital greek letters, such as
and
, are common choices to represent some or all of the assumptions. The 4 different judgments are thus usually written as follows.
Some textbooks use a triple equal sign
to stress that this is
judgmental equality and thus an
extrinsic notion of equality.
The judgments enforce that every term has a type. The type will restrict which rules can be applied to a term.
Rules of Inference
A type theory's
inference rules say what judgments can be made, based on the existence of other judgments. Rules are expressed as a
Gentzen-style
deduction using a horizontal line, with the required input judgments above the line and the resulting judgment below the line. For example, the following inference rule states a
substitution rule for judgmental equality.
The rules are syntactic and work by
rewriting. The
metavariables ,
,
,
, and
may actually consist of complex terms and types that contain many function applications, not just single symbols.
To generate a particular judgment in type theory, there must be a rule to generate it, as well as rules to generate all of that rule's required inputs, and so on. The applied rules form a
proof tree, where the top-most rules need no assumptions. One example of a rule that does not require any inputs is one that states the type of a constant term. For example, to assert that there is a term
of type
, one would write the following.
Type inhabitation
Generally, the desired conclusion of a proof in type theory is one of
type inhabitation.
The decision problem of type inhabitation (abbreviated by
) is:
:Given a context
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.
A type theory usually has several rules, including ones to:
* create a judgment (known as a ''context'' in this case)
* add an assumption to the context (context ''weakening'')
*
rearrange the assumptions
* use an assumption to create a variable
* define
reflexivity,
symmetry and
transitivity for judgmental equality
* define substitution for application of lambda terms
* list all the interactions of equality, such as substitution
* define a hierarchy of type universes
* assert the existence of new types
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.
For examples of rules, an interested reader may follow Appendix A.2 of the ''Homotopy Type Theory'' book,
or read Martin-Löf's Intuitionistic Type Theory.
Connections to foundations
The logical framework of a type theory bears a resemblance to
intuitionistic, or constructive, logic. Formally, type theory is often cited as an implementation of the
Brouwer–Heyting–Kolmogorov interpretation of intuitionistic logic.
Additionally, connections can be made to
category theory
Category theory is a general theory of mathematical structures and their relations. It was introduced by Samuel Eilenberg and Saunders Mac Lane in the middle of the 20th century in their foundational work on algebraic topology. Category theory ...
and
computer programs.
Intuitionistic logic
When used as a foundation, certain types are interpreted to be
propositions (statements that can be proven), and terms inhabiting the type are interpreted to be proofs of that proposition. When some types are interpreted as propositions, there is a set of common types that can be used to connect them to make a
Boolean algebra out of types. However, the logic is not
classical logic but
intuitionistic logic, which is to say it does not have the
law of excluded middle nor
double negation.
Under this intuitionistic interpretation, there are common types that act as the logical operators:
Because the law of excluded middle does not hold, there is no term of type
. Likewise, double negation does not hold, so there is no term of type
.
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.
Constructive mathematics requires when proving "there exists an
with property
", one must construct a particular
and a proof that it has property
. In type theory, existence is accomplished using the dependent product type, and its proof requires a term of that type.
An example of a non-constructive proof is
proof by contradiction
In logic, proof by contradiction is a form of proof that establishes the truth or the validity of a proposition by showing that assuming the proposition to be false leads to a contradiction.
Although it is quite freely used in mathematical pr ...
. 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. Constructive mathematics does not allow the last step of removing the double negation to conclude that
exists.
Most of the type theories proposed as foundations are constructive, and 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.
Curry-Howard correspondence
The
Curry–Howard correspondence 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 similar to expressions 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 opposition of terms and types can also be viewed as one of ''implementation'' and ''specification''. By
program synthesis, (the computational counterpart of) type inhabitation can be used to construct (all or parts of) programs from the specification given in the 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
Category theory
Although the initial motivation for
category theory
Category theory is a general theory of mathematical structures and their relations. It was introduced by Samuel Eilenberg and Saunders Mac Lane in the middle of the 20th century in their foundational work on algebraic topology. Category theory ...
was far removed from foundationalism, the two fields turned out to have deep connections. As
John Lane Bell writes: "In fact categories can ''themselves'' be viewed as type theories of a certain kind; this fact alone indicates that type theory is much more closely related to category theory than it is to set theory." In brief, a category can be viewed as a type theory by regarding its objects as types (or ''sorts'' ), i.e. "Roughly speaking, a category may be thought of as a type theory shorn of its syntax." A number of significant results follow in this way:
*
cartesian closed 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
Homotopy type theory attempts to combine type theory and category theory. It focuses on equalities, especially equalities between types.
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.
Definitions
Terms and types
Atomic terms
The most basic types are called atoms, and a term whose type is an atom is known as an atomic term. Common atomic terms included in type theories are
natural number
In mathematics, the natural numbers are the numbers 0, 1, 2, 3, and so on, possibly excluding 0. Some start counting with 0, defining the natural numbers as the non-negative integers , while others start with 1, defining them as the positive in ...
s, often notated with the type
,
Boolean logic
In mathematics and mathematical logic, Boolean algebra is a branch of algebra. It differs from elementary algebra in two ways. First, the values of the variable (mathematics), variables are the truth values ''true'' and ''false'', usually denot ...
values (
/
), notated with the type
, and
formal variables, whose type may vary.
For example, the following may be atomic terms.
*
*
*
*
Function terms
In addition to atomic terms, most modern type theories also allow for
functions. Function types introduce an arrow symbol, and are
defined inductively: If
and
are types, then the notation
is the type of a function which takes a
parameter of type
and returns a term of type
. Types of this form are known as
''simple'' types.
Some terms may be declared directly as having a simple type, such as the following term,
, which takes in two natural numbers in sequence and returns one natural number.
Strictly speaking, a simple type only allows for one input and one output, so a more faithful reading of the above type is that
is a function which takes in a natural number and returns a function of the form
. The parentheses clarify that
does not have the type
, which would be a function which takes in a function of natural numbers and returns a natural number. The convention is that the arrow is
right associative, so the parentheses may be dropped from
's type.
Lambda terms
New function terms may be constructed using
lambda expressions, and are called lambda terms. These terms are also defined inductively: a lambda term has the form
, where
is a formal variable and
is a term, and its type is notated
, where
is the type of
, and
is the type of
.
The following lambda term represents a function which doubles an input natural number.
The variable is
and (implicit from the lambda term's type) must have type
. The term
has type
, which is seen by applying the function application inference rule twice. Thus, the lambda term has type
, which means it is a function taking a natural number as an
argument
An argument is a series of sentences, statements, or propositions some of which are called premises and one is the conclusion. The purpose of an argument is to give reasons for one's conclusion via justification, explanation, and/or persu ...
and returning a natural number.
A lambda term is often referred to as an
anonymous function because it lacks a name. The concept of anonymous functions appears in many programming languages.
Inference Rules
Function application
The power of type theories is in specifying how terms may be combined by way of
inference rules.
Type theories which have functions also have the inference rule of
function application
In mathematics, function application is the act of applying a function to an argument from its domain so as to obtain the corresponding value from its range. In this sense, function application can be thought of as the opposite of function abs ...
: if
is a term of type
, and
is a term of type
, then the application of
to
, often written
, has type
. For example, if one knows the type notations
,
, and
, then the following type notations can be
deduced from function application.
*
*
*
Parentheses indicate the
order of operations; however, by convention, function application is
left associative, so parentheses can be dropped where appropriate.
In the case of the three examples above, all parentheses could be omitted from the first two, and the third may simplified to
.
Reductions
Type theories that allow for lambda terms also include inference rules known as
-reduction and
-reduction. They generalize the notion of function application to lambda terms. Symbolically, they are written
*