Ord: Reflexivity law is wrong?

Aperta
  • Qualcosa non va?
#300 1 commento 0 reazioni 0 assegnatari Vedi su GitHub

@JamieBallingall ci sta già lavorando.

Dal 18/10/2022.

  • #301 di @JamieBallingall — aperta

Valutazione

Difficoltà
4/5
Tempo stimato
3-5 giorni
Idoneità per principianti
25/100
Tipo di issue
Bug
Chiarezza
Abbastanza chiara
Stato di attività
Ferma
Ambito
backend

Direzione di ricerca

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.

Scritto dal modello di indicizzazione a partire dal testo della issue.

Descrizione

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.

Lingua principale
PureScript
Stelle
168
Fork
90
Merge medio
3g 1h
PR unite (30g)
1

Preparare l'ambiente

  • Nessun Dockerfile né file Docker Compose
  • Ha un modello di pull request
  • Nessuna guida per i contributori

Come iniziare

  1. Leggi tutta la issue e poi la guida ai contributi del progetto.
  2. Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
  3. Fai un fork del repository e lavora su un branch.
  4. Apri una pull request che faccia riferimento al numero della issue.

Altre issue di purescript/purescript-prelude

Tutte le issue di purescript/purescript-prelude

Issue simili

Altre issue su Backend & API Design

Ricevi le nuove issue nella tua casella

Un breve riepilogo di issue GitHub adatte ai principianti.