Bodigrim/smallcheck

questionable wording of conterexample output (there exists 0 1 such that...)

jwaldmann opened this issue · 2 comments

Hi.

The 1.0 release looks good, and contains some features that I sure want to use.

Nit-pick-ingly, I don't know whether the following change is an improvement:

smallcheck-0.6

smallCheck 3 $ \ x y -> x+y==x-(y :: Int)
Depth 0:
  Completed 1 test(s) without failure.
Depth 1:
  Failed test no. 1. Test values follow.
  -1
  -1

smallcheck-1.0.2

smallCheck 3 $ \ x y -> x+y==x-(y :: Int)
Failed test no. 2.
there exist 0 1 such that
  condition is false

The phrase "there exist 0 1 such that" is mathematically meaningless
(the numbers 0 and 1 do exist anyway), and actually a syntax error (after "exists", a variable must follow). I am sensitive to this because of using smallcheck in teaching.

It would be simpler, and mathematically correct, to just say something like the following?

condition 0 1 == False

I totally agree that the current wording is not ideal.

But we cannot consider one case in isolation. To understand the variety of situations, take a look at Pretty instances in Test.SmallCheck.Property.Result. Your wording doesn't generalize to all of them.

If you can suggest a scheme that covers all cases (preferably in the form of a patch), I'd be glad to consider it.

Closing for now; feel free to comment/reopen with a proposed solution.