Topics in Dependent Type Theory

Supervisors:

Prof. dr. Dominique Devriese, dominique.devriese@kuleuven.be
Dr. Andreas Nuyts, andreas.nuyts@kuleuven.be

Event in April

If you want to get a taste of (homotopy) type theory, you can consider to attend (part of) two events on this subject taking place in building 200A on Apr 2-5, 2024:

Apr 2-3: The annual Workshop on Homotopy Type Theory / Univalent Foundations (HoTT/UF),
Apr 4-5: A meeting of EuroProofNet work group 6 on type theory.

Attendance is free. If you plan to attend full days, we ask to register for organizational reasons.

Dependent Type Theory

Martin-Löf type theory (MLTT) [ML82, ML84] is a formal system introduced by Per Martin-Löf as an alternative to set theory. MLTT can serve both as a logic and as a programming language. These two aspects are seamlessly combined in a single formalism using the Curry-Howard correspondence, which encodes propositions as program types, and proofs as programs of the appropriate type. For example,

for every assumption, which is a proposition encoded as a type, the program takes an argument of that type, to be instantiated with a proof that the assumption holds,
for every universal quantification, the program takes an argument, to be instantiated with any object of the type being quantified over, and proceeds to prove the property that this object must satisfy,
for every existential quantification, the program computes a witness of the type being quantified over, and proceeds to prove the property that this witness must satisfy,
for every disjunction, the program will let you know which side of the disjunction it is going to prove, and proceeds to prove that side.

As a logic, MLTT can replace Zermelo-Fraenkel set theory as a foundation for mathematics. In other words, it is possible to express general mathematical theorems and proofs within MLTT, and the expressive power of MLTT is similar to that of set theory. However, MLTT has a number of advantages, compared to set theory:

Constructivity: from a proof that there exists an object with a certain property, we can actually reconstruct the object in question.
Mechanizable proof-checking: when a proof is fully spelled out according to the formal rules of the logic (which is a considerable amount of work and is therefore almost never done for set-theoretic proofs!), a computer can check whether it is indeed a proof of the theorem it claims to prove and if not, will often be able to give useful indications of where the reasoning was flawed or a corner case was missed.
Greater abstraction: natural numbers are not constructed as bizarre sets, but as objects of their own type.

As a programming language, it has the advantage that it can check safety and correctness of programs at compile-time. This is achieved by running a type-checker (which is the exact same algorithm as the proof-checker mentioned above), which will verify

that the program terminates without errors regardless of the (well-typed) input,
that the output has the right type regardless of the (well-typed) input,
that the program satisfies its specification; any formal specification can in principle be expressed since the type system provides all logical operators.

MLTT is part of a broader family of foundational mathematical theories called dependent type theories. Examples of dependently typed proof assistants include Agda, Coq (to be renamed to Rocq), Lean and Idris. A more exhaustive list is found on Wikipedia. Those systems are also called proof-assistants, as the user may input a proof (a computer program) interactively, that is, with constant feedback from the type-checker.

Equality in Type Theory

Equality is an important topic of interest in type theory. We distinguish two forms of equality:

When two objects reduce to the same thing, constructed in the same way, simply by unfolding definitions, we call them definitionally or judgementally equal. Definitional equality can be observed by the type-checker, which usually only considers objects up to definitional equality.
Sometimes, equality of objects cannot simply be observed by unfolding definitions, but needs to be actively proven, making use of the current assumptions. For example, in a group G with neutral element e, if we know that a^5 = e and a^7 = e, then we can conclude that a = e, but this does not follow simply from unfolding definitions. We call this propositional equality and, being a proposition, it is encoded by a type a ≡ e called the identity type. Propositional equality is strictly weaker than definitional equality.

The fact that we have an identity type a ≡ b for a, b : A (a and b of type A) means that we can consider objects p : a ≡ b of the identity type, called equality/identity proofs. One wonders how we should think and reason about these. First, we should note that these proofs have a role not only in further proving activities but also in programming. Indeed, if T(x) is a type dependent on x : A and we have a proof p : a ≡ b, then we are allowed to convert programs of type T(a) to programs of type T(b), via a function subst(T)(p) : T(a) -> T(b) (as present in both the Agda standard library and the Agda cubical library). However, since the types T(a) and T(b) may not be definitionally equal, they may classify different programs, and as such, the conversion function subst(T)(p) : T(a) -> T(b) actually has to perform a computation. This computation needs to be derived from T and p, so p is not just a proof of a fact, but actually carries the computationally relevant information about how to get from a to b.

There are several takes on what an equality proof is:

In intensional type theory (ITT), propositional equality is essentially just the congruence generated by all equalities currently assumed. As such, if we have p : a ≡ b, then after all variables that p depends on have been instantiated with concrete values, it must be the case that a and b are really (definitionally) the same, and p reduces to refl (short for reflexivity): the proof that (definitionally) equal objects are indeed (propositionally) equal. Evaluation of subst(T)(p) simply waits until p reduces to refl, and then subst(T)(refl) reduces to the identity function.

Problematically, function extensionality – the fact that pointwise equal functions are equal – is not provable in ITT and is therefore often assumed without proof. But this means that there is an object funext whose existence has been postulated without providing computational content, and which is never instantiated with a concrete value. As such, conversion along equalities proven using funext will block.
In homotopy type theory (HoTT) [Uni13], propositional equality just means isomorphism, and equality proofs are in 1-1 correspondence with isomorphisms. Clearly then, even after instantiating all variables in a proof p, it can still by any isomorphism and definitional equality will not be guaranteed. Thus, a computational theory of HoTT will be more complex. Early versions of HoTT would simply block on certain axioms, but cubical type theory [CCHM15] is a type system that extends HoTT and fully computes. It derives its name from the fact that it has a semantics in cubical sets (presheaves over the “cube category”). With the option --cubical enabled, Agda acts as a proof assistant for cubical type theory [VMA21]. A relatively extensive standard library containing a significant module for category theory exists for Agda --cubical.
XTT [SAG22] is a type system in which equality proofs are regarded as in ITT, but it uses techniques from cubical type theory to allow computation with equality proofs even before they reduce to refl. Moreover, function extensionality is provable in XTT. For these reasons, we regard XTT as currently the most convenient system to work in when we care about computation, but do not need the full power of HoTT. To our knowledge there is currently no proof assistant for XTT, but it is sufficiently close to cubical type theory that we can simply use Agda --cubical.

Universal Algebra and Programming Languages

Universal algebra is the study of algebraic theories without commiting to a specific one (such as group theory). An algebraic theory can be specified by listing a number of operations, each with an arity, and a number of equations.

Simple or un(i)sorted algebraic theories are theories whose algebras have only a single carrier and examples are group theory, ring theory, linear algebra over a fixed field (if we have a separate unary rescaling operation for every scalar in the field), …, but also unscoped and un(i)typed programming languages.
Multisorted algebraic theories (MATs) allow more than a single carrier. Examples are: the theory of pairs of a field and a vector space over it, but also typed programming languages.
Generalized algebraic theories (GATs) [Car86, KKA19] allow carriers to depend on objects. Examples are: category theory, where there is a carrier Hom(x, y) for every two objects x and y, but also dependently typed programming languages.
Second-order algebraic theories (SO*ATs) [FM13, FS22, Uem19] extend the above notions with special support for variable binding and substitution and are a good abstraction for languages with anonymous user-defined functions (lambda-expressions).

When we specify an algebraic theory, we get:

a syntax up to equality, freely generated by its operators and then quotiented by its equations,
a category of models/algebras of the theory.

The framework of algebraic theories is of interest to mathematics, but also to the study of programming languages and proof assistants. Models of a programming language can be denotational models in which we study a logic’s soundness (a.k.a. consistency), but remarkably, important parts of a programming language implementation such as a type-checker and a compiler can also be made to fit the definition of a model/algebra of an algebraic theory and this turns out to be a good way to structure the implementation’s source code [AACMM21, FS22].

Possible Subjects

We propose the option to work on a master thesis related to the concepts above, and including formalization work in Agda --cubical, likely leading to contributions to the standard cubical library.

Formalization of one or more of the above notions of algebraic theories, including their syntax and categories of algebras/models, in Agda --cubical. There are currently formalizations of SOMATs in plain Agda (using a possibly unnecessary detour where presheaves are represented as □-coalgebras) and MATs in Cubical Agda.
Porting or reconstructing part of the Sikkel project [CND22] – a formalization and implementation of multimodal type theory and its general presheaf model, in Agda using XTT (Agda --cubical) as a metatheory. This should simplify parts of the existing implementation, and non-Sikkel-specific concepts would be contributed to the cubical library.
Formalize interesting categorical concepts in Agda --cubical as contributions to the cubical library.
When defining a mathematical concept in type theory, there are often multiple ways to do so, which may or may not lead to equivalent notions. Even when equivalent, one definition may be more practical to work with than another. A master thesis could further explore a different definition of functors and natural transformations than the one that is currently present in the Agda libraries.

A thesis on these subjects can be written in either Dutch or English.

Relevant courses

Courses particularly relevant here (but not indispensable) are:

Formal Systems and their Applications, which can be taken as part of the master in mathematics.
Commutative Algebra, especially because of the category theory content.
Wiskundige Logica, mostly as background knowledge.

References

This is the list of references that are appropriate in the text above, but the cited papers are not necessarily the best point to start reading. See “Further reading” above instead.

AACMM21: Allais, G., Atkey, R., Chapman, J., McBride, C., & McKinna, J. (2021). A type- and scope-safe universe of syntaxes with binding: their semantics and proofs. J. Funct. Program., 31, e22. https://doi.org/10.1017/S0956796820000076
Car86: Cartmell, J. (1986). Generalised algebraic theories and contextual categories. Ann. Pure Appl. Logic, 32, 209–243. https://doi.org/10.1016/0168-0072(86)90053-9
CCHM15: Cohen, C., Coquand, T., Huber, S., & Mörtberg, A. (2015). Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In T. Uustalu (Ed.), 21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia (Vol. 69, p. 5:1 - 5:34). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.TYPES.2015.5
Ceulemans, J., Nuyts, A., & Devriese, D. (2022). Sikkel: Multimode Simple Type Theory as an Agda Library. In J. Gibbons & M. S. New (Eds.), Proceedings Ninth Workshop on Mathematically Structured Functional Programming, MSFP@ETAPS 2022, Munich, Germany, 2nd April 2022 (Vol. 360, pp. 93–112). https://doi.org/10.4204/EPTCS.360.5
FM13: Fiore, M. P., & Mahmoud, O. (2013). Second-Order Algebraic Theories. CoRR, abs/1308.5409. http://arxiv.org/abs/1308.5409
FS22: Fiore, M., & Szamozvancev, D. (2022). Formal metatheory of second-order abstract syntax. Proc. ACM Program. Lang., 6(POPL), 1–29. https://doi.org/10.1145/3498715
KKA19: Kaposi, A., Kovács, A., & Altenkirch, T. (2019). Constructing quotient inductive-inductive types. Proc. ACM Program. Lang., 3(POPL), 2:1-2:24. https://doi.org/10.1145/3290315
ML82: Martin-Löf, P. (1982). Constructive mathematics and computer programming. Logic, Methodology and Philosophy of Science VI, 153–175.
ML84: Martin-Löf, P. (1984). Intuitionistic type theory. In Studies in proof theory. Bibliopolis.
SAG22: Sterling, J., Angiuli, C., & Gratzer, D. (2022). A Cubical Language for Bishop Sets. Log. Methods Comput. Sci., 18(1). https://doi.org/10.46298/LMCS-18(1:43)2022
Uem19: Uemura, T. (2019). A General Framework for the Semantics of Type Theory. CoRR, abs/1904.04097. http://arxiv.org/abs/1904.04097
Uni13: Univalent Foundations Program, T. (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book.
VMA21: Vezzosi, A., Mörtberg, A., & Abel, A. (2021). Cubical Agda: A dependently typed programming language with univalence and higher inductive types. J. Funct. Program., 31, e8. https://doi.org/10.1017/S0956796821000034