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.