[Haskell] Abusing quickcheck to check existential properties

Norman Ramsey nr at cs.tufts.edu
Sat Oct 18 18:39:32 EDT 2008

 > The answer is that QuickCheck can't correctly constructively verify an
 > existential condition without a constructive mechanism to generate the
 > existential (i.e. the Skolem function mentioned before).

I agree but don't think it's relevant.  QuickCheck can't verify a
universal either.

 > If [elided] you can abuse [QuickCheck] but unfortunately this costs
 > you the invariant that when quickcheck says something is wrong that
 > something really is wrong.
 > And to me at least the value of QuickCheck is that it never cries wolf.

It's a great point, and I agree completely.  

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.


More information about the Haskell mailing list