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 小时
- 30 天内合并 PR
- 1
环境准备
- 没有 Dockerfile 或 Docker Compose 文件
- 有 Pull Request 模板
- 没有贡献指南
从这里开始
- 先读完整个 Issue，再读项目的贡献指南。
- 在 Issue 下留言说明你要接手 —— 这能避免两个人做同样的事。
- Fork 仓库，在一个分支上完成修改。
- 提交 Pull Request，并在描述里引用这个 Issue 编号。
purescript/purescript-prelude 的其他 Issue
-
难度 2/5 1-3 小时 新手友好度 57/100
purescript/purescript-prelude#317 · 1 个 reaction ·
-
难度 3/5 1-2 天 新手友好度 32/100
purescript/purescript-prelude#312 · 5 条评论 ·
-
难度 5/5 一周以上 新手友好度 25/100
purescript/purescript-prelude#310 · 5 条评论 ·
-
难度 5/5 一周以上 新手友好度 24/100
purescript/purescript-prelude#308 · 2 条评论 ·
-
难度 3/5 1-2 天 新手友好度 35/100
purescript/purescript-prelude#307 · 1 条评论 · 1 个 reaction ·
查看 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 天内回复