Concurrency and Typeclass Laws

Date
Tags dejafu, haskell, programming, semantics
Target Audience Haskell programmers.
Attention Conservation Notice By calling dejafu from within a property test, we can check laws of classes which do concurrency.

Note: This is using (at the time of writ­ing) the latest de­vel­op­mental ver­sion of Deja Fu, which is not yet on hack­age. It will be soon! But until then, if you want to rep­licate this, clone from git.

I re­cently im­ple­mented asyn­c-de­jafu, a ver­sion of the async lib­rary using Deja Fu so pro­grams written with it can be tested, and I was curious about checking the rel­evant type­class laws auto­mat­ic­ally.

Checking type­class laws has been done with QuickCheck be­fore, but the dif­fer­ence here is that async uses con­cur­rency! If only we had some way to test con­cur­rent Haskell code! Oh, wait…

The set-up

Spe­cific­ally, I want to test the laws for the Con­cur­rently type. Con­cur­rently is a monad for ex­pressing IO ac­tions which should be run con­cur­rently.

Firstly, we need some lan­guage ex­ten­sions and im­ports:

{-# LAN­GUAGE RankN­Types          #-}
{-# LAN­GUAGE Scoped­TypeVari­ables #-}
{-# LAN­GUAGE ViewPat­terns        #-}

module Con­cur­rently where

im­port Con­trol.Ap­plic­ative
im­port Con­trol.Ex­cep­tion (SomeEx­cep­tion)
im­port Con­trol.­Monad ((>=>), ap, liftM, forever)
im­port Con­trol.­Mon­ad.Catch (onEx­cep­tion)
im­port Con­trol.­Mon­ad.­Con­c.­Class
im­port Data.Maybe (is­Just)
im­port Data.Set (Set, from­List)
im­port Test.De­jaFu (Failure(..), de­fault­Mem­Type)
im­port Test.De­jaFu.­De­term­in­istic (ConcST, Trace)
im­port Test.De­jaFu.SCT (sct­Bound, de­fault­Bounds)
im­port Test.QuickCheck (Ar­bit­rary(..))
im­port Test.QuickCheck­.­Func­tion (Fun, apply)
im­port Un­safe.­Co­erce (un­sa­fe­Co­erce)

I have sadly not man­aged to elim­inate that un­sa­fe­Co­erce, it shows up be­cause 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 Con­cur­rently type. The ori­ginal just uses IO, so we have to para­met­erise ours over the un­der­lying monad:

new­type Con­cur­rently m a = Con­cur­rently { run­Con­cur­rently :: m a }

We’ll also be using a ConcST variant for testing a lot, so here’s a type syn­onym for that:

type CST t = Con­cur­rently (ConcST t)

We also need some in­stances for Con­cur­rently in order to make QuickCheck happy, but these aren’t ter­ribly im­port­ant:

in­stance Show (Con­cur­rently m a) where
  show _ = "<­con­cur­rently>"

in­stance (Ar­bit­rary a, Ap­plic­ative m) => Ar­bit­rary (Con­cur­rently m a) where
  ar­bit­rary = Con­cur­rently . pure <$> ar­bit­rary

Ok, let’s get star­ted!

Functor

Functor lets you apply a pure func­tion to a value in a con­text.

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

A Functor should sat­isfy the iden­tity law:

fmap id = id

And the com­pos­i­tion law:

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

The Functor in­stance for Con­cur­rently just del­eg­ates the work to the in­stance for the un­der­lying monad:

in­stance Mon­ad­Conc m => Functor (Con­cur­rently m) where
  fmap f (Con­cur­rently a) = Con­cur­rently $ f <$> a

The com­pos­i­tion law is a little awk­ward to ex­press in a way that QuickCheck can deal with, as it in­volves ar­bit­rary func­tions. QuickCheck has a Fun type, rep­res­enting func­tions which can be seri­al­ised to a string. Bearing that in mind, here is how we can ex­press those two laws as tests:

prop_­func­tor_id :: Ord a => CST t a -> Bool
prop_­func­tor_id ca = ca `eq` (id <$> ca)

prop_­func­tor_­comp :: Ord c => CST t a -> Fun a b -> Fun b c -> Bool
prop_­func­tor_­comp ca (apply -> f) (apply -> g) = (g . f <$> ca) `eq` (g <$> (f <$> ca))

We’re using view pat­terns here to ex­tract the ac­tual func­tion from the Fun value. let’s see if the laws hold!

λ> quickCheck (prop_­func­tor_id :: CST t Int -> Bool)
+++ OK, passed 100 tests.
λ> quickCheck (prop_­func­tor_­comp :: CST t Int -> Fun Int In­teger -> Fun In­teger String -> Bool)
+++ OK, passed 100 tests.

Cool! Wait, what’s that eq func­tion?

Equality and con­cur­rency?

I’ve de­cided to treat two con­cur­rent com­pu­ta­tions as equal if the sets of values that they can pro­duce are equal:

eq :: Ord a => CST t a -> CST t a -> Bool
eq left right = run­Con­cur­rently left `eq'` run­Con­cur­rently right

eq' :: forall t a. Ord a => ConcST t a -> ConcST t a -> Bool
eq' left right = res­ults left == res­ults right where
  res­ults cst = from­List . map fst $ sct­Bound' cst

  sct­Bound' :: ConcST t a -> [(Either Failure a, Trace)]
  sct­Bound' = un­sa­fe­Co­erce $ sct­Bound de­fault­Mem­Type de­fault­Bounds

This is where the un­for­tu­nate un­sa­fe­Co­erce comes in. The defin­i­tion of sct­Bound' there doesn’t type-check without it, which is a shame. If anyone could offer a solu­tion, I would be very grate­ful.

Ap­plic­ative

Ap­plic­ative ex­tends Functor with the ability to in­ject a value into a con­text without in­tro­du­cing any ef­fects, and to apply a func­tion in a con­text to a value in a con­text.

class Functor f => Ap­plic­ative f where
  pure  :: a -> f a
  (<*>) :: f (a -> b) -> f a -> f b

An Ap­plic­ative should sat­isfy the iden­tity law:

pure id <*> a = a

The ho­mo­morphism law, which says that ap­plying a pure func­tion to a pure value in a con­text is the same as just ap­plying the func­tion to the value and in­jecting the en­tire result into a con­text:

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

The in­ter­change law, which says that when ap­plying a func­tion in a con­text to a pure value, the order in which each is eval­u­ated doesn’t mat­ter:

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

And the com­pos­i­tion law, which is a sort of as­so­ci­ativity prop­erty:

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

Fi­nally, there is a law re­lating Ap­plic­ative to Functor, that says we can de­com­pose fmap into two steps, in­jecting a func­tion into a con­text, and then ap­plic­a­tion within that con­text:

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

This is where Con­cur­rently gets its con­cur­rency. (<*>) runs its two ar­gu­ments con­cur­rently, killing the other if one throws an ex­cep­tion.

in­stance Mon­ad­Conc m => Ap­plic­ative (Con­cur­rently m) where
  pure = Con­cur­rently . pure

  Con­cur­rently fs <*> Con­cur­rently as = Con­cur­rently $
    (\(f, a) -> f a) <$> con­cur­rently fs as

con­cur­rently :: Mon­ad­Conc m => m a -> m b -> m (a, b)
con­cur­rently = ...

Armed with the know­ledge of how to gen­erate ar­bit­rary func­tions, these are all fairly straight-­for­ward to test

prop_ap­plic­at­ive_id :: Ord a => CST t a -> Bool
prop_ap­plic­at­ive_id ca = ca `eq` (pure id <*> ca)

prop_ap­plic­at­ive_homo :: Ord b => a -> Fun a b -> Bool
prop_ap­plic­at­ive_homo a (apply -> f) = (pure $ f a) `eq` (pure f <*> pure a)

prop_ap­plic­at­ive_inter :: Ord b => CST t (Fun a b) -> a -> Bool
prop_ap­plic­at­ive_inter u y = (u' <*> pure y) `eq` (pure ($ y) <*> u') where
  u' = apply <$> u

prop_ap­plic­at­ive_­comp :: Ord c => CST t (Fun b c) -> CST t (Fun a b) -> CST t a -> Bool
prop_ap­plic­at­ive_­comp u v w = (u' <*> (v' <*> w)) `eq` (pure (.) <*> u' <*> v' <*> w) where
  u' = apply <$> u
  v' = apply <$> v
 
prop_ap­plic­at­ive_fmap :: Ord b => Fun a b -> CST t a -> Bool
prop_ap­plic­at­ive_fmap (apply -> f) a = (f <$> a) `eq` (pure f <*> a)

And in­deed we see that the laws hold:

λ> quickCheck (prop_ap­plic­at­ive_id :: CST t Int -> Bool)
+++ OK, passed 100 tests.
λ> quickCheck (prop_ap­plic­at­ive_homo :: String -> Fun String Int -> Bool)
+++ OK, passed 100 tests.
λ> quickCheck (prop_ap­plic­at­ive_inter :: CST t (Fun Int String) -> Int -> Bool)
+++ OK, passed 100 tests.
λ> quickCheck (prop_ap­plic­at­ive_­comp :: CST t (Fun Int String) -> CST t (Fun Char Int) -> CST t Char -> Bool)
+++ OK, passed 100 tests.
λ> quickCheck (prop_ap­plic­at­ive_fmap :: Fun Int String -> CST t Int -> Bool)
+++ OK, passed 100 tests.

Al­tern­ative

Al­tern­ative is a kind of monoid over Ap­plic­ative.

class Ap­plic­ative f => Al­tern­ative f where
  empty :: f a
  (<|>) :: f a -> f a -> f a
  
  -- These both have de­fault defin­i­tions
  some :: f a -> f [a]
  many :: f a -> f [a]

An Al­tern­ative should sat­isfy the monoid laws. Namely, left and right iden­tity:

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

And as­so­ci­ativ­ity:

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

The Al­tern­ative in­stance for Con­cur­rently is used to ex­press races, with (<|>) ex­ecuting both of its ar­gu­ments con­cur­rently and re­turning the first to fin­ish:

in­stance Mon­ad­Conc m => Al­tern­ative (Con­cur­rently m) where
  empty = Con­cur­rently $ forever yield

  Con­cur­rently as <|> Con­cur­rently bs =
    Con­cur­rently $ either id id <$> race as bs

race :: Mon­ad­Conc m => m a -> m b -> m (Either a b)
race = ...

Once again, the trans­la­tion into QuickCheck prop­er­ties is quite sim­ple:

prop_al­tern­at­ive_right_id :: Ord a => CST t a -> Bool
prop_al­tern­at­ive_right_id x = x `eq` (x <|> empty)

prop_al­tern­at­ive_left_id :: Ord a => CST t a -> Bool
prop_al­tern­at­ive_left_id x = x `eq` (empty <|> x)

prop_al­tern­at­ive_assoc :: Ord a => CST t a -> CST t a -> CST t a -> Bool
prop_al­tern­at­ive_assoc x y z = (x <|> (y <|> z)) `eq` ((x <|> y) <|> z)

And the laws hold!

λ> quickCheck (prop_al­tern­at­ive_right_id :: CST t Int -> Bool)
+++ OK, passed 100 tests.
λ> quickCheck (prop_al­tern­at­ive_left_id :: CST t Int -> Bool)
+++ OK, passed 100 tests.
λ> quickCheck (prop_al­tern­at­ive_assoc :: CST t Int -> CST t Int -> CST t Int -> Bool)
+++ OK, passed 100 tests.

There are also some laws re­lating Al­tern­ative to Ap­plic­ative, but these are ex­pressed in terms of some and many, which have de­fault law-sat­is­fying defin­i­tions.

Monad

Monad ex­tends Ap­plic­ative with the ability to squash nested mon­adic values to­gether, and are com­monly used to ex­press se­quen­cing.

class Ap­plic­ative m => Monad m where
  re­turn :: a -> m a
  (>>=)  :: m a -> (a -> m b) -> m b

There are a few dif­ferent for­mu­la­tions of the Monad laws, I prefer the one in terms of (>=>) (the fish op­er­at­or), which is defined as:

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

Using this func­tion the laws be­come simply the monoid laws:

re­turn >=> f = f
f >=> re­turn = f
(f >=> g) >=> h = f >=> (g >=> h)

There are also a few laws re­lating Monad to Ap­plic­ative and Functor:

f <$> a = f `liftM` a
re­turn = pure
(<*>) = ap

As with the Functor, the Monad in­stance just del­eg­ates the work:

in­stance Mon­ad­Conc m => Monad (Con­cur­rently m) where
  re­turn = pure

  Con­cur­rently a >>= f = Con­cur­rently $ a >>= run­Con­cur­rently . f

As these laws are mostly about func­tion equal­ity, a helper func­tion to ex­press 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 trans­la­tion is sim­ple:

prop_­mon­ad_left_id :: Ord b => Fun a (CST t b) -> a -> Bool
prop_­mon­ad_left_id (apply -> f) = f `eqf` (re­turn >=> f)

prop_­mon­ad_right_id :: Ord b => Fun a (CST t b) -> a -> Bool
prop_­mon­ad_right_id (apply -> f) = f `eqf` (f >=> re­turn)

prop_­mon­ad_­comp :: Ord d => Fun a (CST t b) -> Fun b (CST t c) -> Fun c (CST t d) -> a -> Bool
prop_­mon­ad_­comp (apply -> f) (apply -> g) (apply -> h) = ((f >=> g) >=> h) `eqf` (f >=> (g >=> h))

prop_­mon­ad_fmap :: Ord b => Fun a b -> CST t a -> Bool
prop_­mon­ad_fmap (apply -> f) a = (f <$> a) `eq` (f `liftM` a)

prop_­mon­ad_pure :: Ord a => a -> Bool
prop_­mon­ad_pure = pure `eqf` re­turn

prop_­mon­ad_ap :: Ord b => Fun a b -> a -> Bool
prop_­mon­ad_ap (apply -> f) a = (pure f <*> pure a) `eq` (re­turn f `ap` re­turn a)

Are there any counter­examples? No there aren’t!

λ> quickCheck (prop_­mon­ad_left_id :: Fun Int (CST t String) -> Int -> Bool)
+++ OK, passed 100 tests.
λ> quickCheck (prop_­mon­ad_right_id :: Fun Int (CST t String) -> Int -> Bool)
+++ OK, passed 100 tests.
λ> quickCheck (prop_­mon­ad_­comp :: Fun Int (CST t String) -> Fun String (CST t Bool) -> Fun Bool (CST t Int) -> Int -> Bool)
+++ OK, passed 100 tests.
λ> quickCheck (prop_­mon­ad_fmap :: Fun Int String -> CST t Int -> Bool)
+++ OK, passed 100 tests.
λ> quickCheck (prop_­mon­ad_pure :: Int -> Bool)
+++ OK, passed 100 tests.
λ> quickCheck (prop_­mon­ad_ap :: Fun Int String -> Int -> Bool)
+++ OK, passed 100 tests.

So, it cer­tainly looks like all the laws hold! Yay!

What about ef­fects?

Con­sider the eq' func­tion. This sort of “value-­level” equality is good enough for most types, where any type of ef­fect is a value, but it doesn’t work so well when con­cur­rency (or any sort of IO) is in­volved, as there ef­fects do not dir­ectly cor­res­pond to val­ues.

There’s one type of ef­fect we par­tic­u­larly care about for the case of Con­cur­rently: namely, the amount of con­cur­rency going on! To test this, we need to write our tests such that dif­ferent amounts of con­cur­rency can pro­duce dif­ferent res­ults, which means our cur­rent Ar­bit­rary in­stance for Con­cur­rently isn’t good enough. We need in­ter­ac­tion between dif­ferent con­cur­rent in­puts.

So let’s try writing a test case for the (<*>) = ap law, but ex­pli­citly testing the amount of con­cur­rency:

prop_­mon­ad_ap2 :: forall a b. Ord b => Fun a b -> Fun a b -> a -> Bool
prop_­mon­ad_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 com­bine = do
    var <- newEmptyCVar
    let cf = do { res <- tryTakeCVar var; pure $ if is­Just res then f else g }
    let ca = do { putCVar var (); pure a }
    run­Con­cur­rently $ Con­cur­rently cf `com­bine` Con­cur­rently ca

Here we have two func­tions, f and g, and are using whether a CVar is full or empty to choose between them. If the com­bining func­tion ex­ecutes its ar­gu­ments con­cur­rently, then we will see both cases; oth­er­wise 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_­mon­ad_ap2 :: Fun Int String -> Fun Int String -> Int -> Bool)
*** Failed! Falsifi­able (after 3 tests and 8 shrinks):    
{_->""}
{_->"a"}
0

Oops! We found a counter­example! Let’s see what’s hap­pen­ing:

λ> res­ults $ go (<*>) (\_ -> "") (\_ -> "a") 0
from­List [Right "",Right "a"]
λ> res­ults $ go ap (\_ -> "") (\_ -> "a") 0
from­List [Right "a"]

If we look at the defin­i­tion of ap, the problem be­comes clear:

ap :: Monad m => m (a -> b) -> m a -> m b
ap mf ma =
  mf >>= \f ->
  ma >>= \a ->
  re­turn (f a)

The issue is that our definiton of (>>=) is se­quen­tial, whereas (<*>) is con­cur­rent. The Monad in­stance is not con­sistent with that Ap­plic­ative when there is in­ter­ac­tion between ac­tions, as this shows!

So what’s the prob­lem? 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 in­stance for Con­cur­rently got re­moved!

So what?

So what’s the point of this? Big deal, laws are im­port­ant.

Well, that is the point. Laws are im­port­ant, but often we don’t bother to test them. That’s pos­sibly fine if the in­stances are sim­ple, and you can check the laws by just jug­gling defin­i­tions in your head, but when IO is in­volved, the situ­ation be­comes a bit more murky.

Code in­volving IO and con­cur­rency is easy to get wrong, so when building up a monad or whatever based on it, why not ac­tu­ally test the laws, rather than just as­sume they’re right? Be­cause if, as a lib­rary au­thor, your as­sump­tion is wrong, your users will suffer for it.