### Verifying Typeclass Laws in Haskell with QuickCheck

Posted on May 27, 2014

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 `Monoid`s, 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 `String`s.

``````> 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.

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.