Using QuickCheck to Verify Free Monad's Functor Instance

Question

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?

Answer 1

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.