Theory of patches

June 17th, 2005 by Wouter

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 f and g.
  • Given two patches f : A \to B and g : B \to C, commuting the patches f and g corresponds to computing the pullback of f 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.

Leave a Reply