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.
This is something I've also struggled with. I'm coming to the conclusion that it'd really be useful for the "Gen" monad to be parameterizable with some user state, or maybe even be made into a transformer. The only alternative really seems to be passing around the extra information manually between generator-creation functions, and this quickly gets to be a pain. For me this is probably the most serious short-coming of QuickCheck. --Ben On 14 Oct 2008, at 23:36, Norman Ramsey wrote:
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