Ord: Reflexivity law is wrong?
評価
- 難易度
- 4/5
- 見積もり時間
- 3〜5日
- 初心者へのやさしさ
- 25/100
- issue の種類
- バグ
- 明瞭さ
- おおむね明確
- 活発さ
- 停滞
- 領域
- backend
調査の方向性
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.
索引モデルが issue の本文から書いたものです。
説明
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.
- 主要言語
- PureScript
- スター
- 168
- フォーク
- 90
- 平均マージ
- 3日 1時間
- マージ済み PR（30日）
- 1
環境構築
- Dockerfile・Docker Compose ファイルなし
- プルリクエストのテンプレートあり
- コントリビューションガイドなし
はじめの一歩
- issue を最後まで読み、次にプロジェクトのコントリビューションガイドを読みます。
- 着手することを issue にコメントします — 二人が同じ作業をするのを防げます。
- リポジトリをフォークし、ブランチを切って変更します。
- issue 番号を参照したプルリクエストを送ります。
purescript/purescript-prelude のほかの issue
-
難易度 2/5 1〜3時間 初心者へのやさしさ 57/100
purescript/purescript-prelude#317 · リアクション 1 件 ·
-
難易度 3/5 1〜2日 初心者へのやさしさ 32/100
purescript/purescript-prelude#312 · コメント 5 件 ·
-
難易度 5/5 1週間以上 初心者へのやさしさ 25/100
purescript/purescript-prelude#310 · コメント 5 件 ·
-
難易度 5/5 1週間以上 初心者へのやさしさ 24/100
purescript/purescript-prelude#308 · コメント 2 件 ·
-
難易度 3/5 1〜2日 初心者へのやさしさ 35/100
purescript/purescript-prelude#307 · コメント 1 件 · リアクション 1 件 ·
purescript/purescript-prelude の issue をすべて見る
似ている issue
-
難易度 2/5 1〜3時間 初心者へのやさしさ 62/100
-
ManageSieve proxy: a backend's NO/BYE greeting is skipped as a capability line and reported as EOFオープンbug
難易度 2/5 1〜3時間 初心者へのやさしさ 72/100
メンテナーはふだん 1 日以内に返信
-
Mend: dependency security vulnerability
難易度 2/5 1〜3時間 初心者へのやさしさ 65/100
-
Mend: dependency security vulnerability
難易度 2/5 1〜3時間 初心者へのやさしさ 62/100
ManageIQ/manageiq-pods#1476 ·
メンテナーはふだん 1 日以内に返信
-
難易度 2/5 1〜3時間 初心者へのやさしさ 62/100
prime-radiant-inc/evener#6366 ·
メンテナーはふだん 1 日以内に返信