Programming in homotopy type theory and erasing propositions

Abstract

In the recent years, homotopy type theory has become the subject of much study. Homotopy type theory studies the correspondence between the (propositional) equality in Martin-Löf type theory and the concept of homotopy from topology. The correspondence roughly means that inhabitants of a type can be seen as points of a space and that a propositional equality |x == y| can be seen as a path |x ~~> y|. At the time of writing, virtually all material on the subject is of a rather mathematical nature and focuses on its use in formalising mathematics. This thesis aims to provide an introduction to homotopy type theory geared toward programmers familiar with dependently typed programming, but unfamiliar with topology. We will present applications of homotopy type theory to programming, such as quotient types and dealing with views on abstract types. Furthermore, we will discuss the use of h-propositions to identify parts of a program that are not needed at run-time, compare it to existing methods present in Coq and Agda and discuss whether this can be used to optimise programs. Such an approach works in plain Martin-Löf type theory. In homotopy type theory however, it does not work in general, but we can identify cases in which it still works.