Ord: Reflexivity law is wrong?
Bewertung
- Schwierigkeit
- 4/5
- Geschätzter Aufwand
- 3-5 Tage
- Anfängerfreundlichkeit
- 25/100
- Issue-Typ
- Bug
- Klarheit
- Größtenteils klar
- Aktivitätsstatus
- Veraltet
- Bereich
- backend
Rechercherichtung
Read the Ord law documentation and the linked issue #174 and pull request #298 for context; pull request #301 is already open for this issue. The proposed change is to state reflexivity as “if a == b then a <= b”; determine whether that law is appropriate for Ord and how the example of unreduced rationals affects it before making a change.
Vom Indexierungsmodell aus dem Issue-Text verfasst.
Beschreibung
A while back, after some discussion, we updated the antisymetry law of Ord from:
-- | - Antisymmetry: if `a <= b` and `b <= a` then `a = b`
to
-- | - Antisymmetry: if `a <= b` and `b <= a` then `a == b`
so as to connect Eq and Ord. See issue #174 and PR #298.
Ever since, the reflexivity law has been bugging me and I think we need to update that too. Currently, it reads
-- | - Reflexivity: `a <= a`
and I think it should read
-- | - Reflexivity: if `a == b` then `a <= b`
To explain why, I return to my old example of unreduced rational numbers. Take a rational number represented as a record with two fields (n and d) where d is not zero but without the requirement that n and d are coprime. We can define equality as
eq (Rat x) (Rat y) = x.n * y.d == y.n * x.d
But what if we then define Ord using dictionary order
compare (Rat x) (Rat y) = case compare x.n y.n of
EQ -> compare x.d y.d
neq -> neq
These two definitions satisfy the current laws, specifically Ord is reflexive, but:
> x = Rat {n: 2, d: 4}
> y = Rat {n: 1, d: 2}
> x == y
true
> x <= y
false
which is surely not what we want.
- Vorherrschende Sprache
- PureScript
- Sterne
- 168
- Forks
- 90
- Ø Merge
- 3 T. 1 Std.
- Gemergte PRs (30 T.)
- 1
Entwicklungsumgebung
- Kein Dockerfile und keine Docker-Compose-Datei
- Hat eine Pull-Request-Vorlage
- Kein Beitragsleitfaden
Erste Schritte
- Lesen Sie das ganze Issue und danach den Beitragsleitfaden des Projekts.
- Schreiben Sie ins Issue, dass Sie es übernehmen — das erspart doppelte Arbeit.
- Forken Sie das Repository und arbeiten Sie in einem Branch.
- Öffnen Sie einen Pull Request, der die Issue-Nummer nennt.
Mehr aus purescript/purescript-prelude
-
Schwierigkeit 2/5 1-3 Stunden Anfängerfreundlichkeit 57/100
purescript/purescript-prelude#317 · 1 Reaktion ·
-
Int bottom is not safeOffen
Schwierigkeit 3/5 1-2 Tage Anfängerfreundlichkeit 32/100
purescript/purescript-prelude#312 · 5 Kommentare ·
-
Schwierigkeit 5/5 Über eine Woche Anfängerfreundlichkeit 25/100
purescript/purescript-prelude#310 · 5 Kommentare ·
-
Schwierigkeit 5/5 Über eine Woche Anfängerfreundlichkeit 24/100
purescript/purescript-prelude#308 · 2 Kommentare ·
-
Schwierigkeit 3/5 1-2 Tage Anfängerfreundlichkeit 35/100
purescript/purescript-prelude#307 · 1 Kommentar · 1 Reaktion ·
Alle Issues in purescript/purescript-prelude
Ähnliche Issues
-
Schwierigkeit 2/5 1-3 Stunden Anfängerfreundlichkeit 72/100
ROCm/rocm-libraries#15866 ·
Maintainer antworten meist innerhalb von 2 Tagen
-
area: web
Schwierigkeit 2/5 1-3 Stunden Anfängerfreundlichkeit 72/100
inabagumi/shinju-date#6823 ·
Maintainer antworten meist innerhalb von 1 Tag
-
Schwierigkeit 2/5 1-3 Stunden Anfängerfreundlichkeit 62/100
-
ManageSieve proxy: a backend's NO/BYE greeting is skipped as a capability line and reported as EOFOffenbug
Schwierigkeit 2/5 1-3 Stunden Anfängerfreundlichkeit 72/100
Maintainer antworten meist innerhalb von 1 Tag
-
Schwierigkeit 1/5 Unter einer Stunde Anfängerfreundlichkeit 82/100
dmtrKovalenko/odiff#191 ·