A bunch of refactorings in the Darcs.Patch subsystem.

The most important (non-trivial) refactor is
  * replace naturalMerge with mergeNoConflicts

12 patches for repository http://darcs.net/screened:

patch 2f159567f4cac4c1b8395de7b6f2d1f71d96e442
Author: Ben Franksen <ben.franksen@online.de>
Date:   Fri Feb 16 12:19:52 CET 2018
  * apply hunks for the same file in one go for V2, too
  
  It seems this optimization was never done for RepoPatchV2.

patch 72545e3b3d8c082e195039af0eed119a70bae8a2
Author: Ben Franksen <ben.franksen@online.de>
Date:   Thu Apr 26 09:00:37 CEST 2018
  * rename 'conflictedEffect' to 'isConflicted'
  
  This function (class method) is used to classify patches and has
nothing to
  do with the effect of a patch.

patch 0ce071080b90f467e23a7cbb4f514cdc3e4bcda7
Author: Ben Franksen <ben.franksen@online.de>
Date:   Thu Apr 26 09:12:09 CEST 2018
  * add haddocks for D.P.Conflict.IsConflictedPrim

patch 12839791e8952a09579f1432177ce11965d96542
Author: Ben Franksen <ben.franksen@online.de>
Date:   Thu Apr 26 09:12:55 CEST 2018
  * remove out-commented code line from mangleUnravelledHunks

patch 0210b59079b37ea03a6e837e85a85f9cdb5849d3
Author: Ben Franksen <ben.franksen@online.de>
Date:   Tue May 29 14:55:40 CEST 2018
  * improved haddocks for CommuteNoConflicts

patch 5538a1fc92fa3dd0210dd9261fd9b6ed2ad11847
Author: Ben Franksen <ben.franksen@online.de>
Date:   Tue May 29 15:01:51 CEST 2018
  * refactor the instance Commute RepoPatchV2
  
  To avoid repeated calls to commuteNoConflicts in cases where we know
it will
  fail, add commuteConflicting as a separate top-level function. Also factor
  out invertCommuter which is now used for both commuteConflicting and
  commuteNoConflicts.

patch 86ccfc74c0c04b2d8ef2acca37c17c7367432102
Author: Ben Franksen <ben.franksen@online.de>
Date:   Wed May 30 18:30:32 CEST 2018
  * factor swapMerge from D.P.V2.RepoPatch to D.P.Merge

patch 536b211062f18b42715cd525e2be075897b8df91
Author: Ben Franksen <ben.franksen@online.de>
Date:   Wed May 30 18:31:34 CEST 2018
  * simplify V1 merge by calculating both branches in one go

patch 71853b7f5fac8841c62214ccb15ebc81650dace4
Author: Ben Franksen <ben.franksen@online.de>
Date:   Mon Jun  4 17:48:12 CEST 2018
  * in D.P.V1.Commute, remove commuteNoMerger and replace with
commuteNoConflicts

patch c31ae97d50d3e7b5659ba005d0509c4ea78d1e1b
Author: Ben Franksen <ben.franksen@online.de>
Date:   Thu Jun  7 20:14:32 CEST 2018
  * replace naturalMerge with mergeNoConflicts
  
  This change is a consequence of my improved understanding of what
  commuteNoConflicts is about and how non-conflicting merge should work, see
  the haddocks for details. The new function is also more efficient because
  (a) commuteNoConflicts has to consider fewer cases and (b) we can now drop
  the extra commute check on the result of the merge.

patch 95404fa9c8100ee49d976f2cd203b6a49534d69a
Author: Ben Franksen <ben.franksen@online.de>
Date:   Thu Jun  7 21:51:30 CEST 2018
  * add laws to classes Commute and CommuteNoConflicts

patch ad2600e278e89fb4f0fff9413bc94dbff5379e62
Author: Ben Franksen <ben.franksen@online.de>
Date:   Wed May 16 10:02:35 CEST 2018
  * add _forceCommute to D.P.Merge
  
  The only purpose of this function is to document how the merge operation,
  together with the square commute law, allows to commute any pair of
adjacent
  patches.

Attachments

• apply-hunks-for-the-same-file-in-one-go-for-v2_-too.dpatch

Screening this bundle (all patches basically make sense AFAICS and
successfully test on my machines).

A partial review - I've pushed all the patches below to
reviewed. I'm still thinking about the remaining three.

>  * apply hunks for the same file in one go for V2, too

Fine

>  * rename 'conflictedEffect' to 'isConflicted'

OK - to be honest I don't find either name particularly clear.
'isConflicted' feels a bit strange as it doesn't return a Bool.
'conflictedEffect' seems to reflect the fact that ultimately
the implementation on V1 patches calls 'effect' but I agree it
isn't very helpful. I don't have a better name, anyway.

>  * add haddocks for D.P.Conflict.IsConflictedPrim

Fine

>  * remove out-commented code line from mangleUnravelledHunks

Fine


>  * refactor the instance Commute RepoPatchV2

Fine

>  * factor swapMerge from D.P.V2.RepoPatch to D.P.Merge

Fine

>  * simplify V1 merge by calculating both branches in one go

Either delete the commented out code or add a comment to explain why it's there

>  * in D.P.V1.Commute, remove commuteNoMerger and replace with commuteNoConflicts

Fine


>  * add _forceCommute to D.P.Merge

Fine - is calling commute first just an optimisation, or is it necessary for correctness?

As I mentioned, I'm still thinking about the last few patches in this bundle,
that clarify commuteNoConflicts.

One of the things that's making it harder for me to understand them is the
idea that a conflict is between a *sequential* pair of patches (p:>q).
I've always thought of conflicts as between a *parallel* pair of patches
(p:\/:q).

I know the language you used is somewhat implied by the fact that
commuteNoConflicts is the one that actually has a definition. But do you think
it'd make sense to formulate as something like
"commuteNoConflicts (p:>q) fails when commute (p:>q) succeeds in the case
that (p:>q) results from a conflicted merge"?

Maybe further down the line we could also make mergeNoConflicts be the
primitive operation.

>  * improved haddocks for CommuteNoConflicts

Apart from the definition of 'conflict', this is fine. The new documentation is
a bit ambiguous about what happens with composite patches: the answer is that the
commute fails if any of the individual patch commutes fail.

>  * replace naturalMerge with mergeNoConflicts

I need to keep thinking about the comment associated with this change.

>  * add laws to classes Commute and CommuteNoConflicts

It would be nice if these laws had associated tests.

> +-- * If an instance @'Commute' p@ exists, then

Should we just add Commute as a superclass of CommuteNoConflicts?
Even though it's not necessary for the implementation I don't think it's
useful not to have it.

> One of the things that's making it harder for me to understand them is the
> idea that a conflict is between a *sequential* pair of patches (p:>q).
> I've always thought of conflicts as between a *parallel* pair of patches
> (p:\/:q).

I had the same difficulty at first. It was the reason I started with
this because I did not understand what "commuteNoConflicts" was supposed
to mean.

Of course a conflict first arises between a parallel pair. But then
Darcs comes along and merges them anyway, and the result is a sequential
pair with one of the patches, say p, in its original form, and the other
one in the form of a conflictor. If presented in this form, a sequential
pair can indeed be in conflict. The conflictor even tells us /which/
patches (in its own past) it conflicts with.

> I know the language you used is somewhat implied by the fact that
> commuteNoConflicts is the one that actually has a definition. But do
you think
> it'd make sense to formulate as something like
> "commuteNoConflicts (p:>q) fails when commute (p:>q) succeeds in the case
> that (p:>q) results from a conflicted merge"?

Yes, that is perhaps a better way to express it. What I wanted to
express is what it means for a /sequential/ pair to be in conflict (as
opposed to a parallel pair).

I still think we should clearly state somewhere that a conflict shows up
in two different forms: before the merge as a parallel pair, after merge
as a sequential pair. Creating a conflictor doesn't magically make the
conflict go away, it's still there and needs to be resolved!

> Maybe further down the line we could also make mergeNoConflicts be the
> primitive operation.

Hmm. commuteNoConflicts is used independently from mergeNoConflicts e.g.
as an optimization for resolveConflicts (for V2 conflictors, at least).
I doubt that commuteNoConflicts can be expressed in terms of
mergeNoConflicts. Also, commuteNoConflicts does /not/ mean that it
doesn't handle conflictors: it does, but it succeeds only for cases
where the patches are unrelated i.e. all the ingredients commute
naturally. (BTW, this is much clearer to see in the camp theory: for the
unrelated cases, the conflicts stay where they are, whereas for the
cases resulting form a conflicted merge, conflicts move from one patch
to the other.)

>>  * improved haddocks for CommuteNoConflicts
>
> Apart from the definition of 'conflict', this is fine. The new
documentation is
> a bit ambiguous about what happens with composite patches: the answer
is that the
> commute fails if any of the individual patch commutes fail.

As this works exactly analogous as for commute I did not think of
mentioning it explicitly.

>>  * 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.

>>  * add laws to classes Commute and CommuteNoConflicts
>
> It would be nice if these laws had associated tests.

Definitely.

>> +-- * If an instance @'Commute' p@ exists, then
>
> Should we just add Commute as a superclass of CommuteNoConflicts?
> Even though it's not necessary for the implementation I don't think it's
> useful not to have it.

I don't think a Patch type p with CommuteNoConflicts p but not Commute p
makes much sense, so yes. (I still have a slightly bad feeling about
this but I can't explain why, exactly.)

> Should we just add Commute as a superclass of CommuteNoConflicts?
> Even though it's not necessary for the implementation I don't think it's
> useful not to have it.

I had to think a while about this but now I think you are right. The crux is
that for commuteNoConflicts we require the square-commute law to hold, while
for commute it does not hold in general (only the weaker inverse-commute law
holds up; this is the price we pay for getting a total merge operation). So
saying 'instance CommuteNoConflicts T' is a stronger statement than
'instance Commute T', which means Commute should be a superclass of
CommuteNoConflicts. I was confused by the fact that we use
commuteNoConflicts in the implementation of commute, but this is a common
situation (see e.g. Applicative => Monad). In addition, CommuteNoConflicts
should be a superclass of PrimPatch, so we can use mergeNoConflicts for
them.

4 patches for repository http://darcs.net/screened:

patch 0df21caac925062b51b94d5096038430917a85b8
Author: Ben Franksen <ben.franksen@online.de>
Date:   Sat Sep  8 13:13:36 CEST 2018
  * factor CommuteNoConflicts to its own module
  
  Also improved the documentation for it and for mergeNoConflicts.

patch f24efab271e665cc68f67ff6ccd372f27aad94d4
Author: Ben Franksen <ben.franksen@online.de>
Date:   Sat Sep  8 18:50:01 CEST 2018
  * make CommuteNoConflicts a superclass of PrimPatch
  
  This allows to use mergeNoConflicts for prim patches. An alternative would
  be to scrap CommuteNoConflicts and instead add commuteNoCnflicts to the
  Commute class.

patch 47e841900c023bd58d881aa237670bfba98f8b11
Author: Ben Franksen <ben.franksen@online.de>
Date:   Sat Sep  8 16:32:25 CEST 2018
  * use generic commuter functions to scrap boilerplate

patch ead2bc98b2835e7102a708cdad5f553b4f3d54e1
Author: Ben Franksen <ben.franksen@online.de>
Date:   Wed Sep 12 00:00:05 CEST 2018
  * make Commute a superclass of CommuteNoConflicts

Attachments

• factor-commutenoconflicts-to-its-own-module.dpatch
• patch-preview.txt
• unnamed

Sorry about this, it slipped through a last minute rebase.

1 patch for repository http://darcs.net/screened:

patch b15eeb1ad9dae82ee23402761e76c837ee004e24
Author: Ben Franksen <ben.franksen@online.de>
Date:   Fri Sep 14 23:00:37 CEST 2018
  * fix accidental module name change in import list

Attachments

• fix-accidental-module-name-change-in-import-list.dpatch
• patch-preview.txt
• unnamed

>   * factor CommuteNoConflicts to its own module

Fine

>   * 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.

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.

>   * improved haddocks for CommuteNoConflicts

Fine

>  * 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.

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^.

That same argument actually applies to the naturalMerge/mergeNoConflicts
equivalence: commuteConflicting is really there to undo a conflicted 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?

Also, perhaps we could think about breaking merge up into explicit pieces
mergeNoConflicts and mergeConflicting - presumably some laws should hold
between commuteConflicting and mergeConflicting too.

>> Maybe further down the line we could also make mergeNoConflicts be the
>> primitive operation.

> Hmm. commuteNoConflicts is used independently from mergeNoConflicts e.g.
> as an optimization for resolveConflicts (for V2 conflictors, at least).
> I doubt that commuteNoConflicts can be expressed in terms of
> mergeNoConflicts.

OK, yes, this wouldn't make sense.

> patch f24efab271e665cc68f67ff6ccd372f27aad94d4
> Author: Ben Franksen <ben.franksen@online.de>
> Date:   Sat Sep  8 18:50:01 CEST 2018
>  * make CommuteNoConflicts a superclass of PrimPatch

>   This allows to use mergeNoConflicts for prim patches. An
>   alternative would be to scrap CommuteNoConflicts and instead
>   add commuteNoCnflicts to the Commute class.

I'm a little skeptical of this, as I have this intuitive vision
of Prims as a "pure" world where it doesn't even make sense to
talk about conflicts. Are there significant benefits?

> patch 47e841900c023bd58d881aa237670bfba98f8b11
> Author: Ben Franksen <ben.franksen@online.de>
> Date:   Sat Sep  8 16:32:25 CEST 2018
>   * use generic commuter functions to scrap boilerplate

> patch ead2bc98b2835e7102a708cdad5f553b4f3d54e1
> Author: Ben Franksen <ben.franksen@online.de>
> Date:   Wed Sep 12 00:00:05 CEST 2018
>   * make Commute a superclass of CommuteNoConflicts

Fine.

>>   * 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

>>  * make CommuteNoConflicts a superclass of PrimPatch
> 
>>   This allows to use mergeNoConflicts for prim patches. An
>>   alternative would be to scrap CommuteNoConflicts and instead
>>   add commuteNoCnflicts to the Commute class.
> 
> I'm a little skeptical of this, as I have this intuitive vision
> of Prims as a "pure" world where it doesn't even make sense to
> talk about conflicts.

Oh, it makes lots of sense to talk about conflicting prims. I guess what
you meant to say is that it does not make sense to talk about
/commuting/ conflicting prims, and I'd agree with that. But that is
exactly the point, see the longer explanation below.

BTW, this should be reviewed together with:

patch ead2bc98b2835e7102a708cdad5f553b4f3d54e1
Author: Ben Franksen <ben.franksen@online.de>
Date:   Wed Sep 12 00:00:05 CEST 2018
  * make Commute a superclass of CommuteNoConflicts

> Are there significant benefits?
Not really, no. And I won't insist on it. Anyway, here is my rationale:

I was thinking of how these two classes relate to each other and to prim
patches versus generalized patches (=prim patches + conflictors).

Ignore the names for a moment and concentrate on what exactly is
different, formally, in the specification of Commute versus
CommuteNoConflicts. You'll find that the *only* difference is that
CommuteNoConflicts is more demanding: it requires the square commute law
to hold, whereas Commute requires only the weaker inverse commute law.

This means that, as you suggested before, Commute should be a superclass
of CommuteNoConflicts: if you can define a law abiding instance of
CommuteNoConflicts, then you certainly can define the weaker instance
for Commute (just define commute = commuteNoConflicts). (This is really
the same situation as with Applicative being a superclass of Monad.)

Now what about prim patches? Well, their commute really satisfies the
square commute law, so, from a logical point of view they should have an
instance of CommuteNoConflicts to express that. Indeed a sequential pair
of prim patches cannot be in conflict, so commuteNoConflicts necessarily
coincides with commute.

The reason we need the more general Commute class at all is *only*
because of Merge, which requires that both branches of a merge commute
to each other. We (have to) weaken the requirements for Commute
(realtive to CommuteNoConflicts) precisely so that we can state the
merge commute law.

In this sense, the difference between CommuteNoConflicts and Commute
precisely captures, in an abstract way, the difference in behavior
between commute for prim patches and commute for generalized patches.

Cheers, Ben

One more remark. You observed that for generalized patches we define

  commute = commuteNoConflicts + commuteConflicting

(where the '+' is `mplus` lifted to functions).

Again, this serves to illustrate my point: the addition of
commuteConflicting allows more commutes to succeed. We do that in order
to fulfill the promise we made when we defined the Merge instance: the
cases commuteConflicting handles are exactly those required for the
merge commute law to hold. (And the price is that this invalidates the
square commute law.)

Using the new -XDefaultSignatures extension (and perhaps a few minor
refactorings) we could make this explicit by adding

  class CommuteConflicting p where
    commuteConflicting :: (p :> p) wX wY -> Maybe ((p :> p) wX wY)

and then define Commute as

  class Commute p where
    commute :: (p :> p) wX wY -> Maybe ((p :> p) wX wY)
    default commute :: (CommuteNoConflicts p, CommuteConflicting p) =>
      (p :> p) wX wY -> Maybe ((p :> p) wX wY)
    commute ps = commuteNoConflicts ps `mplus` commuteConflicting ps

For prim patches we could then add a trivial

  instance CommuteConflicting Prim where
    commuteConflicting _ = mzero

We could even add this definition of commuteConflicting as a default
implementation to the class, reducing these instances to

  instance CommuteConflicting Prim

Cheers, Ben

>> 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.

FWIW I meant "undo" loosely: it's the operation darcs would do
if you first pulled a conflicting patch then unpulled the
local patch.


>> 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!

Thanks, I hadn't thought about rollbacks. So now I agree with the
statement that the scenario is possible and that mergeNoConflicts
needs to fail when it happens.

Restating it with different naming to clarify it in my own head,
if we start with primitive patches x and y which conflict,
and give them aliases x[1] and x[2] to reflect a real scenario
where they appear as original+rollback in different
named patches, then we have the following picture if the merge
was allowed to succeed:

   x[1]'   x[2]'^
  ------> ------>
 ^       ^        ^
 |       |        |
y|     y'|       y|
 |       |        |
  ------> ------>
   x[1]    x[2]^


So if we use commute for the second merge instead
of commuteNoConflicts, we can essentially undo a conflicted
merge by merging with the rollback, which isn't how darcs works
at the moment.

However, I'm stil struggling a bit with the definition of
"conflict" that justifies this formally: I understand that
since x :\/: y is a conflicting merge, that x :> y' would be
a conflicting commute. How does that give us that x^ :\/: y'
must be a conflicting merge? Do we just have to include it in
the axioms of "conflict", or is it a consequence of the square
commute law somehow?

Regardless of this confusion, I'll mark this patch as reviewed
now as I'm reasonably convinced of its correctness: it's
particularly reassuring that there were tests that showed why
the second commute was required in naturalMerge and that
those tests still pass with mergeNoConflicts.

Am 01.10.2018 um 19:22 schrieb Ganesh Sittampalam:
> Ganesh Sittampalam <ganesh@earth.li> added the comment:
>>> 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.
> 
> FWIW I meant "undo" loosely: it's the operation darcs would do
> if you first pulled a conflicting patch then unpulled the
> local patch.

Ah, okay. Yes in this sense it's undoing something. Though it really
just shifts the conflict to the other patch.

> Restating it with different naming to clarify it in my own head,
> if we start with primitive patches x and y which conflict,
> and give them aliases x[1] and x[2] to reflect a real scenario
> where they appear as original+rollback in different
> named patches, then we have the following picture if the merge
> was allowed to succeed:
> 
>    x[1]'   x[2]'^
>   ------> ------>
>  ^       ^        ^
>  |       |        |
> y|     y'|       y|
>  |       |        |
>   ------> ------>
>    x[1]    x[2]^
> 
> 
> So if we use commute for the second merge instead
> of commuteNoConflicts, we can essentially undo a conflicted
> merge by merging with the rollback, which isn't how darcs works
> at the moment.

Yes, that's exactly how I see it.

> However, I'm stil struggling a bit with the definition of
> "conflict" that justifies this formally: I understand that
> since x :\/: y is a conflicting merge, that x :> y' would be
> a conflicting commute. How does that give us that x^ :\/: y'
> must be a conflicting merge? Do we just have to include it in
> the axioms of "conflict", or is it a consequence of the square
> commute law somehow?

The latter. Let me give a precise definition of "conflict":

  x :\/: y conflict if and only if commuteNoConflicts x^ :\/: y fails.

Your question was: why must x^ :\/: y' be conflicting? Well by the above
definition, if they would not conflict, then commuteNoConflicts (x :>
y') would have to succeed. But we require that commute and
commuteNoConflicts are compatible, that is, their results (on success)
must coincide. So commuteNoConflicts (x :> y') = Just (y :> x'). But now
the square commute law (which we require to hold for commuteNoConflicts)
gives us that commuteNoConflicts x^ :\/: y would /also/ succeed in
contradiction to the assumption that x and y are in conflict. QED.

Cheers
Ben

[should prim patches implement CommuteNoConflicts]

> Now what about prim patches? Well, their commute really satisfies
> the square commute law, so, from a logical point of view they
> should have an instance of CommuteNoConflicts to express that.
> Indeed a sequential pair of prim patches cannot be in conflict,
> so commuteNoConflicts necessarily coincides with commute.

> The reason we need the more general Commute class at all is *only*
> because of Merge, which requires that both branches of a merge 
> commute to each other. We (have to) weaken the requirements for
> Commute (realtive to CommuteNoConflicts) precisely so that we can 
> state the merge commute law.

> In this sense, the difference between CommuteNoConflicts
> and Commute precisely captures, in an abstract way, the
> difference in behavior between commute for prim patches
> and commute for generalized patches.

Right. I think you've uncovered an important part of the "theory" of
darcs here (at least, I wasn't previously aware of it in these 
terms).

I'm less sure about encoding that in the code in its present form.

Our code does use Commute extensively - even Eq2 for lists relies
on it - whereas commuteNoConflicts is in practice only used in the
internals of specific merge implementations, and for marking 
conflicts. You mentioned mergeNoConflicts in the patch comments but 
I don't see any actual uses of it outside the merge implementations.

I worry about making the code harder to work on by introducing
ambiguity between the two different commutes. Perhaps we should
actually be using commuteNoConflicts more widely, but I don't have
an intuition about where.

I won't push further to drop this, but if you do keep it perhaps
you could add a doc comment to the commuteNoConflicts member itself,
explaining when it should be used? That would complement the
existing nice docs on the class itself that explain how to implement
it.

On 02/10/2018 21:42, Ben Franksen wrote:

> Am 01.10.2018 um 19:22 schrieb Ganesh Sittampalam: 

>> However, I'm stil struggling a bit with the definition of
>> "conflict" that justifies this formally: I understand that
>> since x :\/: y is a conflicting merge, that x :> y' would be
>> a conflicting commute. How does that give us that x^ :\/: y'
>> must be a conflicting merge? Do we just have to include it in
>> the axioms of "conflict", or is it a consequence of the square
>> commute law somehow?
> 
> The latter. Let me give a precise definition of "conflict":
> 
>   x :\/: y conflict if and only if commuteNoConflicts x^ :\/: y fails.
> 
> Your question was: why must x^ :\/: y' be conflicting? Well by the above
> definition, if they would not conflict, then commuteNoConflicts (x :>
> y') would have to succeed. But we require that commute and
> commuteNoConflicts are compatible, that is, their results (on success)
> must coincide. So commuteNoConflicts (x :> y') = Just (y :> x'). But now
> the square commute law (which we require to hold for commuteNoConflicts)
> gives us that commuteNoConflicts x^ :\/: y would /also/ succeed in
> contradiction to the assumption that x and y are in conflict. QED.

Thanks, it's all very simple now you put it that way :-)

Ganesh

Marking this as fully reviewed (finally!) - as discussed in an email 
which didn't make it to the tracker, you'll write a doc comment for the 
commuteNoConflicts member.

Final follow-up for commuteNoConflicts refactor.

1 patch for repository http://darcs.net/screened:

patch eb0082a601e22a4d3395515cd299d8fc64417571
Author: Ben Franksen <ben.franksen@online.de>
Date:   Tue Oct 16 09:53:18 CEST 2018
  * add doc comment to commuteNoConflicts member

Attachments

• add-doc-comment-to-commutenoconflicts-member.dpatch
• patch-preview.txt
• unnamed