Is it possible for a non IO monad to violate Associativity in Haskell?

Question

I am new to Haskell and was trying to gain a better appreciation for the associative law for monads that states that:

m >>= (\x -> k x >>= h) = (m >>= k) >>= h

by trying to construct false monads that would violate this law. At a high level, this law appears to be enforcing associativity for application of "monadic functions" (not sure if there's a proper term) to me. In particular, it looked like it was enforcing some version of (f.g) x = f(g(x)), translated to monads.

However, if we consider f and g to be pure mathematical functions, then this relation appears to be trivially true. This led me to wonder if it was even possible to violate this law if IO was not involved, since to my basic understanding of Haskell at present, this would ensure that f and g have no side effects.

I was hoping if someone could elaborate on whether my general line of thought is correct, or if I have some key misconceptions, and it is possible to construct such a counterexample without the use of IO.

Answer 1

A standard example in our collective history is the ListT monad transformer, which is suprisingly difficult^* to get right. The wiki has a full discussion of what goes wrong with the obvious implementation and how to fix it, which I will excerpt here. It uses the following very plausible-looking "monad" instance:

newtype ListT m a = ListT { runListT :: m [a] }
instance (Monad m) => Monad (ListT m) where
    return a = ListT $ return [a]
    m >>= k  = ListT $ do
        a <- runListT m
        b <- mapM (runListT . k) a
        return (concat b)

instance (Monad m) => MonadPlus (ListT m) where
    mzero       = ListT $ return []
    m `mplus` n = ListT $ do
        a <- runListT m
        b <- runListT n
        return (a ++ b)

And here's the counterexample to it being associative:

a,b,c :: ListT IO ()
[a,b,c] = map (liftIO . putChar) ['a','b','c']

t1 :: ListT IO ()
t1 = ((a `mplus` a) >> b) >> c

t2 :: ListT IO ()
t2 = (a `mplus` a) >> (b >> c)

...running runListT t1 prints "aabbcc", while runListT t2 instead prints "aabcbc".

This particular example happens to use IO, but it's not fundamental; we could as well use ListT (Writer String) as the "monad" and tell instead of putChar.

^*This difficulty has led us to have an enormous family of closely-related libraries; the family includes list-t, logict, iteratee, machines, pipes, conduit, and streamly.

Answer 2

As Carl mentioned in a comment, the pure equivalent of the associativity law¹ is:

f . (g . h) = (f . g) . h

And the monadic associativity law is much more obviously related when phrased this way²:

f <=< (g <=< h) = (f <=< g) <=< h

In this form f, g, and h are all what is called "Kleisi arrows", which means they are functions with a type like a -> m b (for some a, m, and b; you don't have to be polymorphic to be a Kleisi arrow). The arrow (or "fish") operator³ is known as "Kleisi composition", and is a perfect monadic analogue to normal function composition.

(.)   :: (b ->   c) -> (a ->   b) -> (a ->   c)
(<=<) :: (b -> m c) -> (a -> m b) -> (a -> m c)

Now, as you noted, the associativity law is "trivially true" for pure functions. But that is because there is just one function composition operator ., and it is in fact associative! Associativity is a property of the operator, not the functions; any operator ⊕ is associative if and only if f ⊕ (g ⊕ h) = (f ⊕ g) ⊕ h for all possible f, g, and h. With pure composition we're only considering one operator ., so there's no "search space" to explore looking for how pure composition could be non-associative.

But each individual monad has its own definition of <=< (via the definition of >>= in the Monad instance), so the question looks more interesting. In fact, the monad associativity law is a bit of a different beast from the associativity property of .. Associativity of . is just a fact. The monad associativity law, to a Haskell programmer, is an obligation, not a mathematical truth⁴. It's something we have to make sure we stick to when writing a Monad instance.

---

Now, lets try to break it by constructing a counter-example. We want some false monad M, such that for some f, g, and h:

f <=< (g <=< h) ≠ (f <=< g) <=< h

Since both sides of our inequality are functions, we can show they're not equal by finding some value for which the functions produce different results. i.e. what we actually want is (for some f, g, h, and x):

(f <=< (g <=< h)) x ≠ ((f <=< g) <=< h) x

And as a reminder, the types of the things involved will be:

x :: z
h :: z -> M a
g :: a -> M b
f :: b -> M c

Now, if our "monad" M were just a boring wrapper of a single value (data M a = M a) then <=< would end up behaving just like . (just with extra wrapping and unwrapping), but we know that . is associative, so we're not going to be able to come up with a counter example like that.

Our M needs more structure than that if we're going to break associativity of <=<. So let's try something like data M a = M a Integer, the type of values that come along with an extra integer on the side.

So our <=< operator definition is going have to be something of this form⁵:

(<=<) :: (b -> M c) -> (a -> M b) -> (a -> M c)
f <=< g
  = \a -> let M b gInt = g a
              M c fInt = f b
           in M c (fInt ⊕ gInt)

Where ⊕ can be any Integer -> Integer -> Integer function we like⁶!

So with those choices made, lets see if we can crunch our original inequation a bit. Left hand side:

(f <=< (g <=< h)) x

-- apply definition of <=< to outer expression
= (\a -> let M b ghInt = (g <=< h) a
             M c fInt = f b
          in M c (fInt ⊕ ghInt)) x

-- apply lambda to x
= let M b ghInt = (g <=< h) x
      M c fInt = f b
   in M c (fInt ⊕ ghInt)

-- apply definition of <=< to inner expression
= let M b ghInt = (\a' -> let M b' hInt = h a'
                              M c' gInt = g b'
                           in M c' (gInt ⊕ hInt))  x
      M c fInt = f b
   in M c (fInt ⊕ ghInt)

-- apply lambda to x
= let M b ghInt = let M b' hInt = h x
                      M c' gInt = g b'
                   in M c' (gInt ⊕ hInt))
      M c fInt = f b
   in M c (fInt ⊕ ghInt)

-- move inner let bindings to outer let
= let M b' hInt = h x
      M c' gInt = g b'
      M b ghInt = M c' (gInt ⊕ hInt))
      M c fInt = f b
   in M c (fInt ⊕ ghInt)

-- since M b ghInt = M c' (gInt ⊕ hInt), apply b = c' and ghInt = (gInt ⊕ hInt)
= let M b' hInt = h x
      M c' gInt = g b'
      M c fInt = f c'
   in M c (fInt ⊕ (gInt ⊕ hInt))

-- rename b' -> a, c' -> b, for ease of reading
= let M a hInt = h x
      M b gInt = g a
      M c fInt = f b
   in M c (fInt ⊕ (gInt ⊕ hInt))

Now lets try the right hand side of our inequality:

((f <=< g) <=< h) x

-- apply definition of <=< to outer expression
= (\a -> let M b hInt = h a
             M c fgInt = (f <=< g) b
          in M c (fgInt ⊕ hInt)) x

-- apply lambda to x
= let M b hInt = h x
      M c fgInt = (f <=< g) b
   in M c (fgInt ⊕ hInt)

-- apply definition of <=< to inner expression
= let M b hInt = h x
      M c fgInt = (\a' -> let M b' gInt = g a'
                              M c' fInt = f b'
                           in M c' (fInt ⊕ gInt)) b
   in M c (fgInt ⊕ hInt)

-- apply lambda to b
= let M b hInt = h x
      M c fgInt = let M b' gInt = g b
                      M c' fInt = f b'
                   in M c' (fInt ⊕ gInt)
   in M c (fgInt ⊕ hInt)

-- move inner let bindings to outer let
= let M b hInt = h x
      M b' gInt = g b
      M c' fInt = f b'
      M c fgInt = M c' (fInt ⊕ gInt)
   in M c (fgInt ⊕ hInt)

-- since M c fgInt = M c' (fInt ⊕ gInt), apply c = c' and fgInt = (fInt ⊕ gInt)
= let M b hInt = h x
      M b' gInt = g b
      M c' fInt = f b'
   in M c' ((fInt ⊕ gInt) ⊕ hInt)

-- rename b -> a, b' -> b, and c' -> c, for ease of reading
= let M a hInt = h x
      M b gInt = g a
      M c fInt = f b
   in M c ((fInt ⊕ gInt) ⊕ hInt)

So putting both sides together, we have wound up with:

let M a hInt = h x
    M b gInt = g a
    M c fInt = f b
 in M c (fInt ⊕ (gInt ⊕ hInt))
≠
let M a hInt = h x
    M b gInt = g a
    M c fInt = f b
 in M c ((fInt ⊕ gInt) ⊕ hInt)

Compare carefully and you'll see that everything has ended exactly the same except for the second parameter of the final M (the "integer on the side"). And this was all regardless of what particular choices are made for f, g, h, and x (or indeed, what their types are); it turns out we don't need to know, our M and <=< definitions produced this form regardless. (You should be able to see what I meant about if we just wrapped a single value, as in data M a = M a; the types force us to be associative in that case, since we end up just implementing something that works the same as the pure composition . operator)

We hadn't actually decided what the ⊕ operation was yet, but the comparison fInt ⊕ (gInt ⊕ hInt) vs (fInt ⊕ gInt) ⊕ hInt is just the definition of associativity again! So all we need for our inequality to hold (and thus for M's <=< to be non-associative) is any non-associative operator on integers. Subtraction and division both are non-associative; I'm sure you can come up with countless others.

So it's actually pretty difficult for a proposed monad of this form⁷ (a value with an extra integer on the side) to pass the associativity requirement; we have to carefully make sure we combine the integers in an associative way (because there are plenty of non-associative integer operations). Any non-associative operation will give rise to a false monad of this form.

Obviously types that can be monads come in a huge variety of forms, I just leapt for a very simple one for the sake of finding a single simple counterexample (and actually found a whole family of them). But what we've found for this form does apply more generally; associativity of <=< doesn't just happen automatically when you're writing a Monad instance, you do have to carefully make sure it holds. It is very possible (and quite easy) to violate this law. Associativity does often fall out quite naturally from the types, which can deceive you into thinking that it will always hold, but that isn't the case.

---

¹ Rather than (f.g) x = f(g(x)), as guessed in the question.

² The law stated in terms of the >>= operator you use to directly make a Monad instance is: m >>= (\x -> k x >>= h) = (m >>= k) >>= h, which is equivalent but looks a bit klunkier due to need to explicitly write a lambda.

³ You can use this <=< operator in your Haskell code; it's in Control.Monad.

⁴ As programmers, we make monad associativity obligatory because associativity of monads is actually a mathematical fact. In maths, if the <=< operator for what you're looking at isn't associative it simply shows that what you have isn't a monad. In Haskell, nothing stops you from coding a Monad instance but defining >>= in such a way that <=< isn't associative. But we want to use theories from mathematical monads to write generic code that works for all Monads; the associativity obligation is what ensures our Monads are also mathematical monads.

⁵ Which implies that >>= in the Monad instance must have looked like:

(M x i) >>= f
  = let M y j = f x
     in M y (j ⊕ i)

⁶ Hopefully you can see that the a, b, and c have to go where they do because <=< is polymorphic, and has no other way to get a value of type c for the final result, but the fInt and gInt values are known to be Integer so we can do whatever we like with them; we can even just make up an arbitrary return value by choosing something like _ ⊕ _ = 37.

⁷ You may have noticed that this form is pretty much exactly the form of the Writer monad, only I've locked down the "log" value to be Integer instead of leaving it as a type parameter. I didn't actually need to do that, since I also didn't use any properties of Integer (beyond the existence of non-associative operations) I just wanted to avoid adding more variables! But that is exactly why the Writer monad instance has a Monoid constraint on the log value; it needs to know an associative operation for combining log values, in order to pass the associativity requirement for monads (as well as needing something like mempty to "initialise" the log value in pure/return).