[Haskell] Abusing quickcheck to check existential properties

Norman Ramsey nr at cs.tufts.edu
Tue Oct 14 18:36:08 EDT 2008


 > > But how do I use QuickCheck to check an existential?
 > 
 > The "standard" method in QuickCheck is to be constructive, and
 > actually implement the function that constructs for the value. So,
 > instead of
 > 
 >   forAll x . exists y . P(x,y)
 > 
 > you write
 > 
 >   forAll x . P(x, find_y(x))
 

Interesting.  For A-E properties I can see where this approach would
be helpful, especially if it's not too hard to think of a good skolem
function.  In my case x is empty and so I'm left with

  'find a y such that P(y)'

or a bit more exactly

  'find an x in the four-dimensional unit cube such that 0.9 < f(x)'

I've already written f and I'd really rather not write f-inverse;
I want the computer to do some of the work for me.  So perhaps
SmallCheck would be a better way to go.

It does seem a pity, as almost all the QuickCheck machinery would be
useful in such a search.  On the other hand there are similar
scenarios on which I've already given up in despair, such as writing a
generator for creating well-typed terms in a nontrivial language.

Anyway, thanks for suggesting a skolem function---I'm sure I'll find
use for one sooner or later.


Norman


More information about the Haskell mailing list