Add tests for the relationship between leq and compare

[mitchellwrosen]

This patch adds a test for the relationship between leq and compare:

if x leq y,
 if y leq x,
    x compare y should be EQ
  else
    x compare y should be LT
else
  x compare y should be GT

The test suite is failing because the derived instances of Ord for the types Dropped, etc. violate this property (the constructors are backwards)

[phadej]

adding PartialOrd instances is :+1:

Imposing law for Ord is :-1:.

Library has:

instance (PartialOrd a, PartialOrd b) => PartialOrd (a, b) where
    -- NB: *not* a lexical ordering. This is because for some component partial orders, lexical
    -- ordering is incompatible with the transitivity axiom we require for the derived partial order
    (x1, y1) `leq` (x2, y2) = x1 `leq` x2 && y1 `leq` y2

and it's correct

[mitchellwrosen]

Oh... interesting! Is it a special case? Are there any other types besides tuples for which the PartialOrd instance may not agree with the Ord instance?

Or asked differently, if PartialOrd was in base, would it be a superclass of Ord?

[mitchellwrosen]

And separately: is it not a bug then that

Drop 5 `leq` Top

but

Drop 5 > Top

?

[phadej]

I think having leq and <= agree were sensibly possible is good goal (so I'm :+1: on changing order of constructors in Dropped).

Yet I don't want expose the requirement leq = <=. I have usecases where leq is interesting in the "buisness domain"; where Ord is used to put things into Data.Set. (EDIT: I guess I have to explain this in the docs, but if you are willing to write as stub, that would be great!)

[mitchellwrosen]

@phadej Sounds good. I've removed the tests, and made leq = (<=) for Dropped, Levitated, Lifted, and Op.

It would be awfully nice if leq = (<=) was a law but that discussion can be moved to a new ticket :)

[phadej]

Merged in https://github.com/phadej/lattices/commit/787b093eeb046a8c8e708e9a547c4d20dbb67b76