> > 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 _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell