Hi Norman, > 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)) for a suitably implemented function find_y. (This function is called a skolem function by logicians). It often depends on the problem domain how easy/hard it is to write such a function. For example, you may be actually able to just calculate y in find_y. Example: prop_Leq x (y :: Integer) = x <= y ==> exists d . d >= 0 s.t. x+d == y becomes prop_Leq x (y :: Integer) = x <= y ==> let d = y-x in d >= 0 && x+d == y In some cases though, some kind of search might be needed. The library SmallCheck provides default such search functions for Haskell types (if your search can be limited by a concept of depth). One thing that writing a skolem search function forces you to do is to decide when the existential can *not* be found (after all, we are interested in finding bugs). So, this forces you to think about what bounds you have on the search domain, which can be hard. /Koen _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell