Patch 2266 get rid of class IdEq2 by defining Patch... (and 4 more)

Title get rid of class IdEq2 by defining Patch... (and 4 more)
Superseder Nosy List bf
Related Issues
Status needs-review Assigned To

Created on 2022-11-19.10:07:53 by bf, last changed 2022-11-19.10:09:19 by bf.

File name Status Uploaded Type Edit Remove
get-rid-of-class-ideq2-by-defining-patchid-for-sequences-as-sets.dpatch bf, 2022-11-19.10:07:45 application/x-darcs-patch
patch-preview.txt bf, 2022-11-19.10:07:45 text/x-darcs-patch
See mailing list archives for discussion on individual patches.
msg23042 (view) Author: bf Date: 2022-11-19.10:07:45
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

  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.
Date User Action Args
2022-11-19 10:07:53bfcreate
2022-11-19 10:09:19bfsetstatus: needs-screening -> needs-review