[Haskell-cafe] A question about GHC test coverage

[Richard A. O'Keefe]

On 22/02/17 9:25 AM, Olaf Klinke wrote:
>>
> If you define an Ord instance that is only a preorder rather than a total order, and then downstream rely on functions f that violate the property
>
> x == y implies f x == f y,
>
> I'd call that poor design.

And I would call it a straw man.
I am talking about a TOTAL ORDER.
Antisymmetric, transitive, and total.
As for x == y implying or not f x == f y, I really don't have
any alternative there.  == and compare are handed to me by the
domain, and the observable difference between definitions of max
turns out (now that I've found it) to be precisely one of the
things I have to model.

I know that "the type system cannot guarantee that every Ord instance
is actually a total order", which is why I have tests for Ord.

The issue is a common issue when you have abstract data types:
there can be values x y such that x == y but x is not identical to y.

Here is is the classic example in Haskell.
Prelude> let pz = 0.0 :: Double
Prelude> let nz = -pz
Prelude> pz == nz
True
Prelude> show pz == show nz
False
Prelude> max pz nz
-0.0
Prelude> max nz pz
0.0

The result of max is well defined up to == but
not well defined up to identity.  By the way, LIA-2 section
5.2.2 "Floating point maximum and minimum" is very
clear that maxF(+0.0, -0.0) is +0.0, so Haskell is
incompatible with LIA-2 here.  And we are not talking
about infinities or NaNs here; we're talking about
strictly the finite floats.

This *isn't* my actual problem, but it's very close in spirit.

Now the substitution principle is pretty important, but
quite clearly the equality function in Haskell is not the
equality that the principle is about.  For one thing,
when talking *about* Haskell, it is natural to say that
if f = g then ($ x) f = ($ x) g, but the equality on the
left is not expressible in Haskell.  For another, since
we have System.Timeout, we can have two expressions u, v
such that u == v (eventually) evaluates to True, but
f u experiences a timeout and f v does not, so they end
up returning unequal results.