Clarify relationship between Eq and Ord

[Thimoteus]

Currently the docs say:

-- | The `Ord` type class represents types which support comparisons with a
-- | _total order_.
-- |
-- | `Ord` instances should satisfy the laws of total orderings:
-- |
-- | - Reflexivity: `a <= a`
-- | - Antisymmetry: if `a <= b` and `b <= a` then `a = b`
-- | - Transitivity: if `a <= b` and `b <= c` then `a <= c`
class Eq a <= Ord a where
  compare :: a -> a -> Ordering

Eq is required, but there's nothing else that says why or how Ord and Eq are related.

[garyb]

You don't think it's kinda implied by the use of equals/less-than-or-equals in the laws?

I suppose they don't have to be related, strictly speaking, it's more that every Ord has an "obvious" sensible Eq, but not every Eq can be Ord, probably.

[Thimoteus]

No, because a == b does not imply a = b, and <=, >= are shorthand for Ord-only functions.

Maybe you could argue that the EQ data constructor implies something, but this is really more coincidence than anything.

[hdgarrood]

Would it make sense to replace = with == in the antisymmetry law? Would we lose anything by doing that?

[Thimoteus]

I think it just turns it from a total order on your type to a total order on equivalence classes on your type.

[hdgarrood]

I guess what I'm saying is, does it ever make sense for the Ord instance to be able to distinguish values for which == says they're the same? I'd imagine not; at least, I'm not able to think of an example.

[Thimoteus]

I can't think of one either.

[JordanMartinez]

I'm not sure what the next action is for this issue.

[JamieBallingall]

I think a good next step would be to take @hdgarrood 's suggestion and simply change "=" to "==" in the laws.

@hdgarrood says "does it ever make sense for the Ord instance to be able to distinguish values for which == says they're the same? I'd imagine not; at least, I'm not able to think of an example."

I think we can ask a stronger question: "does it make sense to force the Ord instance to distinguish values for which == says they're the same?". The current anti-symmetry law, as written, forces Ord to do just that. Any Ord instance creates a concept of equality (when a <= b and b <= a) and the currently law says that concept must coincide with = and not with the more flexibly defined ==.

There are various types one might want to define with both an non-trivial Eq instance and an Ord instance, but let's use rational numbers as an example. The current Rational library reduces every rational number to canonical form (where the numerator and denominator are coprime and the denominator is positive). That allows a simple Eq instance and a law abiding Ord instance. But suppose we want to define rationals only as a pair of numbers with the denominator being non-zero.

We can write an Eq instance as eq (Rational n1 d1) (Rational n2 d2) = n1 * d2 == n2 * d1. But an Ord instance that satisfies if a <= b and b <= a then a = b would be out of reach whereas one that satisfies if a <= b and b <= a then a == b would be straightforward.

In some ways this feels like a very minor change to a comment. But it would be good to clear up and I don't see any argument in favor of the status quo. And, for once, it wouldn't be a breaking change.

Any objections?

(To add a note of caution to an otherwise strident comment, I'm assuming here that a = b means that a and b are representationally identical. In the repl I can only assert equality this way, not test it. That is, x = 1 means "henceforth the symbol x evaluates to 1". If there is an argument for keeping the current law then we ought to, at least, clarify what ... then a = b actually means).

[JordanMartinez]

For what it's worth, the corresponding quickcheck-laws test assumes a = b means a == b: https://github.com/purescript-contrib/purescript-quickcheck-laws/blob/main/src/Test/QuickCheck/Laws/Data/Ord.purs#L45

I don't have any objections to this because I can't think of an example against it either. That being said, if a <= && b <= a means a == b, then one could define a eqDefault function similar to foldlDefault:

eqDefault :: forall a. Ord a => a -> a -> Boolean
eqDefault l r = l <= r && r <= l

That being said, would there be any problems with the below code, where the Ord instance is derived but not the Eq? Or does that produce a compiler error?

data SomeType = ...

instance Eq SomeType where
   eq = eqDefault
derive instance Ord SomeType

[JamieBallingall]

Empirically, that seems to work, although I'm not completely sure of the details.

One could also just define:

eqDefault :: forall a. Ord a => a -> a -> Boolean
eqDefault l r = compare l r == EQ

This prompts the question: what do the laws of Ord look like when stated in terms of compare? This something I might noodle on but I don't think we need to keep this issue open for that. Let's get this closed.

PR incoming.

[JordanMartinez]

Just a thought but this implementation

eqDefault :: forall a. Ord a => a -> a -> Boolean
eqDefault l r = compare l r == EQ

would reject cases where l < r == true and r < l == true whereas the implementation I proposed based on the laws as described would accept it. I don't think that matters in practice (when would l < r && r < l ever be true?), but I did want to point that out.

[JamieBallingall]

I think l < r && r < l being true would violate the laws, although I'm not yet sure exactly how.

I imagine that the laws, as stated in terms of <=, imply the standard laws regarding <. Specifically,

• Irreflexive: not a < a
• Transitive: a < b && b < c => a < c
• Connected: a /= b => a < b || b < a

If l < r && r < l then we can take a = l, b = r, and c = l in the transitive law to get l < l, which violates the irreflexive law.

I assume (because Wikipedia says so) that the laws we have on <= are equivalent to the laws above on < but I haven't worked through the proof yet. I am working (in my spare time, so not at any great pace) on a Gist which would try to prove the connections between:

• The laws of <= as stated in the documentation
• The laws of <= as stated on Wikipedia (basically the same but with an extra "strongly connected" law that I think is equivalent to <= being a total function)
• The laws of < as stated above
• The laws of compare
• The laws of min and max (they should form a lattice of some kind)

Hopefully, that will clarify what's going on here and maybe we can think again about the best way to document Ord. I for one would like to see the addition of laws for compare to the docs since compare is how one actually implements Ord instances.

But in the short-term I think we can just make that simple change in the PR and close this issue.

[Thimoteus]

l < r is shorthand for l <= r && l /= r, or equivalently if you're taking < as basic then l <= r is shorthand for l < r || l = r

[JordanMartinez]

Closed by #298.