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

Ben Franksen bugs at darcs.net
Wed Sep 26 21:18:47 UTC 2018


Ben Franksen <ben.franksen at online.de> added the comment:

>>   * add laws to classes Commute and CommuteNoConflicts
> 
>> -- * The more general Square-Commute law
>> --
>> --   prop> commute (p:>q) == Just (q':>p')
>> --              => commute (invert p:>q') == Just (q:>invert p')
>> --
>> --   is required to hold only for primitive patches, i.e. if the is /no/
>> --   instance @'Merge' p@, because together with 'merge' it implies that
>> --   any two patches commute.
> 
> [I reformatted a bit to reduce line length in this comment]
> 
> I had to think a bit about this. It feels unsatisfactory that commute,
> which I tend to see as more primitive than merge, has a law that depends
> on merge. But maybe it's not really more primitive than merge, or conflicts
> just make the whole thing fundamentally hard.

This is a rather deep and quite interesting question about patch theory
in general and one which has bothered me, too. In the end I don't think
commute is any more fundamental, it's just that we decided long ago that
merge is an operation that cannot fail, while for prim patches it would
naturally be one that can fail. So we call it with a different name
(mergeNoConflicts) and indeed I think just as mergeNoConflicts can be
expressed in terms of invert and commuteNoConflicts, commuteNoConflicts
should be expressible in terms of invert and mergeNoConflicts. We can't
do that in our code, of course because that would just give us an
infinite loop.

Anyway, all this is beside the point:

As stated in the docs, Commute does /not/ have a law that depends on
Merge. The only requirement for Commute is the inverse commute law. This
happens to be a specialization of the square commute law, which is /not/
required to hold for Commute. It /is/ required to required to hold for
CommuteNoConflicts, though, and thus for prim patches because for them
commute and commuteNoConflicts coincide.

Another way to think of this is that the breakdown of the square commute
law is the price we have to pay for extending the partial
mergeNoConflicts to the total merge function. I like to think of this in
terms of a coarse analogy, namely moving from real to complex numbers.
You get totality for solving algebraic equations but at the cost of
losing the total order. In fact, this sort of thing happens everywhere
in math: compactifications are perhaps an even better analogy (though
less familiar to non-mathematicians); e.g. we can extend the natural
numbers in such a way that every bounded sequence converges! Isn't that
great? It is called the Stone-Ĉech compactification and the downside of
course is that this weird monster has almost no interesting algebraic
properties left. Less intimidating and closer to patch theory is the
one-point compactification of the positive real numbers (by adding
positive infinity). Here we can extend all the numeric operations as
well as the total order in such a way that almost every law is preserved
(the exception is cancellation).

> I wonder if we can state this instead as something about banning inverse
> conflictors in the right place in the laws for commute or merge.

That would presume knowledge about which constructors are added when we
move from prim patches to repo patches. This is something our type
classes are designed to abstract over, which is a good thing. Either we
can express the properties at the chosen level of abstraction or we must
change the abstraction. I think the distinction between Commute and
CommuteNoConflicts is exactly what is needed here.

>>  * replace naturalMerge with mergeNoConflicts
> 
> I'm trying to really convince myself this is behaviour preserving.
> Here's where I've got so far:
> 
> To summarise the change for V2 patches (V1 patches are similar although
> the order in which commutes are tried is a little more complicated):
> 
> The normal commute first tries to use commuteNoConflicts, and then
> commuteConflicting if that fails:
> 
>   commute = commuteNoConflicts + commuteConflicting
> 
> Summarising the definitions of the old naturalMerge and the new
> mergeNoConflicts, we have:
> 
>       p'
>      --->
>     ^    ^
>     |    |
>    q|    |q'
>     |    |
>      --->
>       p
> 
>   naturalMerge = commute (p^ :> q) ; commute (p :> q')
>   mergeNoConflicts = commuteNoConflicts (p^ :> q)
> 
> so if commuteConflicting (p^ :> q) would succeed and then either
> commuteNoConflicts or commuteConflicting (p :> q') would succeed,
> we have a behaviour difference.

Exactly. Now, commuteConflicting (p :> q') succeeds if and only if q' is
the result of a conflicted merge with p, which implies that
commuteNoConflicts (p^ :> q) fails (we tried that when we merged p and q
and introduced the conflictor because it failed). In the other case,
i.e. commuteNoConflicts (p :> q') succeeds, we know that p and q' do
/not/ conflict i.e. commuteNoConflicts (p^ :> q) succeeds, which
should(!) imply that commuteConflicting p^:>q fails.

With "should" I mean that I think that it shouldn't matter in which
order we try commuteConflicting and commuteNoConflicts: the cases really
are mutually exclusive. I am not 100% sure this is how the code for V2
is written, though.

> Quoting your comment on mergeNoConflicts:
> 
>> Concretely, suppose we use 'commute' here and that @q@ is a conflictor that
>> represents the primitive patch @r@ and conflicts (only) with (primitive
>> patch) @p^@. That is, @q@ results from the conflicted
>> @merge(r:\/:p^)=(s:/\:q)@, where @s@ is another conflictor. Now, according
>> to 'prop_mergeCommute' we get @commute(p^:>q)=Just(r:>s)@, and thus
>> @mergeNoConflict(p:\/:q)=Just(s^:/\:r)@ in contradiction to our assumption
>> that @p^:\/:q@ are in conflict i.e. @mergeNoConflict(p^:\/:q)@ fails.
> 
> How can this situation actually arise in a normal scenario? If we're merging p
> and q then q can't already be a conflictor with p^.

This is not impossible at all, at least in V1 and V2. Let's say in one
repo we have s:=p^, in another we have r which conflicts with s. We pull
r on top of s, giving us s:>q. Then we record p, which happens to be
equal to s^, on top of s=p^, giving us p^:>p. This is a classical
rollback, no more no less. Then we try to merge p^:>p with p^:q and bang!

> That same argument actually applies to the naturalMerge/mergeNoConflicts
> equivalence: commuteConflicting is really there to undo a conflicted merge,

No. It does not undo it, it merely re-constructs the other branch of the
merge.

> so in a normal scenario commuteConflicting (p^;q) should never actually 
> succeed.
> But then why the second commute in the old naturalMerge implementation? An
> abundance of caution, or some case I haven't thought about?

Definitely not an abundance of caution: the first thing I tried was to
remove the extra check and that gave me lots of failing properties. That
was the point at which I /really/ started to think about this.

It would be interesting to see if we can use commute instead of
commuteNoConflicts for mergeNoConflicts with V3 patches, since in V3 we
cannot record the formal inverse of an existing patch (their IDs would
be unrelated), so the above scenario would indeed be impossible there.
In fact, both the camp paper and the camp implementation use the plain
commute here, and not commuteNoConflicts.

Cheers
Ben

__________________________________
Darcs bug tracker <bugs at darcs.net>
<http://bugs.darcs.net/patch1701>
__________________________________


More information about the darcs-devel mailing list