Understanding Darcs/Patch theory

Math and computer science nerds only

(The occasional physicist will be tolerated)

Casual users be warned, the stuff you're about to read is not for the faint of heart! If you're a day-to-day darcs user, you probably do not need to read anything from this page on. However, if you are interested in learning how darcs really works, we invite you to roll up your sleeves, and follow us in this guided tour of the growing Theory of Patches.

What is the theory of patches?

The darcs patch formalism is the underlying "math" which helps us understand how darcs should behave when exchanging patches between repositories. It is implemented in the darcs engine as data structures for representing sequences of patches and Haskell functions equivalent to the operations in the formalism. This section is addressed at two audiences: curious onlookers and people wanting to participate in the development of the darcs core. My aim is to help you understand the intuitions behind all this math, so that you can get up to speed with current conflictors research as fast as possible and start making contributions. You should note that I myself am only starting to learn about patch theory and conflictors, so there may be mistakes ahead.

Why all this math?

One difference between centralized and distributed version control systems is that "merging" is something that we do practically all the time, so it is doubly important that we get merging right. Turning the problem of version control into a math problem has two effects: it lets us abstract all of the irrelevant implementation details away, and it forces us to make sure that whatever techniques we come up with are fundamentally sound, that they do not fall apart when things get increasingly complicated. Unfortunately, math can be difficult for people who do not make use of it on a regular basis, so what we attempt to do in this manual is to ease you into the math through the use of concrete, illustrated examples.

A word of caution though, "getting merging right" does not necessarily consist of having clever behaviour with respect to conflicts. We will begin by focusing on successful, non-conflicting merges and move on to the darcs approach to handling conflicts.

Context, patches and changes

Let us begin with a little shopping. Arjan is working to build a shopping list for the upcoming darcs hackathon. As we speak, his repository contains a single file s_list with the contents

1 apples
2 bananas
3 cookies
4 rice

Note:the numbers you see are just line numbers; they are not part of the file contents

As we will see in this and other examples in this book, we will often need to assign a name to the state of the repository. We call this name a context. For example, we can say that Arjan's repository is a context $o$, defined by there being a file s_list with the contents mentioned above.

the initial context

Arjan makes a modification which consists of adding a line in s_list. His new file looks like this:

1 apples
2 bananas
3 beer
4 cookies
5 rice

When Arjan records this change (adding beer), we produce a patch which tells us not only what contents Arjan added ("beer") but where he added them, namely to line 3 of s_list. We can say that in his repository, we have moved from context $o$ to context $a$ via a patch A. We can write this using a compact notation like ${}^{o}A^{a}$ or using the graphical representation below:

patch A

Sequential patches

Starting from this context, Arjan might decide to make further changes. His new changes would be patches that apply to the context of the previous patches. So if Arjan makes a new patch $B$ on top of this, it would take us from context $a$ to some new context $b$. The next patch would take us from this context to yet another new context $c$, and so on and so forth. Patches which apply on top of each other like this are called sequential patches. We write them in left to right order as in the table below, either representing the contexts explicitly or leaving them out for brevity:

with context	sans context (shorthand)
${}^{o}A^{a}$	$A$
${}^{o}A^{a}B^{b}$	$AB$
${}^{o}A^{a}B^{b}C^{c}$	$ABC$

All darcs repositories are simply sequences of patches as above; however, when performing a complex operation such as an undo or exchanging patches with another user, it becomes absolutely essential that we have some mechanism for rearranging patches and putting them in different orders. Darcs patch theory is essentially about giving a precise definition to the ways in which patches and patch-trees can be manipulated and transformed while maintaining the coherence of the repository.

Inverses

Let's return to the example from the beginning of this module. Arjan has just added beer to our hackathon shopping list, but in a sudden fit of indecisiveness, he reconsiders that thought and wants to undo his change. In our example, this might consist of firing up his text editor and remove the offending line from the shopping list. But what if his changes were complex and hard to keep track of? The better thing to do would be to let darcs figure it out by itself. Darcs does this by computing an inverse patch, that is, a patch which makes the exact opposite change of some other patch:

Definition (Inverse of a patch):

The Inverse of patch $P$ is $P^{-1}$, which is the patch for which the composition $PP^{-1}$ makes no changes to the context and for which the inverse of the inverse is the original patch.

So above, we said that Arjan has created a patch $A$ which adds beer to the shopping list, passing from context $o$ to $a$, or more compactly, ${}^{o}A^{a}$. Now we are going to create the inverse patch $A^{-1}$, which removes beer from the shopping list and brings us back to context $o$. In the compact context-patch notation, we would write this as ${}^{o}A^{a}{A^{-1}}^{o}$. Graphically, we would represent the situation like this:

An inverse patch makes the opposite change of another patch

Patch inverses may seem trivial, but as we will see later on in this module, they are a fundamental operation and absolutely crucial to make some of the fancier stuff -- like merging -- work correctly. One of the rules we impose in darcs is that every patch must have an inverse. These rules are what we call patch properties. A patch property tells us things which must be true about a patch in order for darcs to work. People often like to dream up new kinds of patches to extend darcs's functionality, and defining these patch properties is how we know that their new patch types will behave properly under darcs. The first of these properties is dead simple:

Commutation

Arjan was lucky to realise that he wanted to undo his change as quickly as he did. But what happens if he was a little slower to realise his mistake? What if he makes some other changes before realising that he wants to undo the first change? Is it possible to undo his first change without undoing all the subsequent changes? It sometimes is, but to do so, we need to define an operation called commutation.

Consider a variant of the example above. As usual, Arjan adds beer to the shopping list. Next, he decides to add some pasta on line 5 of the file:

Beer and pasta

The question is how darcs should behave if Arjan now decides that he does not want beer on the shopping list after all. Arjan simply wants to remove the patch that adds the beer, without touching the one which adds pasta. The problem is that darcs repositories are simple, stupid sequences of patches. We can't just remove the beer patch, because then there would no longer be a context for the pasta patch! Arjan's first patch $A$ takes us to context $a$ like so: ${}^{o}A^{a}$, and his second patch takes us to context $b$, notably starting from the initial context $a$: ${}^{a}B^{b}$. Removing patch $A$ would be pulling the rug out from under patch $B$. The trick behind this is to somehow change the order of patches $A$ and $B$. This is precisely what commutation is for:

Why not keep our old patches?

To understand commutation, you should understand why we cannot keep our original patches, but are forced to rely on evil step sisters instead. It helps to work with a concrete example such as the beer and pasta one above. While we could write the sequence $AB$ to represent adding beer and then pasta, simply writing $BA$ for pasta and then beer would be a very foolish thing to do.

Put it this way: what would happen if we applied $B$ before $A$? We add pasta to line 5 of the file:

1 apples
2 bananas
3 cookies
4 rice
5 pasta

Does something seem amiss to you? We continue by adding beer to line 3. If you pay attention to the contents of the end result, you might notice that the order of our list is subtly wrong. Compare the two lists to see why:

$BA$ (wrong!)	$AB$ (right)
1 apples 2 bananas 3 beer 4 cookies 5 rice 6 pasta	1 apples 2 bananas 3 beer 4 cookies 5 pasta 6 rice

It might not matter here because it is only a shopping list, but imagine that it was your PhD thesis, or your computer program to end world hunger. The error is all the more alarming because it is subtle and hard to pick out with the human eye.

The problem is one of context, specifically speaking, the context between $A$ and $B$. In order for instructions like "add pasta to line 5 of s_list" to make any sense, they have to be in the correct context. Fortunately, commutation is easy to do, it produces two new patches $B_{1}$ and $A_{1}$ which perform the same change as $A$ and $B$ but with a different context in between.

Exercises
Patch $A_{1}$ is identical to $A$. It adds "beer" to line 3 of the shopping list. But what should patch $B_{1}$ do?

One more important detail to note though! We said earlier that getting the context right is the motivation behind commutation -- we can't simply apply patches $AB$ in a different order, $BA$ because that would get the context all wrong. But context does not have any effect on whether A and B can commute (or how they should commute). This is strictly a local affair. Conversely, the commutation of A and B does not have any effect either on the global context: the sequences $AB$ and $B_{1}A_{1}$ (where the latter is the commutation of the former) start from the same context and end in the same context.

The complex undo revisited

Now that we know what the commutation operation does, let's see how we can use it to undo a patch that is buried under some other patch. The first thing we do is commute Arjan's beer and pasta patches. This gives us an alternate route to the same context. But notice the small difference between $B$ and $B_{1}$!

commutation gives us two ways to get to the same patch

The purpose of commuting the patches is essentially to push patch $A$ on to end of the list, so that we could simply apply its inverse. Only here, it is not the inverse of $A$ that we want, but the inverse of its evil step sister $A_{1}$. This is what applying that inverse does: it walks us back to the context $b1$, as if we had only applied the pasta patch, but not the beer one.

commutation gives us two ways to get to the same patch

And now the undo is complete. To sum up, when the patch we want to undo is buried under some other patch, we use commutation to squeeze it to the end of the patch sequence, and then compute the inverse of the commuted patch. For the more sequentially minded, this is what the general scheme looks like:

Using commutation to handle a complex undo

Exercises
Imagine the opposite scenario: Arjan had started by adding pasta to the list, and then followed up with the beer. If there was no commutation, what concretely would happen if he tried to remove the pasta patch, and not the beer patch? Work out how this undo would work using commutation. Pay attention to the line numbers.

Commutation and patches

Every time we define a type of patch, we have to define how it commutes with other patches. Most of time, it is very straightforward. When commuting two hunk patches, for instance, we simply adjust their line offset. For instance, we want to put something on line 3 of the file, but if we use patch $Y$ to insert a single line before that, what used to be line 3 now becomes line 4! So patch $X_{1}$ inserts the line "x" into line 4, much like $X$ inserts it into line 3.

Some patches cannot be commuted. For example, you can't commute the addition of a file with adding contents to it. But for now, we focus on patches which can commute.

Merging

Note: this might be a good place to take a break. We are moving on to a new topic and new (but similar) examples

We have presented two fundamental darcs operations: patch inverse and patch commutation. It turns out these two operations are almost all that we need to perform a darcs merge.

Arjan and Ganesh are working together to build a shopping list for the upcoming darcs hackathon. Arjan initialises the repository and adds a file s_list with the contents

1 apples
2 bananas
3 cookies
4 rice

He then records his changes, and Ganesh performs a darcs get to obtain an identical copy of his repository. Notice that Arjan and Ganesh are starting from the same context

the initial context

Arjan makes a modification which consists of adding a line in s_list. His new file looks like this:

1 apples
2 bananas
3 beer
4 cookies
5 rice

Arjan's patch brings him to a new context $a$:

patch A

Now, in his repository, Ganesh also makes a modification; he decides that s_list is a little hard to decipher and renames the file to shopping. Remember, at this point, Ganesh has not seen Arjan's modifications. He's still starting from the original context $o$, and has moved a new context $b$, via his patch $B$:

patch B

Parallel patches

At this point in time, Ganesh decides that it would be useful if he got a copy of Arjan's changes. Roughly speaking we would like to pull Arjan's patch A into Ganesh's repository B. But, there is a major problem! Namely, Arjan's patch takes us from context $o$ to context $a$. Pulling it into Ganesh's repository would involve trying to apply it to context $b$, which we simply do not know how to do. Put another way: Arjan's patch tells us to add a line to file s_list; however, in Ganesh's repository, s_list no longer exists, as it has been moved to shopping. How are we supposed to know that Arjan's change (adding the line "beer") is supposed to apply to the new file shopping instead?

Ganesh attempts to pull from Arjan

Arjan and Ganesh's patches start from the same context o and diverge to different contexts a and b. We say that their patches are parallel to each other, and write it as $A\vee B$. In trying to pull patches from Arjan's repository, we are trying to merge these two patches. The basic approach is to convert the parallel patches into the sequential patches $BA_{1}$, such that $A_{1}$ does essentially the same change as $A$ does, but within the context of b. We want to produce the situation ${}^{o}{B^{b}}{A_{1}^{c}}$

Performing the merge

Converting Arjan and Ganesh's parallel patches into sequential ones requires little more than the inverse and commutation operations that we described earlier in this module:

1. So we're starting out with just Ganesh's patch. In context notation, we are at ${}^{o}{B}^{b}$
2. We calculate the inverse patch $B^{-1}$. The sequence $BB^{-1}$ consists of moving s_list to shopping and then back again. We've walked our way back to the original context: ${}^{o}{B}^{b}{B^{-1}}^{o}$
3. Now we can apply Arjan's patch without worries: ${}^{o}{B}^{b}{B^{-1}}^{o}A^{a}$, but the result does not look very interesting, because we've basically got the same thing Arjan has now, not a merge.
4. All we need to do is commute the last two patches, ${B}^{-1}{A}$, to get a new pair of patches ${A_{1}}{B_{1}}^{-1}$. Still, the end result doesn't seem to look very interesting since it results in exactly the same state as the last step: ${}^{o}{B}^{b}{A_{1}}^{c}{{B_{1}}^{-1}}^{a}$
5. However, one crucial difference is that the second to last patch produces just the state we're looking for! All we now have to do to get at it is to ditch the ${B_{1}}^{-1}$ patch, which is only serving to undo Ganesh's precious work anyway. That is to say, by simply determining how to produce an $A_{1}$ which will commute with $B$, we have determined the version of $A$ which will update Ganesh's repository.

Merging via inverse and commutation

The end result of all this is that we have the patch we're looking for, $A_{1}$ and a successful merge.

We want a new patch A_1

Merging is symmetric

Merging is symmetric

Concretely, we've talked about Ganesh pulling Arjan's patch into his repository, so what about the other way around? Arjan pulling Ganesh's patch into his repository would work the same exact way, only that he is looking for a commuted version of Ganesh's patch $B_{1}$ that would apply to his repository. If Ganesh can pull Arjan's patch in, then Arjan can pull Ganesh's one too, and the result would be exactly the same:

Merging is symmetric

Definition (Merge of two patches):

The result of a merge of two patches $A$ and $B$ is one of two patches $A_{1}$ and $B_{1}$, which satisfy the relationship $A\vee B\Longrightarrow B{A_{1}}\leftrightarrow A{B_{1}}$

The merge definition describes what should happen when you combine two parallel patches into a patch sequence. The built-in symmetry is essential for darcs because a darcs repository is defined entirely by its patches. Put another way,

To be written

The commutation with inverse property

The definition of a merge tells us what we want merging to look like. How did we know how to actually perform that merge? The answer comes out of the following property of commutation and inverse: if you can commute the inverse of a patch $A^{-1}$ with some other patch $B$, then you can also commute the patch itself against $B_{1}$.

Note how the left hand side of this property exactly matches the relationship demanded by the definition of a merge. To see why this all works,

To be written

Definitions and properties

definition of inverse	$AA^{-1}$ has no effect
inverse of an inverse	$(A^{-1})^{-1}=A$
inverse composition property	$(AB)^{-1}=B^{-1}A^{-1}$
definition of commutation	$AB\leftrightarrow {B_{1}}{A_{1}}$
definition of a merge	$A\vee B\Longrightarrow B{A_{1}}\leftrightarrow A{B_{1}}$
commutation with inverse property	$B{A_{1}}\leftrightarrow A{B_{1}}$ if and only if ${B_{1}}{A_{1}}^{-1}\leftrightarrow {A^{-1}}B$