[Haskell] Abusing quickcheck to check existential properties

[Norman Ramsey]

 > > I guess what I would like is to reuse most of the mechanisms in
 > > QuickCheck to have it say one of these two things:
 > > 
 > >   1. Found an satisfying instance after 73 tries: [gives instance]
 > > 
 > >   2. After 100 tries, could not find a satisfying instance.
 > > 
 > > Like failure, the first tells you something definite about your
 > > program.  And like passing 100 tests, the second tells you nothing.
 > 
 > What you're asking for is similar to what SmallCheck could give you, but 
 > in the context of exhaustive testing of small values not sample testing 
 >   of random values.  However:
 > 
 > 1. As most existentials are within the scope of a universal, there are 
 > many instances tested, so when a witness is indeed found nothing is 
 > reported.
 > 
 > 2. A report is given only when no witness can be found within the 
 > specified search depth -- or when more than one can be found in the case 
 > of a unique existential.

Exactly what I'm looking for.

 > Perhaps your final remark is tongue-in-cheek?

Perhaps it's taken out of context :-)

It was in a reply to Edward Kmett and was a copy of something Edward
had said, with existentials exchanged for universals.  I was aiming to
make the point that if the inability to find a witness is not
interesting, then the inability to find a counterexample is also not
interesting.  Since many of us may think we have learned something
useful about a program when QuickCheck or SmallCheck fails to find a
counterexample of a universal claim, perhaps we should reason
contrapositively and agree that we have also learned something useful
if QuickCheck or SmallCheck fails to find a witness of an existential
claim.   In other words, I was disagreeing with Edward.  Way too
subtly :-)

 > I agree the question of what "passed 100 tests" tells you is
 > tricky; but it isn't "nothing".

I agree violently on both points :-)

 > Anyway, in SmallCheck knowing that any witness could only be beyond the 
 > search depth does tell you something (eg. the expected witness might be 
 > a position in a list where the search depth is the length of the list).

Indeed so.

Now if only I could find time to adapt QuickCheck and/or SmallCheck to
generate unit tests for C code (I'm currently teaching C and assembly
language) I would be one happy camper!


Norman