I've thought for quite a while now that darcs' patch theory doesn't quite go far enough -- in particular, mergers don't end up being quite consistent or behave quite correctly, and it also makes things hard to reason about, which leads to suboptimal, and even exponential, performance.
And of course, other people have thought the same, and there's even a mailing list called [http://abridgegame.org/pipermail/darcs-conflicts/ darcs-conflicts] now.
= Basic Theory =
== Definition ==
There are two types of things, repositories and patches. A repository is some data, that can be changed, and a patch is a way of changing data. A patch can be applied to many different repositories, but not necessarily all of them.
In reality, any repository can be built up starting from the empty repository, and applying patches to it. (Though this need not be the case, for the theory)
We write $R' = R + P$ to indicate the repository $R'$ resulting from applying the patch $P$ to repository $R$. The $+$ operator is left associative, so $R + P_1 + P_2 \doteq (R + P_1) + P_2$.
We write $P_1 \oplus P_2$ to denote the combination of two patches. The $\oplus$ operator is defined as $R + (P_1 \oplus P_2) \doteq R + P_1 + P_2$.
We define the $\oplus$ operator as having higher precedence than $+$, thus $R + P_1 \oplus P_2 \doteq R + (P_1 \oplus P_2)$.
Furthermore we can establish that $\oplus$ is associative, that is $(P_1 \oplus P_2) \oplus P_3 = P_1 \oplus (P_2 \oplus P_3)$. This is easily seen, since, for any repository $R$:
{{{#!latex
\begin{eqnarray*}
R + (P_1 \oplus P_2) oplus P_3 & = & R + (P_1 \oplus P_2) + P_3 \\
& = & R + P_1 + P_2 + P_3 \\
& = & R + P_1 + (P_2 \oplus P_3) \\
& = & R + P_1 \oplus (P_2 \oplus P_3) \\
\end{eqnarray*}
}}}
We write $dom(P)$ to obtain the set of repositories $P$ can be applied to. Note that $dom(P_1 \oplus P_2) \subseteq dom(P_1)$. Additionally, $ran(P) = \{ R + P | R \in dom(P) \}$
== Comparison ==
We say $P = Q$ iff $\forall R \in dom(P) \cap dom(Q), R \oplus P = R + Q$
We say $P \leq Q$ iff $P = Q \wedge dom(P) \subseteq dom(Q)$.
We say $P \equiv Q$ iff $P = Q \wedge dom(P) = dom(Q)$.
== Zero ==
'''REQUIREMENT:''' There is a null patch, called $0$, which applies to any repository and does not change that repository.
== Inversion ==
For our purposes, patches are required to be expressed in a way that allows them to be inverted.
'''REQUIREMENT:''' The inverse of a patch $P$, is written as $-P$, and defined such that $P \oplus -P \leq 0$. Furthermore, $dom(-P) = ran(P)$, and $ran(-P) = dom(P)$, and $-P$ always exists.
Note that $P \oplus -P \oplus P = P$ and thus $-P \oplus P \leq 0$ thus $-(-P) = P$.
Note that $-(P \oplus Q) \doteq -Q \oplus P$.
== Commutation ==
One of the more useful things to be able to do with a sequence of patches is to reorder them, while preserving the overall meaning. This is called commutation, represented by $(P,Q) \rightleftharpoons (Q',P')$.
'''REQUIREMENT:''' All patches that commute, maintain the property $P \oplus Q \equiv Q' \oplus P'$.
Not all patches can commute; patches that do not commute are said to be dependant. We denote the property that $P$ and $Q$ can commute by writing $P \sim Q$.
'''REQUIREMENT:''' For all P, $(P,0) \rightleftharpoons (0,P)$. That is, $P$ and $0$ commute trivially.
'''REQUIREMENT:''' $(P_1 \oplus P_2, Q) \rightleftharpoons (Q', P'_1 \oplus P'_2)$ if and only if $(P_2, Q) \rightleftharpoons (P'_2, Q_m)$ and $(P_1, Q_m) \rightleftharpoons (Q', P'_1)$.
'''REQUIREMENT:''' Additionally, though, we need to have inverses commute. This is pretty simple, given $(P,Q) \rightleftharpoons (Q',P')$ we simply require that $(-Q,-P) \rightleftharpoons (-P',-Q')$. This is fairly trivial, since $0 \leq P \oplus Q \oplus -Q \oplus -P \equiv Q' \oplus P' \oplus -P' \oplus -Q'$.
I'm not sure if there's some sort of stablity property required too. How do you establish that $(P, Q) \rightleftharpoons (Q',P')$ implies $(P',-Q) \rightleftharpoons (-Q',P)$?
Note that commutation is required to be a function, so we can treat $\rightleftharpoons$ as a function on its preceeding argument, as well as an equivalence relation.
Additionally, we define the notation $(P,Q) \rightleftharpoons (\alpha_P(Q),\omega_Q(P))$. We can then note that since $(-Q,-P) \rightleftharpoons (\alpha_{-Q}(-P),\omega_{-P}(-Q))$ then $-\omega_Q(P) = \alpha_{-Q}{-P}$ and $-\alpha_P(Q) = \omega_{-P}(-Q)$.
Maybe we should note some more properties of $\alpha$ and $\omega$ here?
== Merging ==
This allows us to define a merge operator, $\otimes$. Merging occurs when we have two patches which apply to the same repository, and wish to adapt those patches so they can be applied simultaneously without changing the meaning.
{{{#!latex
\begin{eqnarray*}
Q & = & 0 \oplus Q \\
& = & P \oplus -P \oplus Q \\
& = & P \oplus \alpha_{-P}(Q) \oplus \omega_Q(-P) \\
\\
P \otimes Q & \doteq & P \oplus \alpha_{-P}(Q) \\
& = & P \oplus \alpha_{-P}(Q) \oplus \omega_Q(-P) \oplus -\omega_Q(-P) \\
& = & P \oplus -P \oplus Q \oplus -\omega_Q(-P) \\
& = & 0 \oplus Q \oplus -\omega_Q(-P) \\
& = & Q \oplus \alpha_{-Q}(-P) \\
& = & Q \otimes P \\
\end{eqnarray*}
}}}
Obviously the merge operator can only be applied if $-P \sim Q$.
By construction, we see that $\otimes$ is commutative. We can also determine $\oplus$ in terms of $\otimes$.
{{{#!latex
\begin{eqnarray*}
P \oplus Q & = & P \oplus -P \oplus P \oplus Q \\
& = & P \oplus -P \oplus \alpha_{P}(Q) \oplus \omega_{Q}(P) \\
& = & P \oplus \alpha_{-P}\left(\alpha_{P}(Q)\right) \oplus -\omega_{Q}(P) \oplus \omega_{Q}(P) \\
& = & P \otimes \alpha_{P}(Q) \\
\end{eqnarray*}
}}}
Obviously, this relationship only applies if $P$ and $Q$ commute.
We can also establish that $\otimes$ is associative:
{{{#!latex
\begin{eqnarray*}
(P_1 \otimes P_2) \otimes P_3 & = & (P_1 \otimes P_2) \oplus \alpha_{-(P_1 \otimes P_2)}(P_3) \\\
& = & (P_1 \otimes P_2) \oplus \alpha_{-(P_1 \oplus \alpha_{-P_1}(P_2))}(P_3) \\\
& = & (P_1 \otimes P_2) \oplus \alpha_{-\alpha_{-P_1}(P_2) + -P_1)}(P_3) \\\
& = & (P_1 \otimes P_2) \oplus \alpha_{-P_1}(\alpha_{-P_2}(P_3)) \\\
& = & P_1 \oplus \alpha_{-P_1}(P_2) \oplus \alpha_{-P_1}(\alpha_{-P_2}(P_3)) \\\
& = & P_1 \oplus \alpha_{-P_1}(P_2 \oplus \alpha_{-P_2}(P_3)) \\\
& = & P_1 \otimes (P_2 \oplus \alpha_{-P_2}(P_3)) \\\
& = & P_1 \otimes (P_2 \otimes P_3) \\\
\end{eqnarray*}
}}}
If $-P \sim Q$ we say $P$ and $Q$ can be merged, and annotate this as $P \parallel Q$. If they do not commute, we say that $P$ and $Q$ conflict.
This allows us to define the merge function $(P,Q) \Rightarrow (P',Q')$. Note it is also the case that $(Q,P) \Rightarrow (Q',P')$ and $(P,Q') \rightleftharpoons (Q,P')$.
We can trivially define a corresponding unmerge operation as $(P',Q') \Leftarrow (P,Q)$ where $(-P,-Q) \Rightarrow (-P',-Q')$.
{{{#!latex
\begin{eqnarray*}
P + Q & \equiv & Q' + P' \\
\\
\underline{(P,Q)} & \rightleftharpoons & (Q',P') \\
\underline{(Q',P')} & \rightleftharpoons & (P,Q) \\
\underline{(P,Q')} & \Rightarrow & (P',Q) \\
(P,Q') & \Leftarrow & \underline{(P',Q)} \\
\\
P \sim Q & \equiv & -P \sim Q' \\
& \equiv & P' \sim -Q \\
& \equiv & Q' \sim P' \\
\\
P \parallel Q' & \equiv & -P' \parallel -Q \\
\end{eqnarray*}
}}}
Given the underlined terms in the expressions, the remaining terms can be found.
I wonder how many of those are axioms... Hopefully none?
= Unmerging =
We can similarly define an unmerge operator $\odot$, as $P \odot Q = -\left( (-P) \otimes (-Q) \right)$. Note that $\odot$ has the property that if $(P,Q) \Rightarrow (P',Q')$ then $P \otimes Q = P' \odot Q'$, which can be seen by noting
{{{#!latex
\begin{eqnarray*}
P' \odot Q' & = & -((-P') \otimes (-Q')) \\
& = & -(-P' \oplus \alpha_{P'}(-Q')) \\
& = & -(-P' \oplus -Q) \\
& = & -(-(Q \oplus P')) \\
& = & (Q \oplus P') \\
& = & Q \otimes P \\
& = & P \otimes Q \\
\end{eqnarray*}
}}}
Commutativity is obvious from the definition; associativity can be seen by noting:
{{{#!latex
\begin{eqnarray*}
P_1 \odot (P_2 \odot P_3) & = & P_1 \odot (-(-P_2 \otimes -P_3)) \\
& = & -(-P_1 \otimes -(-(-P_2 \otimes -P_3))) \\
& = & -(-P_1 \otimes (-P_2 \otimes -P_3)) \\
& = & -((-P_1 \otimes -P_2) \otimes -P_3)) \\
& = & -(-(P_1 \odot P_2) \otimes -P_3) \\
& = & (P_1 \odot P_2) \odot P_3 \\
\end{eqnarray*}
}}}
= Applying the concepts =
All this is very well, but we really don't want to think about individual patches, but rather sets of patches.
== Representation ==
So, we'd like to be able to theorise about patchsets in two ways. One is obviously a series of patches, applied in order. This is the way people work.
This is pretty easy to deal with: given a sequence of patches, $P_1, ..., P_n$ to be applied to a repository in order, and given $R_0$ as the repository's initial state, then we can write $R = R_0 + \bigoplus_{i=1}^n P_i$.
The other is as a '''set''' of patches, where order is unimportant, and the only question is whether or not you have a patch in your repository or not. Since $\otimes$ and $\odot$ are commutative and associative, we're able to apply them to a set of patches without concerning ourselves with the order of those patches. Isn't that awesome? :)
The general result we then want to achieve is, to be able to "cherrypick" patches -- that is, given any repository, we want to be able to choose a single patch, and using commutation, formulate it into something that can be applied to our repository.
For this to work, we require the property that any two patches commute. However we need this anyway otherwise, since otherwise we would have the problem that given patches $(P,Q)$ that don't commute, we would be unable to merge $P^{-1}$ and $Q$.
Given the possibility of any two patches commuting, we can devise a way of expressing a set of patches uniquely independent of ordering by considering patches, not in the form they were applied but as though they had been commuted to be the first patch applied. Thus if we have $R = R_0 + \bigoplus_{i=1}^n P_i$ we can say $U_{n+1} = \{ \}$ and $U_{n-1} = \{ P_{n-1} \} \cup \{ p' | \forall p \in P_n \cdot p' = \alpha_{P_{n-1}}(p) \}$, then $R = R_0 + \bigoplus_{i=1}^k + \bigotimes U_{k+1}$.
(To be fair, we may be talking about multisets here; though adding an identifier to patches of some sort will remove that caveat)
Note that if we use the above to define a function from $\{P_i | i=1 \ldots n\}$ to $U_0$, we have a mapping from a sequence of patches to a (multi)set of patches, that is stable under commutation of the original sequence. Useful, hey! We'll call that function $U$ for unmerge. We can define a similar function $M$ for merge, such that given a sequence of patches $S$, then $\bigoplus S = \bigotimes U(S) = \bigodot M(S)$.
A combination of these representations is to take $S = S_1 \oplus S_2$ and use $(M(S_1),U(S_2))$. This is convenient for defining the {{{pull}}} operation, where you have two patchsets, $S_a$ and $S_b$, which have a common set of patches. Representing $S_a = M(C) \oplus U(A)$ and $S_b = M(B) \oplus U(B)$ allows us to merge the two repositories by constructing $S_c = M(C) \oplus U(A \cup B)$.
Hrm. This is cool and all, but I don't actually make use of it for analysing anything much yet. The theory was that it'd make it easy to prove that it doesn't matter what order in which you pull/unpull patches, you'll always end up with the same repository, given nothing more than the basic patch properties.
== Identity ==
It's more difficult to think about merge $(M_1,U_1)$ and $(M_2,U_2)$ however: you need to first work out which patches should be considered to already apply to both. This isn't strictly impossible: if you convert both forms to $(0,U'_1)$ and $(0,U'_2)$, you can then take $U_\cap = U_1 \cap U_2$, $(M_\cap,0) = (0,U_\cap)$ to determine the common part of the repositories, and go from there.
That's not so useful in the real world, however, when you might want to generate a conflict when two people independently create the same file, since they might be doing so for different reasons. As such, we can expand the form of patches by adding the concept of ''patch identity'', based on, eg, email address, timestamp, description, random token generated at initial application, UUID, etc.
== Achieving Arbitrary Commutability ==
To achieve arbitrary commutability while still being able to describe patches that "conflict" you need to be able to add some sort of additional information.
So assume you then have simple patches, represented as C(P), and commuted, conflicting patches, $C(P,\diamond{}_P)$, where $\diamond{}_P$ represents some additional information yet to be determined. When $(P,Q) \rightleftharpoons (Q',P')$, then $(C(P),C(Q)) \rightleftharpoons (C(Q'),C(P'))$, however when $Q$ is dependent on $P$, then we commute to $C(Q,\diamond{}_Q)$ and $C(P,\diamond{}_P)$.
The information in $C(Q,\diamond{}_Q)$ needs to be enough to allow us to find some way of applying $Q$ to the repository (eg, we may have difficulties modifying a file that hasn't yet been created). That might be as simple as a note to say "don't do anything, it'll be handled later when another patch is applied". More importantly, it needs to allow us to recreate $C(P,\diamond{}_P)$ when we try to merge $C(Q,\diamond{}_Q)$ and $P$. This must refer to $P$'s identity, to ensure the dependency isn't resolved when a similar but actually independent change is merged, but it needn't do anything more than that.
The information in $C(P,\diamond{}_P)$ on the other hand, needs to be enough to recreate the effect of applying $P + Q$ given however we left the repository after applying $C(Q,\diamond{}_P)$.
== Further requirements ==
So, we need to define:
* $C^{-1}(P_1,\diamond{}_{P_1})$
* $C(P_1,\diamond{}_{P_1}) + C(P_2,\diamond{}_{P_2})$
* $(C(P_1,\diamond{}_{P_1}), C(P_2,\diamond{}_{P_2})) \rightleftharpoons (C(P'_2,\diamond{}_{P'_2}), C(P'_1,\diamond{}_{P'_1})$
And satisfy the properties above, that is:
* If $(P,Q) \rightleftharpoons (Q',P')$ and $Q_2 \leq Q$ then $(P,Q_2) \rightleftharpoons (Q'_2,P')$.
* Inverses commute.
* Merge / commutation properties.
== Random Instantiation Thoughts ==
I think it should work to define a patch as being $P = (\iota_p, p, L, R)$ where $\iota_p$ is the unchanging identity of the patch, $p$ is the intended effect of the patch, and $L$ and $R$ represent patches that were problematic to commute, such that $\bigodot L \oplus (\iota_p, p, \{\}, \{\}) \oplus \bigotimes R = R' \oplus P \oplus L'$.
I'm not sure what that makes the effect of applying $P$; obviously if $L$ and $R$ are empty, it's just a matter of applying $p$. The merge case is probably the most interesting. It gives you $(\iota_b, b, {(-\iota_a, -a, 0, 0)},0)$ and expects that to apply as $-a$. Presumably if $R$ is non-empty, there's already been a "conflicted" patch applied, so that can be a no-op. And if $L$ refers to my $\iota$ then I've already been conflicted with an can be a no-op. Otherwise I just have to apply $\bigodot L \oplus p$, since that couldn't be applied previously. I think it's more complicated than that though.
Inverse: $-(\iota_p, p, L, R)$ means that $\bigodot L \oplus p \oplus \bigotimes R$ made sense, which means $-\bigotimes R \oplus -p \oplus -\bigodot L$ makes sense, which is the same as $\bigodot -R \oplus -p \oplus \bigotimes -L$ which gives us $(-\iota_p, -p, -R, -L)$, which is exactly the sort of elegance we'd like. :)
Commute: We want $(\iota_p, p, L_p, R_p) ~ (\iota_q, q, L_q, R_q)$ always to be true. In that case, we've got $M(L_p) \oplus p \oplus (U(R_p) \otimes Q)$ making sense. That's the same as $M(L_p) \oplus p \oplus Q \oplus U(R'_p)$, which is the same as $M(L_p) \oplus Q' \oplus p' \oplus U(R'_p)$ which is the same as $(M(L'_p) \otimes Q'') \oplus p' \oplus U(R'_p)$. That gives us enough to work out $P' = (\iota_p, p', L'_p, R'_p)$, and a similar argument can work out the others. Well, it would if I knew how to go from $U(P) \otimes q$ to $q' oplus U(P')$ and so forth. And then there's what to do with $Q$. And then there's the possibility that $Q$ or $-Q$ might be in $L_p$ or $R_p$ and conversely. There's also the possibility that $P = -Q$. Arrgghh! :)
== Random Instantiation Thoughts (older) ==
One possibility, which satisfies these requirements, then, is to set $\diamond_P$ to reference $P$'s identity, and $\diamond_Q$ to be the belated application of $Q$. In that case, if $Q$ depends on $P$, their ids are denoted by $\iota{}_P$ and $\iota{}_Q$, we can commute $c(\iota{}_P, P, \{\}, \{\}) + c(\iota{}_Q, Q, \{\}, \{\})$ to
$c(\iota{}_Q, Q, \{\iota{}_P\}, \{\}) + c(\iota{}_P, P, \{\}, \{Q\})$.
Dealing with merging is the same as commuting $(P^{-1}, Q)$. $P^{-1}$ we'll denote as
$c(\iota^{-1}_P, P, \{\}, \{\})$ which gives us $Q' = c(\iota{}_Q, Q, \{\iota^{-1}_P\}, \{\})$.
The check that we need to pass here is that $(P,Q') \rightleftharpoons (Q,P')$. That is,
$(c(\iota{}_P,P,0,0), c(\iota{}_Q,Q,\{\iota^{-1}_P\},0)$ has to commute to
$(c(\iota{}_Q,Q,0,0), c(\iota{}_P,P,\{\iota^{-1}_Q\},0)$.
...
In general, then, commuting $c(\iota{}_P, P, I_P, \Pi{}_P)$ and $c(\iota{}_Q, Q, I_Q, \Pi{}_Q$ should result in $c(\iota{}_P, P', I'_P, \Pi'_P)$ and $c(\iota{}_Q, Q', I'_Q, \Pi'_Q)$ where ...?
Maybe $c(\iota_P, P, \{\iota_{P_1}, \ldots, \iota_{P_n}\}, [(\iota_{Q_1}, Q_1), \ldots, (\iota_{Q_m}, Q_m)])$ is what's needed?
= Conflict Resolution =
It would be nice to be able to resolve conflicts.
That is, given conflicting patches $P$ and $Q$, a patch $P_d$ that depends on $P$, and a patch $Q_d$ that depends on $Q$ we wish to define a resolving patch $R=r(P_r,Q_r)$ that we can add to our repository, giving us $P \oplus Q' \oplus R$. The result should then be that if $(P_r,P_d) \Rightarrow (\underline{~},P'_d)$ then $(Q' \oplus R,P_d) \Rightarrow (\underline{~},P'_d)$ and if $(Q_r,Q_d) \Rightarrow (\underline{~},Q'_d)$ then $(P' \oplus R,Q_d) \Rightarrow (\underline{~},Q'_d)$.
Let's suppose we have a patch $M$ and that $M \parallel P$ and $M \parallel Q$. Then $(P,M) \Rightarrow (\underline{~},P_d)$ and $(Q,M) \Rightarrow (\underline{~},Q_d)$. That is, we want the case where $P_d$ and $Q_d$ don't depend on $P$ or $Q$ and in fact
are the same patch, commuted.
As such, we expect the result to be $P'_d = Q'_d \doteq M'$ since $(P \oplus Q' \oplus R) \otimes M = P \oplus ((Q' \oplus R) \otimes P_d) = P \oplus Q' \oplus R \oplus P'_d$ and this is the same as $(Q \oplus P' \oplus R) \otimes M = Q \oplus ((P' \oplus R) \otimes Q_d) = Q \oplus P' \oplus R \oplus Q'_d$.
Note that $(P_d,P_r) \Rightarrow (M',\underline(~))$ is the same as $(M, P \oplus P_r) \Rightarrow (M',\underline(~))$, and similarly $(M, Q \oplus Q_r) \Rightarrow (M',\underline{~})$.
That is for this to be possible, commuting any patch, $M$, that does not depend on $P$ or $Q$ past either $P \oplus P_r$ or $Q \oplus Q_r$ must result in the same patch $M'$. That's a pretty confusing requirement, so maybe this has been too evil a way of proposing the concept.