A simple example showing that IO doesn't satisfy the monad laws?

Question

I've seen mentioned that IO doesn't satisfy the monad laws, but I didn't find a simple example showing that. Anybody knows an example? Thanks.

Edit: As ertes and n.m. pointed out, using seq is a bit illegal as it can make any monad fail the laws (combined with undefined). Since undefined may be viewed as a non-terminating computation, it's perfectly fine to use it.

So the revised question is: Anybody knows an example showing that IO fails to satisfy the monad laws, without using seq? (Or perhaps a proof that IO does satisfy the laws if seq is not allowed?)

Couldn't you use IO to edit the memory of the running program via external means and force a law to be broken? — Kendall Hopkins
@KendallHopkins Good idea. Another idea (perhaps simpler) could be to exploit known problems of Haskell's lazy IO. — Petr
Is there a practical interest to show it without using seq? — gawi
@gawi The interest is mostly theoretical as any such example will very rarely occur in practical programming. The aim is to get detailed understanding of IO. — Petr

Daniel Fischer Daniel Fischer · Accepted Answer · 2012-09-27T14:14:08

tl;dr upfront: seq is the only way.

Since the implementation of IO is not prescribed by the standard, we can only look at specific implementations. If we look at GHC's implementation, as it is available from the source (it might be that some of the behind-the-scenes special treatment of IO introduces violations of the monad laws, but I'm not aware of any such occurrence),

-- in GHC.Types (ghc-prim)
newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #))

-- in GHC.Base (base)
instance  Monad IO  where
    {-# INLINE return #-}
    {-# INLINE (>>)   #-}
    {-# INLINE (>>=)  #-}
    m >> k    = m >>= \ _ -> k
    return    = returnIO
    (>>=)     = bindIO
    fail s    = failIO s

returnIO :: a -> IO a
returnIO x = IO $ \ s -> (# s, x #)

bindIO :: IO a -> (a -> IO b) -> IO b
bindIO (IO m) k = IO $ \ s -> case m s of (# new_s, a #) -> unIO (k a) new_s

thenIO :: IO a -> IO b -> IO b
thenIO (IO m) k = IO $ \ s -> case m s of (# new_s, _ #) -> unIO k new_s

unIO :: IO a -> (State# RealWorld -> (# State# RealWorld, a #))
unIO (IO a) = a

it's implemented as a (strict) state monad. So any violation of the monad laws IO makes, is also made by Control.Monad.State[.Strict].

Let's look at the monad laws and see what happens in IO:

return x >>= f ≡ f x:
return x >>= f = IO $ \s -> case (\t -> (# t, x #)) s of
                              (# new_s, a #) -> unIO (f a) new_s
               = IO $ \s -> case (# s, x #) of
                              (# new_s, a #) -> unIO (f a) new_s
               = IO $ \s -> unIO (f x) s

Ignoring the newtype wrapper, that means return x >>= f becomes \s -> (f x) s. The only way to (possibly) distinguish that from f x is seq. (And seq can only distinguish it if f x ≡ undefined.)

m >>= return ≡ m:
(IO k) >>= return = IO $ \s -> case k s of
                                 (# new_s, a #) -> unIO (return a) new_s
                  = IO $ \s -> case k s of
                                 (# new_s, a #) -> (\t -> (# t, a #)) new_s
                  = IO $ \s -> case k s of
                                 (# new_s, a #) -> (# new_s, a #)
                  = IO $ \s -> k s

ignoring the newtype wrapper again, k is replaced by \s -> k s, which again is only distinguishable by seq, and only if k ≡ undefined.

m >>= (\x -> g x >>= h) ≡ (m >>= g) >>= h:
(IO k) >>= (\x -> g x >>= h) = IO $ \s -> case k s of
                                            (# new_s, a #) -> unIO ((\x -> g x >>= h) a) new_s
                             = IO $ \s -> case k s of
                                            (# new_s, a #) -> unIO (g a >>= h) new_s
                             = IO $ \s -> case k s of
                                            (# new_s, a #) -> (\t -> case unIO (g a) t of
                                                                       (# new_t, b #) -> unIO (h b) new_t) new_s
                             = IO $ \s -> case k s of
                                            (# new_s, a #) -> case unIO (g a) new_s of
                                                                (# new_t, b #) -> unIO (h b) new_t
((IO k) >>= g) >>= h = IO $ \s -> case (\t -> case k t of
                                                (# new_s, a #) -> unIO (g a) new_s) s of
                                    (# new_t, b #) -> unIO (h b) new_t
                     = IO $ \s -> case (case k s of
                                          (# new_s, a #) -> unIO (g a) new_s) of
                                    (# new_t, b #) -> unIO (h b) new_t

Now, we generally have

case (case e of                    case e of
        pat1 -> ex1) of       ≡      pat1 -> case ex1 of
  pat2 -> ex2                                  pat2 -> ex2

per equation 3.17.3.(a) of the language report, so this law holds not only modulo seq.

Summarising, IO satisfies the monad laws, except for the fact that seq can distinguish undefined and \s -> undefined s. The same holds for State[T], Reader[T], (->) a, and any other monads wrapping a function type.

A simple example showing that IO doesn't satisfy the monad laws?

4 Answers