Ord: Reflexivity law is wrong?
Évaluation
- Difficulté
- 4/5
- Temps estimé
- 3-5 jours
- Accessibilité débutants
- 25/100
- Type d'issue
- Bug
- Clarté
- Plutôt claire
- Activité
- À l'abandon
- Domaine
- backend
Piste de recherche
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.
Rédigé par le modèle d'indexation à partir du texte de l'issue.
Description
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.
- Langage dominant
- PureScript
- Étoiles
- 168
- Forks
- 90
- Merge moyen
- 3 j 1 h
- PR mergées (30 j)
- 1
Préparer son environnement
- Aucun Dockerfile ni fichier Docker Compose
- Propose un modèle de pull request
- Aucun guide de contribution
Par où commencer
- Lisez l'issue en entier, puis le guide de contribution du projet.
- Signalez en commentaire que vous la prenez — cela évite que deux personnes fassent le même travail.
- Forkez le dépôt et travaillez sur une branche.
- Ouvrez une pull request qui référence le numéro de l'issue.
Autres issues de purescript/purescript-prelude
-
Difficulté 2/5 1-3 heures Accessibilité débutants 57/100
purescript/purescript-prelude#317 · 1 réaction ·
-
Int bottom is not safeOuverte
Difficulté 3/5 1-2 jours Accessibilité débutants 32/100
purescript/purescript-prelude#312 · 5 commentaires ·
-
add liftCompare & friendsOuverte
Difficulté 5/5 Plus d'une semaine Accessibilité débutants 25/100
purescript/purescript-prelude#310 · 5 commentaires ·
-
Difficulté 5/5 Plus d'une semaine Accessibilité débutants 24/100
purescript/purescript-prelude#308 · 2 commentaires ·
-
Difficulté 3/5 1-2 jours Accessibilité débutants 35/100
purescript/purescript-prelude#307 · 1 commentaire · 1 réaction ·
Toutes les issues de purescript/purescript-prelude
Issues similaires
-
Difficulté 2/5 1-3 heures Accessibilité débutants 62/100
-
ManageSieve proxy: a backend's NO/BYE greeting is skipped as a capability line and reported as EOFOuvertebug
Difficulté 2/5 1-3 heures Accessibilité débutants 72/100
Les mainteneurs répondent en général sous 1 jour
-
Mend: dependency security vulnerability
Difficulté 2/5 1-3 heures Accessibilité débutants 65/100
-
Mend: dependency security vulnerability
Difficulté 2/5 1-3 heures Accessibilité débutants 62/100
ManageIQ/manageiq-pods#1476 ·
Les mainteneurs répondent en général sous 1 jour
-
Difficulté 2/5 1-3 heures Accessibilité débutants 62/100
prime-radiant-inc/evener#6366 ·
Les mainteneurs répondent en général sous 1 jour