Concurrency and Typeclass Laws

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.