Nottingham FP Lab Blog

Theory of patches

by Wouter on June 17, 2005.
Tagged as: Lunches.

I gave a brief overview of darcs, a new revision control system written in Haskell, and the theory of patches underlying darcs. The key differences with CVS are:

Every copy of the source tree is a repository
Every repository is defined in terms of a series of patches
Every patch can be inverted to recover the situation before it was applied

There are some interesting observations you can make about the algebraic structure of patches. The ‘repository states’ and patches form a category. In fact, we assume every patch is invertible, so they form a groupoid.

Given this model, it is surprisingly easy to define two key operations on patches.

Given two patches $f,g : A \to B$ the merge of the two patches corresponds to the pushout of and .
Given two patches $f : A \to B$ and $g : B \to C$ , commuting the patches and corresponds to computing the pullback of and $g^{-1}$ .

Thinking about patches in this fashion gives new results. For instance, darcs cannot commute the addition of a file and the file’s subsequent deletion. Given the categorical model, commuting two such patches becomes trivial. Unfortunately, it is not immediately clear how to ‘undo’ the commuting of a patch and its inverse. Commuting two patches can lose information about the original patches.