[Haskell] Testing polymorphic properties with QuickCheck

Thu Oct 1 11:13:05 EDT 2009

-----------------------------------------------------------------------
This message is a literate Haskell file, hence:
> {-# LANGUAGE GADTs#-} -- a matter of style only
> import Control.Monad.State hiding (mapM)
> import Control.Applicative
> import Data.Traversable
> import Data.Foldable
> import Data.Monoid
> import Test.QuickCheck
---------------------------------------------------------------------

Hello everyone,

This message is my answer a common question coming from
QuickCheck users: "How do I use QuickCheck on polymorphic
properties?". The answer also applies to all test generators for
Haskell (SmallCheck, ...).

Consider the following polymorphic property:

> prop_reverse_append :: Eq a => [a] -> [a] -> Bool
> prop_reverse_append xs ys = reverse (xs ++ ys) == reverse xs ++ reverse ys

Running QuickCheck on that property is possible, but...

< quickCheck prop_reverse_append
< ... 100 tests passed!

Even though the property is false, it passes QuickCheck, because GHC
has defaulted |a| to |()|, and the unit type cannot capture any difference
in the content of the lists.

The usual QuickCheck answer is to force using |Int| for |a|:

> prop_reverse_append_Int :: [Int] -> [Int] -> Bool
> prop_reverse_append_Int = prop_reverse_append

While sound, this is highly unsatisfactory:

2. Some tests will be weaker than necessary. For example, testing
|prop_reverse_append| with elements that are equal to each other is a
waste: this might only hide bugs in the implementation, as when we
used the unit type.

In fact, one should test |prop_reverse_append| only once for each
length of the input lists, and the elements in the lists should all be
different from each other. Note that this observation applies not only
to |prop_reverse_append|, but to all properties of the same type.

In the remainder I will show how to generalize the argument, and give
a systematic method to compute a monomorphic property which is as
strong as a polymorphic one. This is done only by looking at the type
of the property.

The basic idea is to identify all the ways that the property can
construct elements of the polymorphic type (say |a|), and represent
this in a datatype.

For example, the type |Eq a => [a] -> [a] -> Bool| tells us that the
property can construct an element by picking any element from the
first or the second list.  This yields the datatype:

> data A where
>    XsElement :: Int -> A
>    YsElement :: Int -> A
>  deriving (Eq, Show)

Which we can substitute for the type variable. The gain comes from the
fact that we also know how to fill in the input lists, yielding the
monomorphic property:

> prop_reverse_append_Mono :: [()] -> [()] -> Bool
> prop_reverse_append_Mono xs ys
>   = prop_reverse_append (combine XsElement xs) (combine YsElement ys)

where |combine f| replaces the |i|:th element in the list with |f i|.

Generalization 1
----------------

It is worth noting that "observations", that is, elements which do not
return any |a|, do not play any role in the monomorphisation
process. This is illustrated in the next example, about testing a
filter-like function:

> prop_filter :: Eq a => (a -> Bool) -> [a] -> Bool
> prop_filter = error "add your definition here"

> prop_filter_Mono :: (A -> Bool) -> [()] -> Bool
> prop_filter_Mono p xs = prop_filter p (combine XsElement xs)

Generalization 2
----------------

Arguments which return |a| are turned into constructors of
the monomorphic datatype, and then fixed.

> prop_iterate :: Eq a => a -> (a -> a) -> Bool
> prop_iterate = error "add your definition here"

> data B where
>     Initial :: B
>     Next    :: B -> B
>   deriving (Eq, Show)

> prop_iterate_Mono = prop_iterate Initial Next

Note that the more polymorphic the function is, the more the arguments
become fixed. In the above case, all quantifiers disappear.

Notes
-----

Note that the technique works only for first order polymorphic
arguments. We do not have a generalization for higher order
ones. Also, extra care must be taken in the presence of type classes
constraints: they may "hide" constructors.

More examples and applications, together with the theory behind all
this can be found in a paper I co-authored with Patrik Jansson and Koen
Claessen:

http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=99387
or direct link to the pdf:
http://www.cse.chalmers.se/~bernardy/PolyTest.pdf

Cheers,
Jean-Philippe Bernardy.

PS.

Definition of |combine|
-----------------------

> combine :: Traversable t => (Int -> a) -> t () -> t a
> combine f t = evalState (Data.Traversable.mapM getValue t) 0
>     where getValue _ = do i <- get
>                           put (i+1)
>                           return (f i)

Example:

< combine Just (Node (Leaf ()      ) ()       (Node (Leaf ()      ) ()
      (Leaf ())))
<      ==      (Node (Leaf (Just 0)) (Just 1) (Node (Leaf (Just 2))
(Just 3) (Leaf (Just 4))))

> data Tree a = Empty | Leaf a | Node (Tree a) a (Tree a) deriving Show
> instance Traversable Tree where
>   traverse f Empty = pure Empty
>   traverse f (Leaf x) = Leaf <$> f x
>   traverse f (Node l k r) = Node <$> traverse f l <*> f k <*> traverse f r

> instance Foldable Tree where foldMap = foldMapDefault
> instance Functor Tree where fmap = fmapDefault