2

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:

Wadler's paper Associativity snippet

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):

  1. What is an example of an incorrect monad implementation, that looks correct but breaks associativity?
  2. How does this impact the do-notation?
  3. 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?
PhD
  • 11,202
  • 14
  • 64
  • 112

1 Answers1

6

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.

chi
  • 111,837
  • 3
  • 133
  • 218
  • This is useful. I am not very fluent in Haskell, only use it as a medium for understanding FP constructs. Could you please add some comments explaining what the Monad ListIO is trying to do? Also, why the need for nested `do`s? Perhaps some clarity on the latter would be helpful too. – PhD Mar 20 '20 at 08:51
  • @PhD You explicitly asked for `do` notation. You can rephrase that to `(a >> b) >> c` and `a >> (b >> c)`, which should be equal by associativity, and correspond to different `do` nestings. `ListIO` is trying to "compose" the IO monad (imperative-style side effects) and the `[]` monad (roughly, non-deterministic result). – chi Mar 20 '20 at 08:56
  • 1
    @PhD Roughly, this is trying to combine the IO monad (which you know) and the List monad (which runs a computation on several pieces of data at once, roughly), to produce a monad that can run an IO action on several pieces of data at once. If our data is [1,2,3] and for each piece of data we print "a" and print "b", should we get "ababab" or "aaabbb"? The List monad normally doesn't have this problem, because there are no side-effects in Haskell. – user253751 Mar 20 '20 at 11:39
  • @PhD nested `do`s are roughly analogous to anonymous code blocks in Java or other imperative language https://stackoverflow.com/questions/1563030/anonymous-code-blocks-in-java they can be a prelude to the common "extract method" refactoring. https://refactoring.guru/extract-method The associativity law must hold for that refactoring to be safe in Haskell. – danidiaz Mar 20 '20 at 14:17
  • @chi Are there any monad instances outside of ones with side effects that breaks associativity? It seems to me that law-violating instances of IO are almost trivial, since they can do just anything. This is a bit outside the scope of OP's question, but it would make a nice complement. – MikaelF Mar 21 '20 at 00:26
  • 1
    @MikaelF You could replace IO in the example above with `Writer String`, and `putStr` with `tell`, essentially memorizing all the outputs in a string. – chi Mar 21 '20 at 08:22