A question about GHC test coverage

Olaf Klinke

14 Feb 2017 14 Feb '17

4:35 p.m.

You should not have to write tests for functions you did not define. Correct me if I'm wrong, but any property of max can be derived from the properties of <=. Sadly, the laws for Ord are not stated in the documentation of Data.Ord. (Because there is no consensus?) They are: Reflexive: if x == y then x <= y Transitive: if x <= y and y <= z then x <= z Antisymmetric: if x <= y and y <= x then x == y Olaf

Show replies by date

Richard A. O'Keefe

20 Feb 20 Feb

5:05 p.m.

On 15/02/17 10:35 AM, Olaf Klinke wrote:

...

You should not have to write tests for functions you did not define.

Correct me if I'm wrong, but any property of max can be derived from the properties of <=. Unfortunately, this isn't quite true. Suppose we have two values x y such that x <= y && y <= x && x == y *BUT* x and y are distinguishable some other way. For example, suppose we are modelling rational numbers by pairs (n,d) *without* insisting that gcd(n,d) == 0. Then we have (n1,d1) == (n2,d2) = n1*d2 == n2*d1 compare (n1,d1) (n2,d2) = compare (n1*d2) (n2*d1) BUT (1,2) and (2,4), while ==, are none-the-less distinguishable. Now ask about max x y. If we have max a b = if a > b then a else b then max x y delivers y. But if we have max a b = if a < b then b else a then max x y delivers x, and these two results can be distinguished. I know and freely admit that if I want a version of max that satisfies stronger conditions than Ord can guarantee, it is up to me to write it. So you could say that the bug was that I *should* have written my own max, and didn't. But that's basically my point. (For an example of two values that can't be distinguished by compare or ==, consider -0.0 and +0.0. If I give those to max, what do I get back? No, that wasn't the test case I needed.)

Olaf Klinke

21 Feb 21 Feb

3:25 p.m.

...

Am 20.02.2017 um 23:05 schrieb Richard A. O'Keefe :

On 15/02/17 10:35 AM, Olaf Klinke wrote:

...
You should not have to write tests for functions you did not define.

Correct me if I'm wrong, but any property of max can be derived from the properties of <=.

Unfortunately, this isn't quite true.

Suppose we have two values x y such that x <= y && y <= x && x == y *BUT* x and y are distinguishable some other way. For example, suppose we are modelling rational numbers by pairs (n,d) *without* insisting that gcd(n,d) == 0. Then we have (n1,d1) == (n2,d2) = n1*d2 == n2*d1 compare (n1,d1) (n2,d2) = compare (n1*d2) (n2*d1) BUT (1,2) and (2,4), while ==, are none-the-less distinguishable.

Now ask about max x y. If we have

max a b = if a > b then a else b

then max x y delivers y. But if we have

max a b = if a < b then b else a

then max x y delivers x, and these two results can be distinguished.

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. The above formula would be something for a Quickcheck module. That said, I myself found it handy in the past to define such preordered types.

...

I know and freely admit that if I want a version of max that satisfies stronger conditions than Ord can guarantee, it is up to me to write it. Or rather, be aware of the standard implementation of max in Data.Ord. Anyways, you are right: Since the type system can not guarantee that every Ord instance is actually a total order, test coverage statistics won't help us here.

Regards, Olaf

Richard A. O'Keefe

8:01 p.m.

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.

3010

Age (days ago)

3018

Last active (days ago)

List overview

Download

3 comments

2 participants

participants (2)

Olaf Klinke
Richard A. O'Keefe