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
falsewhich is surely not what we want.
A while back, after some discussion, we updated the antisymetry law of
Ordfrom:-- | - 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
EqandOrd. 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 (
nandd) wheredis not zero but without the requirement thatnanddare coprime. We can define equality asBut what if we then define
Ordusing dictionary orderThese two definitions satisfy the current laws, specifically
Ordis reflexive, but:which is surely not what we want.