seeking lore of the QuickCheck masters

[Malcolm Wallace]

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