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
|
