## Breaking the Law: Verifying Typeclass Laws with QuickCheck and Deja Fu

*Note: This is using (at the time of writing) the latest developmental version of Deja Fu, which is not yet on hackage. It will be soon! But until then, if you want to replicate this, clone from git.*

I recently implemented async-dejafu, a version of the async library using Deja Fu so programs written with it can be tested, and I was curious about checking the relevant typeclass laws automatically.

Checking typeclass laws has been done with QuickCheck before, but the difference here is that async uses *concurrency*! If only we had some way to test concurrent Haskell code! Oh, wait…

## The set-up

Specifically, I want to test the laws for the `Concurrently`

type. `Concurrently`

is a monad for expressing `IO`

actions which should be run concurrently.

Firstly, we need some language extensions and imports:

```
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}
module Concurrently where
import Control.Applicative
import Control.Exception (SomeException)
import Control.Monad ((>=>), ap, liftM, forever)
import Control.Monad.Catch (onException)
import Control.Monad.Conc.Class
import Data.Maybe (isJust)
import Data.Set (Set, fromList)
import Test.DejaFu (Failure(..), defaultMemType)
import Test.DejaFu.Deterministic (ConcST, Trace)
import Test.DejaFu.SCT (sctBound, defaultBounds)
import Test.QuickCheck (Arbitrary(..))
import Test.QuickCheck.Function (Fun, apply)
import Unsafe.Coerce (unsafeCoerce)
```

I have sadly not managed to eliminate that `unsafeCoerce`

, it shows up because of the use of higher-ranked types, and makes me very sad. If anyone knows how I can get rid of it, I would be very happy!

Now we need our `Concurrently`

type. The original just uses `IO`

, so we have to parameterise ours over the underlying monad:

```
newtype Concurrently m a = Concurrently { runConcurrently :: m a }
```

We’ll also be using a `ConcST`

variant for testing a lot, so here’s a type synonym for that:

```
type CST t = Concurrently (ConcST t)
```

We also need some instances for `Concurrently`

in order to make QuickCheck happy, but these aren’t terribly important:

```
instance Show (Concurrently m a) where
show _ = "<concurrently>"
instance (Arbitrary a, Applicative m) => Arbitrary (Concurrently m a) where
arbitrary = Concurrently . pure <$> arbitrary
```

Ok, let’s get started!

## Functor

`Functor`

lets you apply a pure function to a value in a context.

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

A `Functor`

should satisfy the identity law:

```
fmap id = id
```

And the composition law:

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

The `Functor`

instance for `Concurrently`

just delegates the work to the instance for the underlying monad:

```
instance MonadConc m => Functor (Concurrently m) where
fmap f (Concurrently a) = Concurrently $ f <$> a
```

The composition law is a little awkward to express in a way that QuickCheck can deal with, as it involves arbitrary functions. QuickCheck has a `Fun`

type, representing functions which can be serialised to a string. Bearing that in mind, here is how we can express those two laws as tests:

```
prop_functor_id :: Ord a => CST t a -> Bool
prop_functor_id ca = ca `eq` (id <$> ca)
prop_functor_comp :: Ord c => CST t a -> Fun a b -> Fun b c -> Bool
prop_functor_comp ca (apply -> f) (apply -> g) = (g . f <$> ca) `eq` (g <$> (f <$> ca))
```

We’re using view patterns here to extract the actual function from the `Fun`

value. let’s see if the laws hold!

```
λ> quickCheck (prop_functor_id :: CST t Int -> Bool)
+++ OK, passed 100 tests.
λ> quickCheck (prop_functor_comp :: CST t Int -> Fun Int Integer -> Fun Integer String -> Bool)
+++ OK, passed 100 tests.
```

Cool! Wait, what’s that `eq`

function?

### Equality and concurrency?

I’ve decided to treat two concurrent computations as equal if the sets of values that they can produce are equal:

```
eq :: Ord a => CST t a -> CST t a -> Bool
eq left right = runConcurrently left `eq'` runConcurrently right
eq' :: forall t a. Ord a => ConcST t a -> ConcST t a -> Bool
eq' left right = results left == results right where
results cst = fromList . map fst $ sctBound' cst
sctBound' :: ConcST t a -> [(Either Failure a, Trace)]
sctBound' = unsafeCoerce $ sctBound defaultMemType defaultBounds
```

This is where the unfortunate `unsafeCoerce`

comes in. The definition of `sctBound'`

there doesn’t type-check without it, which is a shame. If anyone could offer a solution, I would be very grateful.

## Applicative

`Applicative`

extends `Functor`

with the ability to inject a value into a context without introducing any effects, and to apply a function in a context to a value in a context.

```
class Functor f => Applicative f where
pure :: a -> f a
(<*>) :: f (a -> b) -> f a -> f b
```

An `Applicative`

should satisfy the identity law:

```
pure id <*> a = a
```

The homomorphism law, which says that applying a pure function to a pure value in a context is the same as just applying the function to the value and injecting the entire result into a context:

```
pure (f a) = pure f <*> pure a
```

The interchange law, which says that when applying a function in a context to a pure value, the order in which each is evaluated doesn’t matter:

```
u <*> pure y = pure ($ y) <*> u
```

And the composition law, which is a sort of associativity property:

```
u <*> (v <*> w) = pure (.) <*> u <*> v <*> w
```

Finally, there is a law relating `Applicative`

to `Functor`

, that says we can decompose `fmap`

into two steps, injecting a function into a context, and then application within that context:

```
f <$> x = pure f <*> x
```

This is where `Concurrently`

gets its concurrency. `(<*>)`

runs its two arguments concurrently, killing the other if one throws an exception.

```
instance MonadConc m => Applicative (Concurrently m) where
pure = Concurrently . pure
Concurrently fs <*> Concurrently as = Concurrently $
(\(f, a) -> f a) <$> concurrently fs as
concurrently :: MonadConc m => m a -> m b -> m (a, b)
concurrently = ...
```

Armed with the knowledge of how to generate arbitrary functions, these are all fairly straight-forward to test

```
prop_applicative_id :: Ord a => CST t a -> Bool
prop_applicative_id ca = ca `eq` (pure id <*> ca)
prop_applicative_homo :: Ord b => a -> Fun a b -> Bool
prop_applicative_homo a (apply -> f) = (pure $ f a) `eq` (pure f <*> pure a)
prop_applicative_inter :: Ord b => CST t (Fun a b) -> a -> Bool
prop_applicative_inter u y = (u' <*> pure y) `eq` (pure ($ y) <*> u') where
u' = apply <$> u
prop_applicative_comp :: Ord c => CST t (Fun b c) -> CST t (Fun a b) -> CST t a -> Bool
prop_applicative_comp u v w = (u' <*> (v' <*> w)) `eq` (pure (.) <*> u' <*> v' <*> w) where
u' = apply <$> u
v' = apply <$> v
prop_applicative_fmap :: Ord b => Fun a b -> CST t a -> Bool
prop_applicative_fmap (apply -> f) a = (f <$> a) `eq` (pure f <*> a)
```

And indeed we see that the laws hold:

```
λ> quickCheck (prop_applicative_id :: CST t Int -> Bool)
+++ OK, passed 100 tests.
λ> quickCheck (prop_applicative_homo :: String -> Fun String Int -> Bool)
+++ OK, passed 100 tests.
λ> quickCheck (prop_applicative_inter :: CST t (Fun Int String) -> Int -> Bool)
+++ OK, passed 100 tests.
λ> quickCheck (prop_applicative_comp :: CST t (Fun Int String) -> CST t (Fun Char Int) -> CST t Char -> Bool)
+++ OK, passed 100 tests.
λ> quickCheck (prop_applicative_fmap :: Fun Int String -> CST t Int -> Bool)
+++ OK, passed 100 tests.
```

## Alternative

`Alternative`

is a kind of monoid over `Applicative`

.

```
class Applicative f => Alternative f where
empty :: f a
(<|>) :: f a -> f a -> f a
-- These both have default definitions
some :: f a -> f [a]
many :: f a -> f [a]
```

An `Alternative`

should satisfy the monoid laws. Namely, left and right identity:

```
empty <|> x = x
x <|> empty = x
```

And associativity:

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

The `Alternative`

instance for `Concurrently`

is used to express races, with `(<|>)`

executing both of its arguments concurrently and returning the first to finish:

```
instance MonadConc m => Alternative (Concurrently m) where
empty = Concurrently $ forever yield
Concurrently as <|> Concurrently bs =
Concurrently $ either id id <$> race as bs
race :: MonadConc m => m a -> m b -> m (Either a b)
race = ...
```

Once again, the translation into QuickCheck properties is quite simple:

```
prop_alternative_right_id :: Ord a => CST t a -> Bool
prop_alternative_right_id x = x `eq` (x <|> empty)
prop_alternative_left_id :: Ord a => CST t a -> Bool
prop_alternative_left_id x = x `eq` (empty <|> x)
prop_alternative_assoc :: Ord a => CST t a -> CST t a -> CST t a -> Bool
prop_alternative_assoc x y z = (x <|> (y <|> z)) `eq` ((x <|> y) <|> z)
```

And the laws hold!

```
λ> quickCheck (prop_alternative_right_id :: CST t Int -> Bool)
+++ OK, passed 100 tests.
λ> quickCheck (prop_alternative_left_id :: CST t Int -> Bool)
+++ OK, passed 100 tests.
λ> quickCheck (prop_alternative_assoc :: CST t Int -> CST t Int -> CST t Int -> Bool)
+++ OK, passed 100 tests.
```

There are also some laws relating `Alternative`

to `Applicative`

, but these are expressed in terms of `some`

and `many`

, which have default law-satisfying definitions.

## Monad

`Monad`

extends `Applicative`

with the ability to squash nested monadic values together, and are commonly used to express sequencing.

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

There are a few different formulations of the `Monad`

laws, I prefer the one in terms of `(>=>)`

(the fish operator), which is defined as:

```
(>=>) :: Monad m => (a -> m b) -> (b -> m c) -> a -> m c
f >=> g = \x -> f x >>= g
```

Using this function the laws become simply the monoid laws:

```
return >=> f = f
f >=> return = f
(f >=> g) >=> h = f >=> (g >=> h)
```

There are also a few laws relating `Monad`

to `Applicative`

and `Functor`

:

```
f <$> a = f `liftM` a
return = pure
(<*>) = ap
```

As with the `Functor`

, the `Monad`

instance just delegates the work:

```
instance MonadConc m => Monad (Concurrently m) where
return = pure
Concurrently a >>= f = Concurrently $ a >>= runConcurrently . f
```

As these laws are mostly about function equality, a helper function to express that is used:

```
eqf :: Ord b => (a -> CST t b) -> (a -> CST t b) -> a -> Bool
eqf left right a = left a `eq` right a
```

Given that, the translation is simple:

```
prop_monad_left_id :: Ord b => Fun a (CST t b) -> a -> Bool
prop_monad_left_id (apply -> f) = f `eqf` (return >=> f)
prop_monad_right_id :: Ord b => Fun a (CST t b) -> a -> Bool
prop_monad_right_id (apply -> f) = f `eqf` (f >=> return)
prop_monad_comp :: Ord d => Fun a (CST t b) -> Fun b (CST t c) -> Fun c (CST t d) -> a -> Bool
prop_monad_comp (apply -> f) (apply -> g) (apply -> h) = ((f >=> g) >=> h) `eqf` (f >=> (g >=> h))
prop_monad_fmap :: Ord b => Fun a b -> CST t a -> Bool
prop_monad_fmap (apply -> f) a = (f <$> a) `eq` (f `liftM` a)
prop_monad_pure :: Ord a => a -> Bool
prop_monad_pure = pure `eqf` return
prop_monad_ap :: Ord b => Fun a b -> a -> Bool
prop_monad_ap (apply -> f) a = (pure f <*> pure a) `eq` (return f `ap` return a)
```

Are there any counterexamples? No there aren’t!

```
λ> quickCheck (prop_monad_left_id :: Fun Int (CST t String) -> Int -> Bool)
+++ OK, passed 100 tests.
λ> quickCheck (prop_monad_right_id :: Fun Int (CST t String) -> Int -> Bool)
+++ OK, passed 100 tests.
λ> quickCheck (prop_monad_comp :: Fun Int (CST t String) -> Fun String (CST t Bool) -> Fun Bool (CST t Int) -> Int -> Bool)
+++ OK, passed 100 tests.
λ> quickCheck (prop_monad_fmap :: Fun Int String -> CST t Int -> Bool)
+++ OK, passed 100 tests.
λ> quickCheck (prop_monad_pure :: Int -> Bool)
+++ OK, passed 100 tests.
λ> quickCheck (prop_monad_ap :: Fun Int String -> Int -> Bool)
+++ OK, passed 100 tests.
```

So, it certainly *looks* like all the laws hold! Yay!

## What about effects?

Consider the `eq'`

function. This sort of “value-level” equality is good enough for most types, where any type of effect is a value, but it doesn’t work so well when concurrency (or any sort of `IO`

) is involved, as there effects do not directly correspond to values.

There’s one type of effect we particularly care about for the case of `Concurrently`

: namely, the amount of concurrency going on! To test this, we need to write our tests such that different amounts of concurrency can produce different results, which means our current `Arbitrary`

instance for `Concurrently`

isn’t good enough. We need interaction between different concurrent inputs.

So let’s try writing a test case for the `(<*>) = ap`

law, but explicitly testing the amount of concurrency:

```
prop_monad_ap2 :: forall a b. Ord b => Fun a b -> Fun a b -> a -> Bool
prop_monad_ap2 (apply -> f) (apply -> g) a = go (<*>) `eq'` go ap where
go :: (CST t (a -> b) -> CST t a -> CST t b) -> ConcST t b
go combine = do
var <- newEmptyCVar
let cf = do { res <- tryTakeCVar var; pure $ if isJust res then f else g }
let ca = do { putCVar var (); pure a }
runConcurrently $ Concurrently cf `combine` Concurrently ca
```

Here we have two functions, `f`

and `g`

, and are using whether a `CVar`

is full or empty to choose between them. If the combining function executes its arguments concurrently, then we will see both cases; otherwise we’ll only see the `g`

case. *If* the law holds, and `(<*>) = ap`

, then we will see both cases for both of them!

```
λ> quickCheck (prop_monad_ap2 :: Fun Int String -> Fun Int String -> Int -> Bool)
*** Failed! Falsifiable (after 3 tests and 8 shrinks):
{_->""}
{_->"a"}
0
```

Oops! We found a counterexample! Let’s see what’s happening:

```
λ> results $ go (<*>) (\_ -> "") (\_ -> "a") 0
fromList [Right "",Right "a"]
λ> results $ go ap (\_ -> "") (\_ -> "a") 0
fromList [Right "a"]
```

If we look at the definition of `ap`

, the problem becomes clear:

```
ap :: Monad m => m (a -> b) -> m a -> m b
ap mf ma =
mf >>= \f ->
ma >>= \a ->
return (f a)
```

The issue is that our definiton of `(>>=)`

is *sequential*, whereas `(<*>)`

is *concurrent*. The `Monad`

instance is not consistent with that `Applicative`

*when there is interaction between actions*, as this shows!

So what’s the problem? It’s *close enough*, right? Well, close enough isn’t good enough, when it comes to laws. This very issue caused breakage, and is the reason that the `Monad`

instance for `Concurrently`

got removed!

## So what?

So what’s the point of this? Big deal, laws are important.

Well, that *is* the point. Laws *are* important, but often we don’t bother to test them. That’s possibly fine if the instances are simple, and you can check the laws by just juggling definitions in your head, but when `IO`

is involved, the situation becomes a bit more murky.

Code involving `IO`

and concurrency is easy to get wrong, so when building up a monad or whatever based on it, why not *actually test* the laws, rather than just assume they’re right? Because if, as a library author, your assumption is wrong, your users will suffer for it.