intuitionistic type theory
   HOME

TheInfoList



OR:

Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory (MLTT)) is a
type theory In mathematics and theoretical computer science, 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 as a foundation of ...
and an alternative
foundation of mathematics Foundations of mathematics are the logical and mathematical framework that allows the development of mathematics without generating self-contradictory theories, and to have reliable concepts of theorems, proofs, algorithms, etc. in particul ...
. Intuitionistic type theory was created by
Per Martin-Löf Per Erik Rutger Martin-Löf (; ; born 8 May 1942) is a Sweden, Swedish logician, philosopher, and mathematical statistics, mathematical statistician. He is internationally renowned for his work on the foundations of probability, statistics, mathe ...
, a Swedish
mathematician A mathematician is someone who uses an extensive knowledge of mathematics in their work, typically to solve mathematical problems. Mathematicians are concerned with numbers, data, quantity, mathematical structure, structure, space, Mathematica ...
and
philosopher Philosophy ('love of wisdom' in Ancient Greek) is a systematic study of general and fundamental questions concerning topics like existence, reason, knowledge, Value (ethics and social sciences), value, mind, and language. It is a rational an ...
, who first published it in 1972. There are multiple versions of the type theory: Martin-Löf proposed both intensional and extensional variants of the theory and early impredicative versions, shown to be inconsistent by Girard's paradox, gave way to predicative versions. However, all versions keep the core design of constructive logic using dependent types.


Design

Martin-Löf designed the type theory on the principles of mathematical constructivism. Constructivism requires any existence proof to contain a "witness". So, any proof of "there exists a prime greater than 1000" must identify a specific number that is both prime and greater than 1000. Intuitionistic type theory accomplished this design goal by internalizing the BHK interpretation. A useful consequence is that proofs become mathematical objects that can be examined, compared, and manipulated. Intuitionistic type theory's type constructors were built to follow a one-to-one correspondence with logical connectives. For example, the logical connective called implication (A \implies B) corresponds to the type of a function (A \to B). This correspondence is called the Curry–Howard isomorphism. Prior type theories had also followed this isomorphism, but Martin-Löf's was the first to extend it to
predicate logic First-order logic, also called predicate logic, predicate calculus, or quantificational logic, is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables ove ...
by introducing dependent types.


Type theory

A type theory is a kind of mathematical
ontology Ontology is the philosophical study of existence, being. It is traditionally understood as the subdiscipline of metaphysics focused on the most general features of reality. As one of the most fundamental concepts, being encompasses all of realit ...
, or foundation, describing the fundamental objects that exist. In the standard foundation,
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 ...
combined with
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 ...
, the fundamental object is the set, which is a container that contains elements. In type theory, the fundamental object is the term, each of which belongs to one and only one type. Intuitionistic type theory has three finite types, which are then composed using five different type constructors. Unlike set theories, type theories are not built on top of a logic like Frege's. So, each feature of the type theory does double duty as a feature of both math and logic.


0 type, 1 type and 2 type

There are three finite types: The 0 type contains no terms. The 1 type contains one canonical term. The 2 type contains two canonical terms. Because the 0 type contains no terms, it is also called the empty type. It is used to represent anything that cannot exist. It is also written \bot and represents anything unprovable (that is, a proof of it cannot exist). As a result,
negation In logic, negation, also called the logical not or logical complement, is an operation (mathematics), operation that takes a Proposition (mathematics), proposition P to another proposition "not P", written \neg P, \mathord P, P^\prime or \over ...
is defined as a function to it: \neg A := A \to \bot. Likewise, the 1 type contains one canonical term and represents existence. It also is called 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 set. ...
. Finally, the 2 type contains two canonical terms. It represents a definite choice between two values. It is used for Boolean values but ''not'' propositions. Propositions are instead represented by particular types. For instance, a true proposition can be represented by the 1 type, while a false proposition can be represented by the 0 type. But we cannot assert that these are the only propositions, i.e. 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 three laws of thought, along with the law of noncontradiction and t ...
does not hold for propositions in intuitionistic type theory.


Σ type constructor

Σ-types contain ordered pairs. As with typical ordered pair (or 2-tuple) types, a Σ-type can describe the
Cartesian product In mathematics, specifically set theory, the Cartesian product of two sets and , denoted , is the set of all ordered pairs where is an element of and is an element of . In terms of set-builder notation, that is A\times B = \. A table c ...
, A \times B, of two other types, A and B. Logically, such an ordered pair would hold a proof of A and a proof of B, so one may see such a type written as A \wedge B. Σ-types are more powerful than typical ordered pair types because of dependent typing. In the ordered pair, the type of the second term can depend on the value of the first term. For example, the first term of the pair might be a
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 ...
and the second term's type might be a
sequence In mathematics, a sequence is an enumerated collection of objects in which repetitions are allowed and order matters. Like a set, it contains members (also called ''elements'', or ''terms''). The number of elements (possibly infinite) is cal ...
of reals of length equal to the first term. Such a type would be written: \sum_ \operatorname(, n) Using set-theory terminology, this is similar to an indexed
disjoint union In mathematics, the disjoint union (or discriminated union) A \sqcup B of the sets and is the set formed from the elements of and labelled (indexed) with the name of the set from which they come. So, an element belonging to both and appe ...
of sets. In the case of the usual cartesian product, the type of the second term does not depend on the value of the first term. Thus the type describing the cartesian product \times is written: \sum_ It is important to note here that the value of the first term, n, is not depended on by the type of the second term, . Σ-types can be used to build up longer dependently-typed
tuple In mathematics, a tuple is a finite sequence or ''ordered list'' of numbers or, more generally, mathematical objects, which are called the ''elements'' of the tuple. An -tuple is a tuple of elements, where is a non-negative integer. There is o ...
s used in mathematics and the records or structs used in most programming languages. An example of a dependently-typed 3-tuple is two integers and a proof that the first integer is smaller than the second integer, described by the type: \sum_ Dependent typing allows Σ-types to serve the role of
existential quantifier Existentialism is a family of philosophy, philosophical views and inquiry that explore the human individual's struggle to lead an Authenticity (philosophy), authentic life despite the apparent Absurdity#The Absurd, absurdity or incomprehensibili ...
. The statement "there exists an n of type , such that P(n) is proven" becomes the type of ordered pairs where the first item is the value n of type and the second item is a proof of P(n). Notice that the type of the second item (proofs of P(n)) depends on the value in the first part of the ordered pair (n). Its type would be: \sum_ P(n)


Π type constructor

Π-types contain functions. As with typical function types, they consist of an input type and an output type. They are more powerful than typical function types however, in that the return type can depend on the input value. Functions in type theory are different from set theory. In set theory, you look up the argument's value in a set of ordered pairs. In type theory, the argument is substituted into a term and then computation ("reduction") is applied to the term. As an example, the type of a function that, given a natural number n, returns a vector containing n real numbers is written: \prod_ \operatorname(, n) When the output type does not depend on the input value, the function type is often simply written with a \to. Thus, \to is the type of functions from natural numbers to real numbers. Such Π-types correspond to logical implication. The logical proposition A \implies B corresponds to the type A \to B, containing functions that take proofs-of-A and return proofs-of-B. This type could be written more consistently as: \prod_ B Π-types are also used in logic for
universal quantification In mathematical logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as "given any", "for all", "for every", or "given an arbitrary element". It expresses that a predicate can be satisfied by e ...
. The statement "for every n of type , P(n) is proven" becomes a function from n of type to proofs of P(n). Thus, given the value for n the function generates a proof that P(\,\cdot\,) holds for that value. The type would be \prod_ P(n)


= type constructor

=-types are created from two terms. Given two terms like 2+2 and 2 \cdot 2, you can create a new type 2+2=2\cdot 2. The terms of that new type represent proofs that the pair reduce to the same canonical term. Thus, since both 2+2 and 2\cdot 2 compute to the canonical term 4, there will be a term of the type 2+2=2\cdot 2. In intuitionistic type theory, there is a single way to introduce =-types and that is by reflexivity: \operatorname \mathbin \prod_ (a = a). It is possible to create =-types such as 1=2 where the terms do not reduce to the same canonical term, but you will be unable to create terms of that new type. In fact, if you were able to create a term of 1=2, you could create a term of \bot. Putting that into a function would generate a function of type 1=2 \to \bot. Since \ldots \to \bot is how intuitionistic type theory defines negation, you would have \neg (1=2) or, finally, 1 \neq 2. Equality of proofs is an area of active research in
proof theory Proof theory is a major branchAccording to , proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. consists of four corresponding parts, with part D being about "Proof The ...
and has led to the development of homotopy type theory and other type theories.


Inductive types

Inductive types allow the creation of complex, self-referential types. For example, a
linked list In computer science, a linked list is a linear collection of data elements whose order is not given by their physical placement in memory. Instead, each element points to the next. It is a data structure consisting of a collection of nodes whi ...
of natural numbers is either an empty list or a pair of a natural number and another linked list. Inductive types can be used to define unbounded mathematical structures like
tree In botany, a tree is a perennial plant with an elongated stem, or trunk, usually supporting branches and leaves. In some usages, the definition of a tree may be narrower, e.g., including only woody plants with secondary growth, only ...
s, graphs, etc.. In fact, the natural numbers type may be defined as an inductive type, either being 0 or the
successor Successor may refer to: * An entity that comes after another (see Succession (disambiguation)) Film and TV * ''The Successor'' (1996 film), a film including Laura Girling * The Successor (2023 film), a French drama film * ''The Successor'' ( ...
of another natural number. Inductive types define new constants, such as zero 0 \mathbin and the successor function S \mathbin \to . Since S does not have a definition and cannot be evaluated using substitution, terms like S 0 and S S S 0 become the canonical terms of the natural numbers. Proofs on inductive types are made possible by induction. Each new inductive type comes with its own inductive rule. To prove a predicate P(\,\cdot\,) for every natural number, you use the following rule: \, \mathbin P(0)\, \to \left(\prod_ P(n) \to P(S(n))\right) \to \prod_ P(n) Inductive types in intuitionistic type theory are defined in terms of W-types, the type of
well-founded In mathematics, a binary relation is called well-founded (or wellfounded or foundational) on a set (mathematics), set or, more generally, a Class (set theory), class if every non-empty subset has a minimal element with respect to ; that is, t ...
trees. Later work in type theory generated coinductive types, induction-recursion, and induction-induction for working on types with more obscure kinds of self-referentiality. Higher inductive types allow equality to be defined between terms.


Universe types

The universe types allow proofs to be written about all the types created with the other type constructors. Every term in the universe type \mathcal_0 can be mapped to a type created with any combination of 0,1,2,\Sigma,\Pi,=, and the inductive type constructor. However, to avoid paradoxes, there is no term in \mathcal_n that maps to \mathcal_n for any \mathcal \in \mathbb. To write proofs about all "the small types" and \mathcal_0, you must use \mathcal_1, which does contain a term for \mathcal_0, but not for itself \mathcal_1. Similarly, for \mathcal_2. There is a predicative hierarchy of universes, so to quantify a proof over any fixed constant k universes, you can use \mathcal_. Universe types are a tricky feature of type theories. Martin-Löf's original type theory had to be changed to account for Girard's paradox. Later research covered topics such as "super universes", " Mahlo universes", and impredicative universes.


Judgements

The formal definition of intuitionistic type theory is written using judgements. For example, in the statement "if A is a type and B is a type then \textstyle \sum_ B is a type" there are judgements of "is a type", "and", and "if ... then ...". The expression \textstyle \sum_ B is not a judgement; it is the type being defined. This second level of the type theory can be confusing, particularly where it comes to equality. There is a judgement of term equality, which might say 4=2+2. It is a statement that two terms reduce to the same canonical term. There is also a judgement of type equality, say that A=B, which means every element of A is an element of the type B and vice versa. At the type level, there is a type 4=2+2 and it contains terms if there is a proof that 4 and 2+2 reduce to the same value. (Terms of this type are generated using the term-equality judgement.) Lastly, there is an English-language level of equality, because we use the word "four" and symbol "4" to refer to the canonical term S S S S 0. Synonyms like these are called "definitionally equal" by Martin-Löf. The description of judgements below is based on the discussion in Nordström, Petersson, and Smith. The formal theory works with ''types'' and ''objects''. A type is declared by: * A\ \mathsf An object exists and is in a type if: * a \mathbin A Objects can be equal * a = b and types can be equal * A = B A type that depends on an object from another type is declared * (x \mathbin A)B and removed by substitution * B / a, replacing the variable x with the object a in B. An object that depends on an object from another type can be done two ways. If the object is "abstracted", then it is written * and removed by substitution * b / a, replacing the variable x with the object a in b. The object-depending-on-object can also be declared as a constant as part of a recursive type. An example of a recursive type is: * 0 \mathbin \mathbb * S \mathbin \mathbb \to \mathbb Here, S is a constant object-depending-on-object. It is not associated with an abstraction. Constants like S can be removed by defining equality. Here the relationship with addition is defined using equality and using pattern matching to handle the recursive aspect of S: : \begin \operatorname &\mathbin\ (\mathbb \times \mathbb) \to \mathbb \\ \operatorname(0, b) &= b \\ \operatorname(S(a), b) &= S(\operatorname(a, b))) \end S is manipulated as an opaque constant - it has no internal structure for substitution. So, objects and types and these relations are used to express formulae in the theory. The following styles of judgements are used to create new objects, types and relations from existing ones: By convention, there is a type that represents all other types. It is called \mathcal (or \operatorname). Since \mathcal is a type, the members of it are objects. There is a dependent type \operatorname that maps each object to its corresponding type. ''In most texts \operatorname is never written.'' From the context of the statement, a reader can almost always tell whether A refers to a type, or whether it refers to the object in \mathcal that corresponds to the type. This is the complete foundation of the theory. Everything else is derived. To implement logic, each proposition is given its own type. The objects in those types represent the different possible ways to prove the proposition. If there is no proof for the proposition, then the type has no objects in it. Operators like "and" and "or" that work on propositions introduce new types and new objects. So A \times B is a type that depends on the type A and the type B. The objects in that dependent type are defined to exist for every pair of objects in A and B. If either A or B have no proof and is an empty type, then the new type representing A \times B is also empty. This can be done for other types (booleans, natural numbers, etc.) and their operators.


Categorical models of type theory

Using the language of
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 ...
, R. A. G. Seely introduced the notion of a locally cartesian closed category (LCCC) as the basic model of type theory. This has been refined by Hofmann and Dybjer to ''Categories with Families'' or ''Categories with Attributes'' based on earlier work by Cartmell. A category with families is a category ''C'' of contexts (in which the objects are contexts, and the context morphisms are substitutions), together with a functor ''T'' : ''C''op → ''Fam''(''Set''). ''Fam''(''Set'') is the category of families of Sets, in which objects are pairs of an "index set" ''A'' and a function ''B'': ''X'' → ''A'', and morphisms are pairs of functions ''f'' : ''A'' → ''A' '' and ''g'' : ''X'' → ''X' '', such that ''B' '' ° ''g'' = ''f'' ° ''B'' – in other words, ''f'' maps ''Ba'' to ''B''''g''(''a''). The functor ''T'' assigns to a context ''G'' a set of types, and for each , a set of terms. The axioms for a functor require that these play harmoniously with substitution. Substitution is usually written in the form ''Af'' or ''af'', where ''A'' is a type in and ''a'' is a term in , and ''f'' is a substitution from ''D'' to ''G''. Here and . The category ''C'' must contain a terminal object (the empty context), and a final object for a form of product called comprehension, or context extension, in which the right element is a type in the context of the left element. If ''G'' is a context, and , then there should be an object final among contexts ''D'' with mappings ''p'' : ''D'' → ''G'', ''q'' : ''Tm''(''D,Ap''). A logical framework, such as Martin-Löf's, takes the form of closure conditions on the context-dependent sets of types and terms: that there should be a type called Set, and for each set a type, that the types should be closed under forms of dependent sum and product, and so forth. A theory such as that of predicative set theory expresses closure conditions on the types of sets and their elements: that they should be closed under operations that reflect dependent sum and product, and under various forms of inductive definition.


Extensional versus intensional

A fundamental distinction is extensional vs intensional type theory. In extensional type theory, definitional (i.e., computational) equality is not distinguished from propositional equality, which requires proof. As a consequence type checking becomes undecidable in extensional type theory because programs in the theory might not terminate. For example, such a theory allows one to give a type to the Y-combinator; a detailed example of this can be found in Nordstöm and Petersson ''Programming in Martin-Löf's Type Theory''. However, this does not prevent extensional type theory from being a basis for a practical tool; for example, Nuprl is based on extensional type theory. In contrast, in intensional type theory
type checking In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a ''type'' (for example, integer, floating point, string) to every '' term'' (a word, phrase, or other set of symbols). Usu ...
is decidable, but the representation of standard mathematical concepts is somewhat more cumbersome, since intensional reasoning requires using setoids or similar constructions. There are many common mathematical objects that are hard to work with or cannot be represented without this, for example, integer numbers,
rational number In mathematics, a rational number is a number that can be expressed as the quotient or fraction of two integers, a numerator and a non-zero denominator . For example, is a rational number, as is every integer (for example, The set of all ...
s, and
real number In mathematics, a real number is a number that can be used to measure a continuous one- dimensional quantity such as a duration or temperature. Here, ''continuous'' means that pairs of values can have arbitrarily small differences. Every re ...
s. Integers and rational numbers can be represented without setoids, but this representation is difficult to work with. Cauchy real numbers cannot be represented without this. Homotopy type theory works on resolving this problem. It allows one to define higher inductive types, which not only define first-order constructors ( values or points), but higher-order constructors, i.e. equalities between elements ( paths), equalities between equalities ( homotopies), ''ad infinitum''.


Implementations of type theory

Different forms of type theory have been implemented as the formal systems underlying a number of
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 edi ...
s. While many are based on Per Martin-Löf's ideas, many have added features, more axioms, or a different philosophical background. For instance, the Nuprl system is based on computational type theory and Coq is based on the calculus of (co)inductive constructions. Dependent types also feature in the design of
programming language A programming language is a system of notation for writing computer programs. Programming languages are described in terms of their Syntax (programming languages), syntax (form) and semantics (computer science), semantics (meaning), usually def ...
s such as ATS, Cayenne,
Epigram An epigram is a brief, interesting, memorable, sometimes surprising or satirical statement. The word derives from the Greek (, "inscription", from [], "to write on, to inscribe"). This literary device has been practiced for over two millennia ...
, Agda (programming language), Agda, and Idris (programming language), Idris.


Martin-Löf type theories

Per Martin-Löf Per Erik Rutger Martin-Löf (; ; born 8 May 1942) is a Sweden, Swedish logician, philosopher, and mathematical statistics, mathematical statistician. He is internationally renowned for his work on the foundations of probability, statistics, mathe ...
constructed several type theories that were published at various times, some of them much later than when the preprints with their description became accessible to specialists (among others Jean-Yves Girard and Giovanni Sambin). The list below attempts to list all the theories that have been described in a printed form and to sketch the key features that distinguished them from each other. All of these theories had dependent products, dependent sums, disjoint unions, finite types and natural numbers. All the theories had the same reduction rules that did not include η-reduction either for dependent products or for dependent sums, except for MLTT79 where the η-reduction for dependent products is added. MLTT71 was the first type theory created by Per Martin-Löf. It appeared in a preprint in 1971. It had one universe, but this universe had a name in itself, i.e., it was a type theory with, as it is called today, "Type in Type". Jean-Yves Girard has shown that this system was inconsistent, and the preprint was never published. MLTT72 was presented in a 1972 preprint that has now been published. That theory had one universe V and no identity types (=-types). The universe was " predicative" in the sense that the dependent product of a family of objects from V over an object that was not in V such as, for example, V itself, was not assumed to be in V. The universe was à la Russell's ''
Principia Mathematica The ''Principia Mathematica'' (often abbreviated ''PM'') is a three-volume work on the foundations of mathematics written by the mathematician–philosophers Alfred North Whitehead and Bertrand Russell and published in 1910, 1912, and 1 ...
'', i.e., one would write directly "T∈V" and "t∈T" (Martin-Löf uses the sign "∈" instead of modern ":") without an added constructor such as "El". MLTT73 was the first definition of a type theory that Per Martin-Löf published (it was presented at the Logic Colloquium '73 and published in 1975). There are identity types, which he describes as "propositions", but since no real distinction between propositions and the rest of the types is introduced the meaning of this is unclear. There is what later acquires the name of J-eliminator but yet without a name (see pp. 94–95). There is in this theory an infinite sequence of universes V0, ..., V''n'', ... . The universes are predicative, à la Russell and ''non-cumulative''. In fact, Corollary 3.10 on p. 115 says that if A∈V''m'' and B∈V''n'' are such that A and B are convertible then ''m'' = ''n''. MLTT79 was presented in 1979 and published in 1982. In this paper, Martin-Löf introduced the four basic types of judgement for the dependent type theory that has since become fundamental in the study of the meta-theory of such systems. He also introduced contexts as a separate concept in it (see p. 161). There are identity types with the J-eliminator (which already appeared in MLTT73 but did not have this name there) but also with the rule that makes the theory "extensional" (p. 169). There are W-types. There is an infinite sequence of predicative universes that ''are cumulative''. Bibliopolis: there is a discussion of a type theory in the ''Bibliopolis'' book from 1984, but it is somewhat open-ended and does not seem to represent a particular set of choices and so there is no specific type theory associated with it.


See also

*
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 ...
* Typed lambda calculus


Notes


References

*


Further reading


Per Martin-Löf's Notes, as recorded by Giovanni Sambin (1980)
* * *


External links



– lecture notes and slides from the Types Summer School 2005

– letter from
John Baez John Carlos Baez ( ; born June 12, 1961) is an American mathematical physicist and a professor of mathematics at the University of California, Riverside (UCR) in Riverside, California. He has worked on spin foams in loop quantum gravity, ap ...
and James Dolan to Ross Street, November 29, 1995 {{DEFAULTSORT:Intuitionistic Type Theory Foundations of mathematics Dependently typed programming Constructivism (mathematics) Type theory Logic in computer science Intuitionism