Monadic Sequencing and the Encoding of Effects

An expression that prints a line and returns a number is not a number. If it were, the substitution property would fail for it, and every optimization that duplicates or reorders expressions would be unsound. The monadic encoding resolves this by making the effectful expression a value that describes an action, and by making the composition of such descriptions an ordinary function application. The program is pure; the action it denotes is not.

A value that describes rather than performs

The type constructor separates the description from the result. For a computation that may perform effects of type e and produce a value of type a, the type is written m a, and the two operations are

return :: a -> m a
(>>=)  :: m a -> (a -> m b) -> m b

return lifts a plain value into a computation that does nothing. >>= takes a computation, waits for its result, and passes that result to a function that produces the next computation. Neither operation performs anything: return 3 is a description, and readFile "x" >>= \s -> return (length s) is a description of a description.

The concrete instance for I/O makes this explicit. A value of type IO a is traditionally explained as a state transformer over the real world, or equivalently a function from a world token to a pair of a result and a new world. The token is never produced by the program, the world is not copyable, and the only operation that touches it is the one that sequences two actions, >>=. That is the whole content of the “IO is a state monad” explanation, and it is the reason a value of type IO a can be named, stored, and passed to a combinator such as forever or replicateM_ without changing what it means: forever getLine reads lines until something throws, because one stored description is run repeatedly, not because the expression was re-executed at each step.

The state-monad reading is a useful model and not the implementation. GHC’s IO is a primitive type with primitive operations, and the state-passing story is an explanation of why the sequencing discipline is sound rather than a description of the runtime representation. The distinction matters when reasoning about performance: an IO action does not allocate a world token.

Bind as the only sequencing primitive

Every monad has the same shape, and the shape determines what “sequencing” means.

Maybe. Nothing >>= f = Nothing, and Just x >>= f = f x. Sequencing short-circuits on the first failure, and the computation after the failure is never run. This is the monadic encoding of exceptions without a control-flow primitive.

Either e. The same, with the failure carrying a value of type e. The difference from Maybe is that the short-circuit can report why, and the cost is the extra payload on every failure.

List. xs >>= f = concatMap f xs. Sequencing means “for each result of the first computation, run the second and collect all results”. This is the encoding of non-determinism, and the length of the result is the product of the branching factors.

Reader r. f >>= g = \r -> g (f r) r. Sequencing threads a shared environment. The environment is read-only by construction, because there is no operation that writes it.

State s. f >>= g = \s -> let (a, s') = f s in g a s'. Sequencing threads a mutable state, and the state is threaded in the type so that no two branches can observe each other’s writes.

Writer w. Sequencing accumulates a log by appending. The monoid instance on w decides whether the log is a list, a count, or something with a cheaper append.

The important observation is that the six instances have the same type signature and different behaviour, and that the type signature alone does not determine the behaviour. Maybe and Either e have the same shape of short-circuit and differ in what they carry. List and Writer [a] both accumulate, and differ in whether the accumulation is a result or a side channel. This is why the monad abstraction covers so much ground and why it is not a specification: a function polymorphic in m can use only return and >>=, and what those mean is decided at the call site.

The laws, and what they are for

Three equations define a lawful monad:

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

The first two say that return is a unit for sequencing on both sides. The third says that sequencing associates. Together they say that a chain of binds is a list of steps with a well-defined order and no dependence on parenthesization.

The laws are not checked by the compiler and not enforced by the type. A type with the right signatures and the wrong behaviour is a monad by type and not by law, and code written against it will still compile. What the laws buy is the ability to reason: a do block can be read as a sequence of steps, a helper function can be lifted into the chain without changing its meaning, and a refactoring that groups two steps is meaning-preserving. Without the laws those rewrites are guesses.

The laws also constrain the implementation in ways that are easy to miss. The second law requires that a computation rebound with return is indistinguishable from the original, so a >>= that transforms the value it was given into something else, or that records the fact that a bind happened, fails it; this is the sense in which a monad is not an instrumentation hook. The third law rules out a >>= that treats a bind of a bind differently from a flattened one, so a bind cannot count the number of steps in the chain.

Do-notation is a surface form

The do syntax desugars to binds and lambdas:

do x <- m1
   y <- m2 x
   return (x + y)

-- desugars to
m1 >>= \x -> m2 x >>= \y -> return (x + y)

The desugaring is mechanical and complete: every do block is a nested chain of >>= and return, with >> as the variant that discards a result and let as a pure binding. A pattern that may fail desugars to a case expression whose fall-through calls the monad’s fail, drawn from the MonadFail class since that class was separated from Monad; that is why a do block whose pattern does not refute can fail at run time in some monads and not in others, and why a Monad instance without a MonadFail instance rejects such a block at compile time.

The syntax is not part of the abstraction. A language can have the monad without the sugar, and many do; the sugar is what makes the encoding usable at scale, because a chain of twenty binds written with explicit lambdas nests twenty levels deep. The alternative encoding is the applicative one, where <*> sequences two computations without letting the second depend on the first’s result; the monad is what allows the dependence, and that dependence is exactly the extra power.

Why the abstraction is not free

The first cost is that a monadic program is written in a style that has no direct analogue in a language without the type constructor. A function that returns IO a cannot be called from a pure context and cannot be optimized across the boundary: the compiler must preserve the order of the actions, which is exactly the constraint that purity was supposed to remove. Inside the monad, the optimizer’s freedom is the same as in an impure language, and the purity is on the outside.

The second cost is the IO boundary itself. A function that mixes pure computation and I/O must either return IO or be split into a pure part and an IO part. The split is usually the right design and is also the source of the “monad transformers” complexity, because two effects that must compose need a combined monad, and the combination is a stack of transformers with a lift at every boundary.

The third cost is performance. A bind is a function call, and a chain of binds is a chain of calls that the compiler must inline to recover the loop. GHC’s optimizer does this for the common monads through the Monad instance’s unfolding and the do desugaring, and a monad implemented behind an abstract interface in another module may not inline. The result is that a hand-written recursive loop over a list can be faster than the equivalent forM_ chain, and the difference is entirely in whether the bind inlined.

The relationship to effects as a language feature

The monadic encoding is one answer to the question of how to add effects to a pure language. Its distinguishing property is that effects are values, so they can be passed, returned, stored, and interpreted by a handler the programmer writes. A program can then be recorded as a tree of requests and interpreted later, which is what free monads provide. The alternative is to make effects a primitive of the language with a handler construct, which is what algebraic effect systems do.

The monadic answer’s cost is that composition of effects requires composing the types, and the type-level composition is where the complexity lives. The primitive answer’s cost is that the language must define the handler semantics and the type-and-effect system, and the programmer cannot invent a new effect without changing the language. Both are responses to the same constraint, which is that referential transparency must be preserved at the boundary between pure and effectful code.

The other point worth keeping is that the monad is a sequencing abstraction, not an effect abstraction. It says how computations compose; it does not say what they do. That is why the same interface covers non-determinism, state, failure, logging, and I/O, and why a monad alone cannot tell a caller which effects a computation performs. A type that tracks the effects, rather than the sequencing, is a different and stronger abstraction, and it is the reason effect systems exist.