Homotopy Type Theory
Lead Research Organisation:
University of Cambridge
Department Name: Computer Science and Technology
Abstract
Type theory was originally developed by Russell as a foundation of mathematics which avoids paradoxes such as Russell's paradox. It was further developed by Church and Martin-Löf, amongst others. Unlike Set Theory, which must be used inside a logical framework such as Higher Order Logic, Martin-Löf's type theory (MLTT, or dependent type theory) internalises the Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic, which corresponds to the computational model of Church's lambda calculus. One notable advantage of this intuitionistic interpretation is that every term in intensional MLTT can be reduced to a canonical form, and every function is computable, whereas in Set Theory it is possible to define incomputable functions. This makes it possible to develop theorem-proving systems where type checking is decidable.
Quotient sets occur widely in mathematics. The current generation of dependently-typed theorem-proving systems do not make it very easy to produce
proofs involving quotients. In informal mathematical practice one often describes constructions on quotient sets by saying what to do on a representative of an equality class, leaving the reader to check that it is well defined, that is, respects the equivalence relation. One aim of this research is to find easier ways to produce formal machine-checked proofs involving Quotient Inductive Types (QITs), ideally in a way that fits better with existing informal mathematical practice. It will build on the techniques researched in Steenkamp's Master's project on QITs. More generally it plans to investigate the use of Higher Inductive Types (HITs) in both theorem proving and functional programming. Two open problems in this field are finding a general schema for HITs, and giving a computational interpretation.
Many researchers have identified the importance of this field, and the implications for mathematics and formal verification techniques should not be
understated. One of the goals of the late Voevodsky and others is: "[T]hat, in a not too distant future, mathematicians will be able to verify the correctness of their own papers [...] in a proof assistant and that doing so will become natural even for pure mathematicians (in the same way that most mathematicians now typeset their own papers in TeX)." - Awodey, Pelayo, Warren (2013). The advantages are clear: Big or complex proofs can be tackled with much higher assurance, and anyone with a computer would have the capability of verifying a proof. This would allow fair assessment of research, not biased by name or status, perhaps leading to faster progress and a greater variety of ideas in mathematical research.
Another major application of type theory research is in the development of type systems for programming languages, which guarantee certain kinds of error cannot occur. Experience has taught us that weakly typed languages result in bug-ridden, unmaintainable code. This is evidenced by the trend in industry away from weakly-typed languages and the recent development of languages with stronger type systems, such as Swift, Go, TypeScript, and C#. One notable example is Rust, in which the type system guarantees memory safety and thread safety. As the scale and complexity of computer programs continues to increase it is vital that research is carried out in type theory to ensure that future programs are robust, particularly in aerospace, medicine, security, and other high-assurance domains.
Existing techniques such as unit tests cannot check for bugs such as "Will this program ever get stuck in an infinite loop?". Formal verification techniques can be used to prove that a program always terminates. Most formal verification techniques require translating the program into a model. This integration of program and proof will increase the adoption of verification tools, and the productivity of software developers using them.
Quotient sets occur widely in mathematics. The current generation of dependently-typed theorem-proving systems do not make it very easy to produce
proofs involving quotients. In informal mathematical practice one often describes constructions on quotient sets by saying what to do on a representative of an equality class, leaving the reader to check that it is well defined, that is, respects the equivalence relation. One aim of this research is to find easier ways to produce formal machine-checked proofs involving Quotient Inductive Types (QITs), ideally in a way that fits better with existing informal mathematical practice. It will build on the techniques researched in Steenkamp's Master's project on QITs. More generally it plans to investigate the use of Higher Inductive Types (HITs) in both theorem proving and functional programming. Two open problems in this field are finding a general schema for HITs, and giving a computational interpretation.
Many researchers have identified the importance of this field, and the implications for mathematics and formal verification techniques should not be
understated. One of the goals of the late Voevodsky and others is: "[T]hat, in a not too distant future, mathematicians will be able to verify the correctness of their own papers [...] in a proof assistant and that doing so will become natural even for pure mathematicians (in the same way that most mathematicians now typeset their own papers in TeX)." - Awodey, Pelayo, Warren (2013). The advantages are clear: Big or complex proofs can be tackled with much higher assurance, and anyone with a computer would have the capability of verifying a proof. This would allow fair assessment of research, not biased by name or status, perhaps leading to faster progress and a greater variety of ideas in mathematical research.
Another major application of type theory research is in the development of type systems for programming languages, which guarantee certain kinds of error cannot occur. Experience has taught us that weakly typed languages result in bug-ridden, unmaintainable code. This is evidenced by the trend in industry away from weakly-typed languages and the recent development of languages with stronger type systems, such as Swift, Go, TypeScript, and C#. One notable example is Rust, in which the type system guarantees memory safety and thread safety. As the scale and complexity of computer programs continues to increase it is vital that research is carried out in type theory to ensure that future programs are robust, particularly in aerospace, medicine, security, and other high-assurance domains.
Existing techniques such as unit tests cannot check for bugs such as "Will this program ever get stuck in an infinite loop?". Formal verification techniques can be used to prove that a program always terminates. Most formal verification techniques require translating the program into a model. This integration of program and proof will increase the adoption of verification tools, and the productivity of software developers using them.
Organisations
| Description | The nature of this work is highly technical, and concerns a sub-field of mathematics and theoretical computer science known as type theory. I will briefly explain the nature of our work below as it relates to our main discovery thus far. Our most substantial achievement so far is a construction of (Infinitary) Quotient Inductive Types (QITs). The significance of these can be understood from (at least) two perspectives. From the perspective of type theory, QITs generalise the notion of inductive types. One may be familiar with the notion of "(generic) algebraic data type" ((G)ADTs) from programming languages such as Ocaml, Rust, Haskell, Swift, Kotlin, C#, etc. These allow for definitions of common data types, such as List, Tree, Maybe, (Option,) Vector (list-with-known-length), Result, Either, and so on, all of which are essential tools in those languages. For example, Option is ubiquitous in Haskell and Result is ubiquitous in Rust. There are other data-types that programmers of these languages would benefit from using, but cannot be expressed as GADTs. For example, un-ordered lists ("multisets"), or rotation-invariant red-black trees. This is because QITs allow expressing not only inductive structure, but also identification structure. As a simple example, it is not possible to directly define integers as an inductive type or GADT: they must either be defined as pairs of subtracted natural numbers, or given an additional sign value (e.g. Bool × Nat). In any case, this means the integers have recursive functions defined directly, instead such functions must break down the non-inductive structure first. To give the simplest example, QITs it is possible to define the integers as follows: 0 : Z + 1 : Z ? Z - 1 : Z ? Z addsub : n + 1 - 1 = n subadd : n - 1 + 1 = n The key advantage being that addsub and subadd are expressible with QITs, but not expressible with GADTs, and so this achievement lays the foundation for adding this feature to proof assistants and programming languages. In particular, most type theories formalised through a proof assistant allow for indexed inductive type definitions, giving a way to work with initial algebras for dependent polynomial functors. With our development we show how to work with indexed quotient inductive type definitions, allowing for initial algebras of polynomial functors with an associated system of equations. The other major perspective is from the mathematical perspective of universal algebra. This is the study of mathematical structures such as monoids, rings, semigroups, and so-on. (To give concrete examples: Integers with addition are an instance of the monoid algebra, and natural numbers with addition and multiplication are an instance of the ring algebra.) All such algebras are characterised by a collection of operations, and a collection of equations. Having constructed QITs, our work provides a semantics (or model) for initial algebras and free algebras for any instance of a universal algebra structure. In particular, this provides a mathematically-justified way of reasoning about universal algebra within type theory. More generally, our work studies the categorical notion of algebra, and we demonstrate how to construct initial and free algebras for a wide class of endofunctors, and moreover do so in constructive mathematics, rather than classical. This is of important practical significance, because, while some of these results are known classically, from the computer science perspective each type requires corresponding computation rules that in turn describe the run-time behaviour of a program. And from the category theory perspective, since this means that our result holds in a wide range of toposes. Additionally, all mathematics done in Homotopy Type Theory must be constructive. This is aside from the various philosophical advantages of constructive mathematics. |
| Exploitation Route | There are many research directions opened up by this work, including but not limited to: - Semantics for Higher Inductive Types (This is one of the major unsolved questions in the field of Homotopy Type Theory). - Equivalence between Generalised Algebraic Theories, Dependent Algebraic Theories, and Natural Deduction Systems. - Type Theory within Type Theory. |
| Sectors | Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software),Education,Electronics,Energy,Financial Services, and Management Consultancy,Security and Diplomacy,Other |
| URL | https://arxiv.org/abs/2101.02994 |
| Title | Agda code supporting "Quotients, Inductive Types and Quotient Inductive Types" (v2) |
| Description | This paper introduces an expressive class of indexed quotient-inductive types, called QWI types, within the framework of constructive type theory. They are initial algebras for indexed families of equational theories with possibly infinitary operators and equations. We prove that QWI types can be derived from quotient types and inductive types in the type theory of toposes with natural number object and universes, provided those universes satisfy the Weakly Initial Set of Covers (WISC) axiom. We do so by constructing QWI types as colimits of a family of approximations to them defined by well-founded recursion over a suitable notion of size, whose definition involves the WISC axiom. We developed the proof and checked it using the Agda theorem prover. |
| Type Of Material | Database/Collection of data |
| Year Produced | 2021 |
| Provided To Others? | Yes |
| Impact | This is the first construction of the type of ordinals described by Blass, and adapted by Lumsdain and Shulman to a 1-HIT, in a type theory that does not have the axiom of choice. |
| URL | https://doi.org/10.17863/CAM.82943 |
| Title | Code supporting "Constructing Initial Algebras Using Inflationary Iteration" |
| Description | Formalization of definitions, theorems and proofs from the paper A. M. Pitts and S. C. Steenkamp, Constructing Initial Algebras Using Inflationary Iteration. In K. Kishida (ed), Fourth International Conference on Applied Category Theory (ACT 2021), EPTCS 2012, to appear. using the Agda theorem-proving system |
| Type Of Material | Database/Collection of data |
| Year Produced | 2021 |
| Provided To Others? | Yes |
| Impact | An old theorem of Adámek constructs initial algebras for sufficiently cocontinuous endofunctors via transfinite iteration over ordinals in classical set theory. We prove a new version that works in constructive logic, using "inflationary" iteration over a notion of size that abstracts from limit ordinals just their transitive, directed and well-founded properties. Borrowing from Taylor's constructive treatment of ordinals, we show that sizes exist with upper bounds for any given signature of indexes. From this it follows that there is a rich class of endofunctors to which the new theorem applies, provided one admits a weak form of choice (WISC) due to Streicher, Moerdijk, van den Berg and Palmgren, and which is known to hold in the internal constructive logic of many kinds of topos. |
| URL | https://www.repository.cam.ac.uk/handle/1810/330134 |