[Haskell] Abusing quickcheck to check existential properties

Koen Claessen koen at chalmers.se
Mon Oct 13 05:57:17 EDT 2008

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


  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.


More information about the Haskell mailing list