This week at ICFP, Carlo will talk about our paper:

Homotopical Patch Theory

Carlo Angiuli, Ed Morehouse, Dan Licata, Robert Harper

Homotopy type theory is an extension of Martin-Loef type theory, based on a correspondence with homotopy theory and higher category theory. In homotopy type theory, the propositional equality type becomes proof-relevant, and corresponds to paths in a space. This allows for a new class of datatypes, called higher inductive types, which are specified by constructors not only for points but also for paths. In this paper, we consider a programming application of higher inductive types. Version control systems such as Darcs are based on the notion of patches—syntactic representations of edits to a repository. We show how patch theory can be developed in homotopy type theory. Our formulation separates formal theories of patches from their interpretation as edits to repositories. A patch theory is presented as a higher inductive type. Models of a patch theory are given by maps out of that type, which, being functors, automatically preserve the structure of patches. Several standard tools of homotopy theory come into play, demonstrating the use of these methods in a practical programming context.

For people who are interested in HoTT from a programming perspective, we hope that this paper will be a nice starting point for learning about higher inductive types and the line of work on synthetic homotopy theory.  

For experts, one of the interesting things that happened in this paper is that we ended up writing a lot of functions whose computational content we care about, but which map into types that are homotopically trivial.  E.g. a patch optimizer might have type

optimize : (p : Patch) → Σ (q : Patch). p = q

I.e. given a patch, the optimizer produces another patch that behaves the same as the first one.  The result type is contractible, so all functions of this type are equal.  But we care about the computational content of the particular optimization function that we define, which is supposed to make patches simpler, rather than more complex.  Similar things happen in Section 6, where the patch theory itself is contractible (because any repository state can be reached from the initial state), but we still care about the paths computationally.  I think these examples will be a nice test for computational interpretations of HoTT.

Also, there’s some fun cube stuff that goes into showing that the patch theory in Section 6 is contractible, but more on that in another post.