[Haskell] Abusing quickcheck to check existential properties

[Koen Claessen]

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