[darcs-users] How to extend a patch theory to fully commute

[Ben Franksen]

>> Conflictors in Darcs can be seen as "internalizing" the relevant parts
>> of the above tree structure /into/ the (conflicted) patch
>> representation. This is the source of their complexity. What we gain
>> form that is the possibility arrange all patches in a repo in a linear
>> sequence where commutation is the only allowed (and required) form of
>> sequence re-arrangement.
> 
> Maybe it would be helpful to formalize this connection. If nothing
> else, it might be an alternative way of explaining the Camp theory.
> Actually, for all I know this is exactly how I'm supposed to think of
> conflictors in Camp. I never fully understood that write-up; maybe I
> should take another look.

In camp/darcs-3 (see src/Darcs/Patch/V3) a conflictor consists of three
parts (all prim patches are of course named):

* The effect (a sequence of prim patches that negate all patches that we
conflict with, unless already negated by a previous conflictor),

* a set of "contexted" (prim) patches (those we conflict with)

* the (prim) patch itself (its "identity"), also as a contexted prim patch.

Contexted patches should be visualized as forking off to the side, the
only part that is actually applied is the effect. The "contexted" here
means that the actual prim patch is prefixed by a sequence of prim
patches that re-context the original patch such that it applies at the
end of the conflictor. The camp paper visualizes this as (arrows point
rightward):

                /
         (context+)conflicts
              /
  *--effect--*--(next patch)--
              \
         (context+)identity
                \

In principle it would be possible to replace the contexted patches in
the set of conflicts with patch names, since it is guaranteed (by a
global invariant) that they must occur in the context (preceding
patches). The above representation makes conflictors self-contained with
respect to commute and merge i.e. we don't have to consult (or know) the
context. Also note that the "context" in a contexted patch usually
consists of negated patches (we have to walk backwards along the history
to reach the patch we reference). BTW, to keep them minimal we do use
cancellation of inverses in these "contexts" and also commute any patch
past (and then drop it) if possible.

The only difficult thing here is to determine the proper side-conditions
when commuting and merging conflictors, so that the patch laws (mainly
permutivity) are satisfied. The source code in Darcs has a number of
comments to explain what is going on but may still be hard to follow for
someone unfamiliar with the code base. The last chapter of teh camp
paper explains each case in detail and motivates the various side
conditions with examples.

The tree view can only be equivalent to this if we somehow store
additional information about which patches are in (direct) conflict with
each other. This is because given only the tree view we cannot
distinguish between a conflict (between say patches d and e) and its
(manual) resolution c (recorded after the conflict), since all three
patches start from the same "context" (node in the tree). In Darcs the
conflict resolution patch *depends* on the conflicted patches, but it
does not conflict with them. Also, whenever we have multiple conflicts
at the same point (say, a conflicts with b, which conflicts with c, but
a doesn't conflict directly with c), then we have to either store or
re-calculate that information because camp conflictors only store direct
conflicts and thus only considers these in the merge and commute rules.

If we have this extra information (as, say, a finite map from patch
names to sets of patch names), and a way to look up the (unique, per
repo) patch representation plus its context (preceding patches) by name,
then we can reconstruct the conflictor representation from that.
Conversely, given a sequence of (possibly conflicted) patches, we can
reconstruct the tree by traversing "contexted" patches in a conflictor
backwards until we reach the patch they reference, then create a branch
of the tree at that point. (This is just a rough sketch but I hope you
get the idea).

I still wonder if a consistent patch theory *different* from
camp/darcs-3 could be devised in which conflict resolutions really are
freely exchangeable with the conflicted patches instead of depending on
them. In other words, we may *choose* one of the conflicting patches as
the resolution (creating a new one if none are suitable). I think this
would require, in the tree view, to add a special flag to mark such
patches as the chosen resolution. This would make the theory more
symmetric and would perhaps also make resolving conflicts easier to
handle; and perhaps simplify commute and merge, too. I haven't thought
this through, though, and it may turn out that this doesn't work.

Cheers
Ben