# Using QuickCheck to Verify Free Monad's Functor Instance

Given the Free Monad, and my Eq, Show, and Functor instances, I attempted to verify the first Functor law using QuickCheck:

data Free f a = Var a
| Node (f (Free f a))


I defined the following Eq and Show instances (credit to duplode for helping me out on the Eq instance:

instance (Eq (f (Free f a)), Eq a) => Eq (Free f a) where
(==) (Var x) (Var y)       = x == y
(==) (Node fu1) (Node fu2) = fu1 == fu2
(==) _ _                   = False

instance (Show (f (Free f a)), Show a) => Show (Free f a) where
show (Var x)  = "Var " ++ (show x)
show (Node x) = "Node " ++ (show x)


Then, I implemented a Functor instance:

instance Functor f => Functor (Free f) where
fmap g (Var x)  = Var (g x)
fmap g (Node x) = Node $fmap (\y -> fmap g y) x  And now the QuickCheck work: instance Arbitrary (Free Maybe Int) where arbitrary = do x <- arbitrary :: Gen Int y <- arbitrary :: Gen Int elements [Var x, Var y, Node (Nothing), Node (Just (Var y))] --fmap id = id functor_id_law :: Free Maybe Int -> Bool functor_id_law x = (fmap id x) == (id x)  Finally, run it in QuickCheck: ghci> quickCheck functor_id_law +++ OK, passed 100 tests.  However, I haven't included other Functor's, such as [], etc. Nor have I used other types, i.e. Char, String, etc. What's a more rigorous approach to verifying that my definition of the Free Monad's Functor instance obeys the first Functor Law? ## 1 Answer # Use Eq1 to implement Eq, Show1 to implement Show While it's a very recent addition, you should implement Eq via Eq1 and Show via Show1. That removes the UndecidableInstances pragma from your code: import Data.Functor.Classes data Free f a = Var a | Node (f (Free f a)) instance (Eq1 f) => Eq1 (Free f) where liftEq f (Var x) (Var y) = f x y liftEq f (Node fu1) (Node fu2) = liftEq (liftEq f) fu1 fu2 liftEq _ _ _ = False instance (Eq1 f, Eq a) => Eq (Free f a) where (==) = eq1 instance Show1 f => Show1 (Free f) where liftShowsPrec sp sl = go where go d (Var a) = showsUnaryWith sp "Var" d a go d (Node fa) = showsUnaryWith (liftShowsPrec go (liftShowList sp sl)) "Node" d fa instance (Show1 f, Show a) => Show (Free f a) where showsPrec = showsPrec1  We need to lift twice: once through the functor f, and once through the next Free. # QuickCheck Your instance isn't very flexible. Furthermore, QuickCheck cannot set its size. Instead of a fixed size, use sized: instance Arbitrary (Free Maybe Int) where arbitrary = sized go where go 0 = Var <$> arbitrary
go n = Node <$> oneof [pure Nothing, Just <$> go (n - 1)]


However, that only yields a single instance. As with Show and Eq, there exists an Arbitrary1 class we can use instead:

instance Arbitrary1 f => Arbitrary1 (Free f) where
liftArbitrary a = sized (go . min 3)
where
go 0 = Var <$> a go n = Node <$> liftArbitrary (go (n - 1))

instance (Arbitrary1 f, Arbitrary a) => Arbitrary (Free f a) where
arbitrary = arbitrary1


We can now check the functor id law easily for many combinations.

# The more rigorous approach

The more rigorous approach with functor laws is to proof them by hand. So let us assume that functor laws hold for the functor f in Free f a. Then we have to show that

fmap id value = value


for any value :: Free f a. There are two cases. Either value is a Var x for some x :: a. Then

fmap id value = fmap id (Var x) = Var (id x) = Var x = value


and the law holds. Or value is a Node y for some y :: f (Free f a). Then

fmap id value = fmap id (Node y)
= Node (fmap id y)
= Node (id y)      -- used functor law for f'
= Node y
= value
`

Therefore, the first functor law holds for your instance.