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