----------------------------------------------------------------------- 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: 1. Many tests will be redundant. For example, if |prop_reverse_append [1] [2]| holds, then |prop_reverse_append [a] [b]| holds for any choice of a and b. So if the first test passes, it is useless to test |prop_reverse_append [1] [3]|, |prop_reverse_append [1] [4]|, etc. Unfortunately, QuickCheck does not realize this and may perform all these tests. 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