Ord: Reflexivity law is wrong?
Avaliação
- Dificuldade
- 4/5
- Tempo estimado
- 3-5 dias
- Facilidade para iniciantes
- 25/100
- Tipo de issue
- Bug
- Clareza
- Razoavelmente clara
- Status de atividade
- Estagnada
- Domínio
- backend
Direção de pesquisa
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.
Escrita pelo modelo de indexação a partir do texto da issue.
Descrição
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.
- Linguagem predominante
- PureScript
- Estrelas
- 168
- Forks
- 90
- Merge médio
- 3d 1h
- PRs com merge (30d)
- 1
Preparar o ambiente
- Sem Dockerfile nem arquivo Docker Compose
- Tem um modelo de pull request
- Sem guia de contribuição
Primeiros passos
- Leia a issue inteira e depois o guia de contribuição do projeto.
- Comente na issue dizendo que vai assumir — evita que duas pessoas façam o mesmo trabalho.
- Faça um fork do repositório e trabalhe em uma branch.
- Abra um pull request que referencie o número da issue.
Mais de purescript/purescript-prelude
-
Dificuldade 2/5 1-3 horas Facilidade para iniciantes 57/100
purescript/purescript-prelude#317 · 1 reação ·
-
Int bottom is not safeAberta
Dificuldade 3/5 1-2 dias Facilidade para iniciantes 32/100
purescript/purescript-prelude#312 · 5 comentários ·
-
add liftCompare & friendsAberta
Dificuldade 5/5 Mais de uma semana Facilidade para iniciantes 25/100
purescript/purescript-prelude#310 · 5 comentários ·
-
Dificuldade 5/5 Mais de uma semana Facilidade para iniciantes 24/100
purescript/purescript-prelude#308 · 2 comentários ·
-
Dificuldade 3/5 1-2 dias Facilidade para iniciantes 35/100
purescript/purescript-prelude#307 · 1 comentário · 1 reação ·
Todas as issues de purescript/purescript-prelude
Issues semelhantes
-
Dificuldade 2/5 1-3 horas Facilidade para iniciantes 72/100
ROCm/rocm-libraries#15866 ·
Mantenedores costumam responder em até 2 dias
-
お問い合わせのメール送信に失敗しても成功と表示されるAbertaarea: web
Dificuldade 2/5 1-3 horas Facilidade para iniciantes 72/100
inabagumi/shinju-date#6823 ·
Mantenedores costumam responder em até 1 dia
-
Dificuldade 2/5 1-3 horas Facilidade para iniciantes 62/100
-
ManageSieve proxy: a backend's NO/BYE greeting is skipped as a capability line and reported as EOFAbertabug
Dificuldade 2/5 1-3 horas Facilidade para iniciantes 72/100
Mantenedores costumam responder em até 1 dia
-
Dificuldade 1/5 Menos de uma hora Facilidade para iniciantes 82/100
dmtrKovalenko/odiff#191 ·