[darcs-devel] [patch1701] refactorings in the Darcs.Patch subsystem

[Ben Franksen]

Am 25.08.2018 um 16:06 schrieb Ben Franksen:
>>>  * replace naturalMerge with mergeNoConflicts
>>
>> I need to keep thinking about the comment associated with this change.
> 
> I fought with this for a long time. This is perhaps the most difficult
> to understand part of patch theory. The scenario I describe in the
> comment is hard to follow unless you draw yourself a picture. The point
> is that the non-conflicting merge exploits the square-commute law, but
> this law breaks down (in general) when we add conflictors, more
> specifically, it breaks down in the case of a conflicted merge. If we
> used the general commute for mergeNoConflicts (and without the extra
> side-condition that was previously there), then we would use the
> square-commute law in a situation where it no longer applies.

To elaborate a bit:

Suppose p and q are parallel patches that conflict. This means p^ :> q
does not commute (using ^ to mean inverse). We merge them, giving us the
c(q) :/\: c(p) (writing c(x) for the conflictor that represents x). If
we look at this square from the left and apply the square commute law,
we get the absurd result that p^ :> q /does/ commute, namely to c(q) :>
c(p)^, i.e. the force-commute of p and q.

This is not /quite/ a contradiction, from a mathematically POV: the
original judgement that p^ :> q do not commute is a statement about
primitive patches, whereas the result of applying the quare commute law
to the merge square is one about the enlarged type of RepoPatches. It
becomes a contradiction only if we stipulate that the embedding of
primitive patches in the RepoPatch type preserves the commute behavior.
And we do that, see e.g.
/home/ben/src/darcs/screened/src/Darcs/Patch/V2/RepoPatch.hs

Cheers
Ben