Verifying Typeclass Laws in Haskell with QuickCheck

Austin Rochford

2014-05-27

Recently, I was somewhat idly thinking about how to verify that Haskell typeclasses satisfy the appropriate laws. My first thought was to use equational reasoning to prove that the laws hold. For example, to verify that the left identity law holds for the Maybe monad, we can show that

return x >>= f = Just x >>= f = f x

While this proof is simple (due to the simplicity of the Maybe monad), I wanted a solution expressed in executable Haskell that could be included in a test suite. As with many Haskell testing problems, QuickCheck seemed to be a natural solution. In this post, I’ll show how to verify typeclass laws using QuickCheck for the classes Monoid, Functor, and Monad.

Monoids

The definition of the Monoid typeclass is

class Monoid a where
  mappend :: a -> a -> a
  mempty :: a

The module Data.Monoid defines the infix operator (<>) as a synonym for mappend. We will use the more consise operator form here.

An instance of Monoid must satisy the associative law

x <> (y <> z) == (x <> y) <> z

and the identity laws

x <> mempty == x

and

mempty <> x == x

We begin by writing a proposition to test the assocative law, which is fairly straightforward.

{-# LANGUAGE ViewPatterns #-}

module Laws where

import Control.Applicative ((<$>))

import Data.Monoid

import Test.QuickCheck
import Test.QuickCheck.Function
import Test.QuickCheck.Gen

monoidAssocProp :: (Eq m, Monoid m) => m -> m -> m -> Bool
monoidAssocProp x y z = (x <> (y <> z)) == ((x <> y) <> z)

We can use this code to test the Monoid instance of [Int] as follows.

> quickCheck (monoidAssocProp :: [Int] -> [Int] -> [Int] -> Bool)
+++ OK, passed 100 tests.

It is important to include the type annotation, as monoidAssocProp is written to be applicable to any monoid (technically any monoid that is also an instance of Eq, but this restriction is not too onerous).

Similarly, we can test the right and left identity laws as follows.

monoidRightIdProp :: (Eq m, Monoid m) => m -> Bool
monoidRightIdProp x = x == (x <> mempty)

monoidLeftIdProp :: (Eq m, Monoid m) => m -> Bool
monoidLeftIdProp x = (mempty <> x) == x

> quickCheck (monoidRightIdProp :: [Int] -> Bool)
+++ OK, passed 100 tests.

> quickCheck (monoidLeftIdProp :: [Int] -> Bool)
+++ OK, passed 100 tests.

At this point, we can feel reasonable sure that the Monoid instance of [Int] satisfies the monoid laws. QuickCheck supports testing many monoids out-of-the-box in this manner, but others require more work on our part.

Suppose we would like to check the monoid laws for Sum Int. (Recall that mappend for Sum Int is addition and mempty is zero.)

> quickCheck (monoidRightIdProp :: Sum Int -> Bool)

Unfortunately, this command fails with the following message.

No instance for (Arbitrary (Sum Int))
  arising from a use of `quickCheck'
Possible fix: add an instance declaration for (Arbitrary (Sum Int))
In the expression:
  quickCheck (monoidRightIdProp :: Sum Int -> Bool)
In an equation for `it':
    it = quickCheck (monoidRightIdProp :: Sum Int -> Bool)

In order to generate test cases, QuickCheck requires the arguments of our proposition to be instances of the Arbitrary class. Fortunately, since Int is an instance of Arbitrary, we can quickly make Sum Int an instance of arbitrary as well. In fact, for any data type a which is an instance of Arbitrary, we will make Sum a an instance of Arbitrary as well.

instance (Arbitrary a) => Arbitrary (Sum a) where
    arbitrary = Sum <$> arbitrary

Now we can verify the monoid laws for Sum Int.

> quickCheck (monoidAssocProp :: Sum Int -> Sum Int -> Sum Int -> Bool)
+++ OK, passed 100 tests.

> quickCheck (monoidRightIdProp :: Sum Int -> Bool)
+++ OK, passed 100 tests.

> quickCheck (monoidLeftIdProp :: Sum Int -> Bool)
+++ OK, passed 100 tests.

Functors

Even considering the need to define Arbitrary instances for some Monoids, testing the monoid laws was fairly straightforward. Testing the functor laws with QuickCheck is a bit more involved, due to the need to generate random functions between Arbitrary instances.

The definition of the Functor typeclass is

class Functor f where
    fmap :: (a -> b) -> f a -> f b

An instance of Functor must satisfy the identity law

fmap id = id

and the composition law

fmap (f . g) = fmap f . fmap g

Testing the identity law is relatively simple, since it does not involve arbitrary functions.

functorIdProp :: (Functor f, Eq (f a)) => f a -> Bool
functorIdProp x = (fmap id x) == x

We can test the identity law for the Maybe functor applied to Strings.

> quickCheck (functorIdProp :: Maybe String -> Bool)
+++ OK, passed 100 tests.

Testing the composition law is a bit more complicated, as f :: a -> b and g :: b -> c may be arbitrary functions. Fortunately, Test.QuickCheck.Function provides a way to generate arbitrary functions a -> b (as long as a and b are instances of appropriate typeclasses). The Fun data type from this module represents an arbitrary function. With this module, we can write a proposition testing the composition law as follows.

functorCompProp :: (Functor f, Eq (f c)) => f a -> Fun a b -> Fun b c -> Bool
functorCompProp x (apply -> f) (apply -> g) = (fmap (g . f) x) == (fmap g . fmap f $ x)

Here we use a view pattern to extract a function a -> b from the second argument, which has type Fun a b, using the apply function. We similarly use a view pattern to extract a function b -> c from the third argument.

We can use this function to test the composition law for the list functor applied to Int with two functions Int -> Int as follows

> quickCheck (functorCompProp :: [Int] -> Fun Int Int -> Fun Int Int -> Bool)
+++ OK, passed 100 tests.

The test functorCompProp is rather flexible. We can test the Functor instance of Maybe, staring with Int and involving arbitrary functions Int -> String and String -> Double as follows.

> quickCheck (functorCompProp :: Maybe Int -> Fun Int String -> Fun String Double -> Bool)
+++ OK, passed 100 tests.

For certain types, this test may take a while to run, as generating arbitrary functions can take some time for the right (or wrong, depending on your point of view) combination of domain and range types.

Monads

As with functors, testing the monad laws relies heavily on the Arbitrary instance of Fun, with slightly more complicated types.

The definition of the Monad typeclass is

class Monad m where
    (>>=) :: m a -> (a -> m b) -> m b
    return :: a -> m a

An instance of Monad must satisfy three laws. The first is the right identity law,

x >>= return = x

The second is the left identity law,

return x >>= f = f x

The third is the associative law,

(x >>= f) >>= g = x >>= (\x' -> f x' >>= g)

Testing the right identity law is fairly straightforward, because it involves no arbitrary functions.

monadRightIdProp :: (Monad m, Eq (m a)) => m a -> Bool
monadRightIdProp x = (x >>= return) == x

We can test the right identity law for the type Either String Int (recall that Either a is a monad) as follows

> quickCheck (monadRightIdProp :: Either String Int -> Bool)
+++ OK, passed 100 tests.

Since the left identity law only involves one arbitrary function, it is slightly simpler to test than the associative law.

monadLeftIdProp :: (Monad m, Eq (m b)) => a -> Fun a (m b) -> Bool
monadLeftIdProp x (apply -> f) = (return x >>= f) == (f x)

We can verify the left identity law for [Int] as follows.

> quickCheck (monadLeftIdProp :: Int -> Fun Int [Int] -> Bool)
+++ OK, passed 100 tests.

Finally, we write a test for the associative property.

monadAssocProp :: (Monad m, Eq (m c)) => m a -> Fun a (m b) -> Fun b (m c) -> Bool
monadAssocProp x (apply -> f) (apply -> g) = ((x >>= f) >>= g) == (x >>= (\x' -> f x' >>= g))

We can verify the associative law for the Maybe monad and functions f :: Int -> Maybe [Int] and g :: [Int] -> Maybe String as follows.

> quickCheck (monadAssocProp :: Maybe Int -> Fun Int (Maybe [Int]) -> Fun [Int] (Maybe String) -> Bool)
+++ OK, passed 100 tests.

This post is written in literate Haskell and the source available on GitHub.