Supervisors:
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 computing evidence. For example,
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:
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
MLTT is part of a broader family of foundational mathematical theories called dependent type theories. Examples of dependently typed proof assistants include Agda, Rocq (formerly called Coq), 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.
We propose the option to work on a master thesis in the area of dependent type theory, and including formalization work in Agda, Lean or Rocq, possibly leading to contributions to the library ecosystem of these languages. Some relevant concepts are further introduced below.
Formalization of one or more notions of algebraic theories, including their syntax and categories of algebras/models, in Agda --cubical or Lean. 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.
Related topics below: Equality in TT, Universal Algebra and PL
Porting or reconstructing part of the (Bi)Sikkel project [CND25, CND22] – a formalization and implementation of multimodal type theory and its general presheaf model, in Agda using XTT (approximated by Agda --cubical=no-glue) as a metatheory. This should simplify parts of the existing implementation, and non-Sikkel-specific concepts would be contributed to the cubical library.
Related topics below: Equality in TT, Universal Algebra and PL
Formalize interesting categorical concepts in Agda --cubical as contributions to the cubical library.
Related topics below: Equality in TT
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.
Related topics below: Equality in TT
Side effects in type theory and (purely) functional programming languages like Haskell, can be supported through a special kind of type functors called monads. These monads can be combined using monad transformers. Container functors (a.k.a. polynomial functors) are a class of well-behaved functors that contain most functors relevant in functional programming. Through combinatorial analysis, it is understood that container comonads (comonads whose underlying functors are container functors) correspond to small categories [AU16], whereas container monads have a close connection to algebraic syntax. A thesis subject could be to map out the combinatorial structure of monad transformers.
Related topics below: Side effects, (Universal Algebra and PL)
Reasoning about effectful programs is currently poorly supported in dependent type theory. A thesis subject could be to explore what can be done specifically for container monads.
Related topics below: Side effects, (Universal Algebra and PL)
As a side effect of my research on dependent type theory, I have accumulated a few conjectures / only roughly proven results related to the theory of strict 2-categories, which have for every two objects x and y a category Hom(x, y), such that composition is a functor. A few of these conjectures are about strictification of pseudofunctors and (op)lax 2-functors, of which some are likely known and some are likely novel. One result connects monotonically increasing functions between finite linear orders, to lax-idempotent 2-monads [Nuy23]. A thesis subject could be to fully prove one or a few of these results, either on paper and/or in a proof assistant.
A thesis on these subjects can be written in either Dutch or English.
Equality is an important topic of interest in type theory. We distinguish two forms of equality:
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, in absence of unproven assumptions, it must be the case that propositionally equal values are in fact definitionally equal, so that any equality proof is ultimately refl: the proof that propositional equality is reflexive. Then subst(T)(refl) is simply the identity.
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. As there are many more isomorphisms than reflexivity proofs, a computational theory of HoTT will be more complex than one of ITT. 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 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 better computation. 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. XTT is said to be implemented in the Aya theorem prover and is closely approximated by Agda --cubical=no-glue.
The Lean proof assistant has its own take on equality, and may have benefits similar to XTT.
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.
Hom(x, y) for every two objects x and y, but also dependently typed programming languages.When we specify an algebraic theory, we get:
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].
Dependent type theory in itself is a pure programming language which means that its functions behave as in mathematics: calling a function with a give input only produces an output; no side effects such as user interaction or memory reads/writes are performed and by consequence the input only determines the output and the output only depends on the input.
Monads are a mathematical construct that computer scientists use to reason about computations with side effects in a pure language. Some examples of monads are:
IO (input-output) monad. A value of type IO(A) is a computation that interacts with the physical world to produce an output of type A. Thus, a function with return value IO(A) must return a value of type A but can interact with the physical world.Maybe monad. A value of type Maybe(A) is either a value of type A, or nothing. Thus, a function with return value Maybe(A) should either fail and return nothing, or successfully return a value of type A.List monad. A value of type List(A) is a list of values of type A. Thus, a function with return value List(A) should return a value of type A, but may fork in the process. For example, we can compute the list of all subsets of a set S by iterating over all elements of S, every time forking the computation, once including the element in the returned set and once discarding it.Monads are well-understood in the setting of simply typed languages (which are less useful for theorem-proving). We are interested in how monads interact with dependently typed languages. Most work on the subject is about allowing a specific single effect throughout the dependently-typed language, and not about allowing arbitrary effects within delimited do-blocks as is possible in simply-typed languages such as Haskell.
If you choose this thesis subject, your first task will be to familiarize yourself with the basic concepts of dependent type theory and the dependently typed programming language Agda, as well as with the concept of monads and the so-called ‘do’-notation. In order to understand monads, prior knowledge of category theory (such as taught in the course on Commutative Algebra) is a plus. After that, the goal of this thesis is to give an overview of what is already known about combining monads and dependent types, and to find one or more creative solutions to problems that present themselves when using monads in dependently typed languages.
Related work:
More accessible resources:
Some fluency with the basic concepts of category theory, and some fluency with programming (ideally even functional programming) would be very recommendable at the start of the thesis.
Courses particularly relevant here (but not indispensable) are:
Relevant resources can be found here.
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.