What is an example of an incorrect monad that violates the law of associativity?

Question

Background Context:

Mathematically, I can see the need for associativity to keep things simple without relying on order. All implementations of example monads that I've come across (blogs, books etc.,) seem to always work. It seems simply the act of having map, flatMap (Scala) or fmap, >>= (Haskell) makes things a working monad.

From what I gather this isn't entirely true, but can't come up with a counter example showing the "need" for the law via a failure case.

Wadler's paper mentions the possibility of an incorrect implementation:

The Haskell Wiki mentions the following:

The third law is a kind of associativity law for >>=. Obeying the three laws ensures that the semantics of the do-notation using the monad will be consistent.

Any type constructor with return and bind operators that satisfy the three monad laws is a monad. In Haskell, the compiler does not check that the laws hold for every instance of the Monad class. It is up to the programmer to ensure that any Monad instance they create satisfies the monad laws.

Question(s):

What is an example of an incorrect monad implementation, that looks correct but breaks associativity?
How does this impact the do-notation?
How does one validate the correctness of a monad implementation? Do we need to write test cases for each new monad, or a generic one can be written to check that any monad implementation is correct?

chi chi · Accepted Answer · 2020-03-20T07:51:10

Here's an example of non-monad which fails associativity:

{-# LANGUAGE DeriveFunctor #-}

import Control.Monad

newtype ListIO a = L { runListIO :: IO [a] }
  deriving Functor

instance Applicative ListIO where
   pure x = L $ return [x]
   (<*>) = ap

instance Monad ListIO where
   (L m) >>= f = L $ do
      xs <- m
      concat <$> mapM (runListIO . f) xs

If associativity were satisfied, these two do blocks would be equivalent

act1 :: ListIO Int
act1 = do
   L (pure [1,2,3])
   do L (putStr "a" >> return [10])
      L (putStr "b" >> return [7])

act2 :: ListIO Int
act2 = do
   do L (pure [1,2,3])
      L (putStr "a" >> return [10])
   L (putStr "b" >> return [7])

However, running the actions produces different outputs:

main :: IO ()
main = do
   runListIO act1 -- ababab
   putStrLn ""
   runListIO act2 -- aaabbb
   return ()

Validation of the associativity law can be hard, in general. One could write tests, sure, but the ideal way to ensure associativity would be to write a mathematical proof of the law. In some cases, equational reasoning suffices to prove associativity. Sometimes, we also need induction.

What is an example of an incorrect monad that violates the law of associativity?

1 Answers