> 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. Norman _______________________________________________ Haskell mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell
