seeking lore of the QuickCheck masters

[John Hughes]

On Tue, 15 Apr 2003, Malcolm Wallace wrote:

> nr@eecs.harvard.edu (Norman Ramsey) writes:
>
> > I am playing around with an implementation of a little language,
> > and I would like to use QuickCheck to test my code.  My problem is
> > that I want to test only well-typed terms.  I don't know how to craft
> > my `arbitrary' functions so that the probability of generating a well-typed
> > term is more than vanishingly small.  Can anybody pass on interesting
> > tips and tricks that might help?
>
> You want a generator that can produce an arbitrary code fragment,
> *given* what type you want it to have.  So first, generate an arbitrary
> type, then generate an arbitrary expression for it.
>
> Assuming that your little language is sort-of functional, then to
> generate a code fragment for a given type, say Int, you might have
> the following choices:
>
>  * Generate a literal value :: Int
>  * Generate a conditional.
>        e.g.  if <arbitrary :: Bool> then <arbitrary :: Int> else <arbitrary :: Int>
>  * Generate a case.
>        e.g.  case <arbitrary :: a> of
>                  <arbitrary pattern :: a>  ->  <arbitrary :: Int>
>                  <arbitrary pattern :: a>  ->  <arbitrary :: Int>
>  * and so on for other language constructs.
>  * Generate an application of a unary function
>                :: ArbitraryType a => a -> Int
>    or perhaps  :: ArbitraryTypeInvolving Int a => a -> Int
>    to a value of the constrained type.
>  * Generate an application of a binary function
>        :: (ArbitraryType a)                  => a -> (a -> Int)
>    or  :: (ArbitraryType a, ArbitraryType b) => a -> (b -> Int)
>    or  :: (ArbitraryTypeInvolving Int a)                  => a -> (a -> Int)
>    or  :: (ArbitraryTypeInvolving Int a, ArbitraryType b) => a -> (b -> Int)
>    or  :: (ArbitraryTypeInvolving Int b, ArbitraryType a) => a -> (b -> Int)
>    to a value of the constrained type.
>  * and so on for more complex types.
>
> It is quite a lot trickier than this little sketch, I'm sure, but I
> hope this helps to spark some more ideas.
>
> Regards,
>     Malcolm

Yes, this is how I would do it. Then, of course, it's important to control
the size of the generated terms. I would write a sized generator dividing
the size between sub-expressions, and restricting expressions to be
lambdas, constants or variables when the size reaches zero.

John