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