A question about GHC test coverage

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

A question about GHC test coverage

Olaf Klinke
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
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: A question about GHC test coverage

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.

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.)



_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: A question about GHC test coverage

Olaf Klinke

> Am 20.02.2017 um 23:05 schrieb Richard A. O'Keefe <[hidden email]>:
>
>
>
> 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
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: 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.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.