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.