This fixes long standing misgivings about nominal versus semantic equality
in Darcs.

I know I have defended the Eq2 instances for FL/RL in the past. So it may
come as a (happy) surprise to you (Ganesh) that I have changed my mind. See
the patch descriptions for details.

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

patch c84bf9af618b14d6abb5bc73a69f1ccc00b0c6e0
Author: Ben Franksen <ben.franksen@online.de>
Date:   Sun Jun 19 11:45:31 CEST 2022
  * get rid of class IdEq2 by defining PatchId for sequences as Sets

  The former class methods are now regular overloaded operators. This patch
  also simplifies and clarifies the laws associated with Ident and related
  classes. The main point is that nominal equality is supposed to coincide
  with the equivalence relation that identifies patch sequences up to
  commutation. For sequences (:>, FL, RL, PatchSet) this is precisely captured
  by using the set of patch names as the identity.

patch 800c07c43dd93c42a54040620f0e7a2b22a2f187
Author: Ben Franksen <ben.franksen@online.de>
Date:   Sun Jun 19 12:02:05 CEST 2022
  * re-format export list of Darcs.Patch.Permutations

patch 9465d1977eb97e9d3b958023b82b69c6bb45ef1c
Author: Ben Franksen <ben.franksen@online.de>
Date:   Fri Aug 27 10:13:17 CEST 2021
  * reformat code for instances Eq2 FL/RL

patch 5d382c8eb0ac99ff382bd2b7df83f104931d3ff2
Author: Ben Franksen <ben.franksen@online.de>
Date:   Thu Jun 16 16:26:44 CEST 2022
  * fix Eq2 instances for Named and PatchInfoAnd

  It is tempting to define the Eq2 instances for Named and PatchInfoAnd by
  reducing them to nominal equality (for efficiency and simplicity) because
  the types of =\/= and =/\= suggest that we can assume coinciding start or
  end states, which in turn allows us to conclude that equality must hold.
  (Never mind that the code didn't even define =\/= but rather unsafeCompare;
  it makes no difference in practice.)

  This is problematic for two reasons. First, the default implementation of
  unsafeCoerce in terms of =/\= indicates that implementations should /not/
  rely on assumptions about context. Indeed, doing so for named patches
  reduces unsafeCompare to general nominal equality regardless of context,
  which is a much weaker concept than intended. Second, even if we disregard
  unsafeCompare as not meaningful in general, defining Eq2 in this way makes
  the laws governing the relation between semantic and nominal equality
  trivial i.e. true by definition, which in turn makes it pointless to test
  them.

  For PatchInfoAnd, this change means that testing for equality becomes
  partial: it is defined only if both sides have hashes, or else if both sides
  have Available patch content; otherwise it is undefined and we call error.

patch 95daebf5467bf1c8c96b1d8efda33fd9df17978b
Author: Ben Franksen <ben.franksen@online.de>
Date:   Fri Jun 17 11:06:36 CEST 2022
  * fix the generic instance Eq2 for FL/RL

  This changes the semantics of =\/= and =/\= to compare patches one-by-one
  without reordering. New operators =\~/= and =/~\= are introduced for the
  coarser equivalence that ignores differences in patch ordering. These are
  only needed internally in the implementation of RepoPatchV2 and for testing.
  The functions eqFL and eqFLUnsafe are no longer needed, their uses (in the
  test suite) are replaced with =\/= and unsafeCompare, respectively.

  Rationale: Treating sequences that differ only in the ordering of patches as
  equal is wrong, because the order of patches in Darcs *is* observable;
  indeed it must be observable, else 'commute' could be replaced with 'id' and
  all patch properties become vacuously true.

Attachments

• get-rid-of-class-ideq2-by-defining-patchid-for-sequences-as-sets.dpatch
• patch-preview.txt

More incremental reviewing, apologies if it makes the review less
coherent but it's the only way I can keep the progress if I don't
come back soon.

> prop> 'commute' (p :> _) == 'Just' (_ :> p') <=> 'ident' p == 'ident' p'

I get what you're trying to say with the reverse implication, but
I struggle with the formal meaning, particularly given the `_`s
on the left.

Maybe it's something like

prop> (\exists q q' . 'commute' (p :> q) == 'Just' (q' :> p')) <=> 'ident' p == 'ident' p'

?

But also q might need to be a list of whatever patch type p is, rather
than being the same type.

It's actually quite a powerful statement about patch identity being
a global property, and it's great that it's being written down formally.

> prop> 'unsafeCompare' p q => ('ident' p == 'ident' q)

> However, if the patches have a common context, then semantic and nominal
> equality should coincide:

> prop> p '=\/=' q  <=> p '=\^/=' q
> prop> p '=/\=' q  <=> p '=/^\=' q

I found the shift from ident p == ident q to p =\^/= q etc a bit jarring,
until I thought about it more carefully and realised it's to do with
witnesses. Just noting it, I don't have any specific suggestions to
change it.

Shouldn't these properties use `=\~/=` etc, given that identities of
sequences are sets?

Very good points!

Your version of the first law using an existential quantifier (I would 
restrict this to the backward implication) exactly captures what I wanted to 
express. And yes, q needs to be a sequence in that formulation.

> > prop> p '=\/=' q  <=> p '=\^/=' q
> > prop> p '=/\=' q  <=> p '=/^\=' q
> [...]
> Shouldn't these properties use `=\~/=` etc, given that identities
> of sequences are sets?

Again, you are right about that... which briefly made me wonder whether 
choosing sets for the identity of sequences was the right decision. But then,  
looking at how we use them (in findCommonFL, findCommonRL, and to compare the 
effects of V3 conflictors) confirms that this is the definition we need in 
practice. On the technical side, =\~/= and =/~\= are currently only defined 
for FLs because I didn't want to add yet another type class for "patch 
equality up to internal re-ordering", not to speak of finding a suitable name 
for such a class ;-). I guess it is okay to ignore this (implementation) 
detail in the law, as it should be obvious how to generalize these operators.

I will follow up with appropriate fixes.

> Your version of the first law using an existential quantifier
> (I would restrict this to the backward implication)

Yeah, it's certainly uglier for the forward implication, but on the
other hand a two-way law is perhaps easier to read and reason with.

I actually realised after posting my comment that the previous docs did 
roughly express this too, though I think the existential makes things a
bit more concise.

> which briefly made me wonder whether choosing sets for the identity
> of sequences was the right decision.

I'm still mulling over the general topic. One thing I'm not totally
happy with is that the identity (and commute-based equality) on
`FL (FL p)` etc is dependent on the partitioning. Maybe that's
inevitable/natural? I'm not sure.

I was also vaguely wondering if we can better express the "You may
commute this" concept via wrapper types instead of new classes/operators.
Again just random ideas at this point.

> One thing I'm not totally happy with is that the identity (and
> commute-based equality) on `FL (FL p)` etc is dependent on the
> partitioning. Maybe that's inevitable/natural? I'm not sure.

I was thinking about this, too. One idea I came up with was to 
always make ident return a Set of PatchIds, and then define PatchId 
(FL p) = PatchId p and use Set.unions for sequences. The main 
disadvantage is that when we want/expect a single PatchId we need an 
extra case distinction, sometimes with an error case.

Follow-up on review

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

patch 2174487b757e60e69b08ace86aadbf4af5d9018d
Author: Ben Franksen <ben.franksen@online.de>
Date:   Mon Jun 26 10:33:28 CEST 2023
  * make the laws for class Ident more precise

Attachments

• make-the-laws-for-class-ident-more-precise.dpatch
• patch-preview.txt

>  * get rid of class IdEq2 by defining PatchId for sequences as Sets
>  * make the laws for class Ident more precise

Both together fine.

>  * re-format export list of Darcs.Patch.Permutations
>  * reformat code for instances Eq2 FL/RL

Both fine.

>   * fix Eq2 instances for Named and PatchInfoAnd

Looks good. Since Eq2 PatchInfoAnd is not used at all,
and Eq2 Named is used only in the test harness, I wonder
if we should just remove them/move to the harness?

> +instance (Commute p, Eq2 p) => Eq2 (Named p) where

I guess the Commute constraint can be removed again after the
subsequent patch for Eq2 FL.

> New operators =\~/= and =/~\= are introduced for the coarser
> equivalence that ignores differences in patch ordering.
> These are only needed internally in the implementation of
> RepoPatchV2 and for testing.

I tried removing the FL/RL instances and got errors from
all of V1/V2/V3 - I see that you've actually updated
both V2 and V3 but not V1. Does that need updating too?

The code in V1 is in unravel which I think is for conflict
marking only, but I always get a bit confused by that code.

I can reproduce your observations. It seems I was a bit sloppy when I 
checked where instance Eq2 FL are used. V3 is fine, but it seems I 
overlooked that both V1 and V2 complain about

 • Could not deduce (Eq2 (FL prim)) arising from a use of ‘nub’

This affects conflict markup. They are now using the new instance based 
on patch-by-patch comparison with no reordering. In the worst case this 
can cause duplicated alternatives when conflicts are marked.

Fixing this means to not use 'nub' but a specialized implementation 
'nubFL' based on =\~/=. Even though I can't remember observing 
duplicated alternatives with V2, and it doesn't trigger any test 
failures, I think we are safer off with such a fix. Will follow up.

>> +instance (Commute p, Eq2 p) => Eq2 (Named p) where
>
> I guess the Commute constraint can be removed again after the
> subsequent patch for Eq2 FL.

Yes. Could I ask you to ignore this for the moment? I have a patch 
(not yet sent because of dependencies) to systematically remove all 
redundant constraints and also add -Wredundant-constraints (with a 
few exceptions) and would like to avoid yet another round of 
rebasing if possible.

Following up as promised.

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

patch b69e074264e5475a056ba0dac8ad3fd9dcbdc853
Author: Ben Franksen <ben.franksen@online.de>
Date:   Wed Jul 12 13:01:16 CEST 2023
  * fix: use order-independent equality when eliminating duplicate alternatives

  This concerns conflict markup for RepoPatchV1 and RepoPatchV2. In

  patch 95daebf5467bf1c8c96b1d8efda33fd9df17978b
  Author: Ben Franksen <ben.franksen@online.de>
  Date:   Fri Jun 17 11:06:36 CEST 2022
    * fix the generic instance Eq2 for FL/RL

  I failed to notice that the former 'instance Eq2 (FL p)' also gives rise to
  an 'instance Eq (Sealed FL wX)', which was used indirectly via 'nub'. This
  is now replaced with a new function 'nubFL' based on =\~/=.

Attachments

• fix_-use-order_independent-equality-when-eliminating-duplicate-alternatives.dpatch
• patch-preview.txt

I think I found one more instance in Darcs.UI.Commands.Convert.Darcs2
in the helper function convertOne - it wasn't visible before because
it depends on the V1 unravel code.

> Yes. Could I ask you to ignore this for the moment? I have a patch
> (not yet sent because of dependencies) to systematically remove all
> redundant constraints and also add -Wredundant-constraints (with a
> few exceptions) and would like to avoid yet another round of
> rebasing if possible.

No problem - for what it's worth I sometimes find it easier to manage 
this kind of transition with one patch that introduces the new
warning globally but turns it off file-by-file, and then separate 
patches that clean up individual instances.

Well spotted.

I made sure this time that there are no more uses of the instance in darcs
proper, except for Named patches where we actually want the new instance.

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

patch d95f444fe9fd74a09e2a151ab400e8c3a2409969
Author: Ben Franksen <ben.franksen@online.de>
Date:   Wed Jul 12 15:35:36 CEST 2023
  * fix: use order-independent equality in darcs-2 conversion

  Again, this restores behavior to what it was before

    patch 95daebf5467bf1c8c96b1d8efda33fd9df17978b
      * fix the generic instance Eq2 for FL/RL

Attachments

• fix_-use-order_independent-equality-in-darcs_2-conversion.dpatch
• patch-preview.txt

> Since Eq2 PatchInfoAnd is not used at all,
> and Eq2 Named is used only in the test harness, I wonder
> if we should just remove them/move to the harness?

I have some plans that may require these instances, so I would prefer to 
keep them for now. Also, orphan instances; admittedly not a real problem 
for the test suite but still.

Looks good, thanks!