Homotopical Patch Theory

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.

This entry was posted in Uncategorized. Bookmark the permalink.

4 Responses to Homotopical Patch Theory

  1. kram1032 says:

    Will there be video coverage of the given talks available somewhere later down the line?

  2. Dan Licata says:

    I think so, yes. I saw a link on twitter (#icfp) to videos from this weekend’s workshops.

  3. kram1032 says:

    For those interested: Here is the recording https://www.youtube.com/watch?v=4yCvTaw1nUg
    Really nice talk!

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s