[Haskell] Abusing quickcheck to check existential properties
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.
More information about the Haskell