โ† back to index

Monads

Bartosz Milewski ยท 2016-2017 ยท Category Theory for Programmers, Ch. 17

Prereqs: ๐Ÿž Ch4 (Kleisli Categories), ๐Ÿž Ch7 (Functors), ๐Ÿž Ch10 (Natural Transformations). 12 min.

A monad is a functor M equipped with two natural transformations: return (η : a → M(a)) and join (μ : M(M(a)) → M(a)). Equivalently, bind (>>=) replaces both. The monad laws (associativity, left/right identity) are the Kleisli category's composition laws. Monads compose effects: partiality, nondeterminism, logging, state.

Return and join: the categorical definition

A monad on a category C is an endofunctor M : C → C with two natural transformations: return (η : Id → M) embeds a pure value, and join (μ : M∘M → M) collapses a nested layer. The monad laws: join is associative, return is its two-sided identity. This is a wpmonoid in the category of endofunctors.

a M(a) M(M(a)) η (return) μ (join) return embeds, join collapses
Scheme

Bind: the programmer's interface

bind (>>=) takes a monadic value M(a) and a function a → M(b), and produces M(b). Equivalent to join composed with fmap: bind m f = join (fmap f m). Conversely, join = bind id. Bind is how programmers use monads: chain computations that produce effects.

a b c f : a → M(b) g : b → M(c) g >=> f : a → M(c)
Scheme

The monad laws

Three laws govern every monad. In terms of the fish operator (>=>, Kleisli composition): associativity (f >=> g) >=> h = f >=> (g >=> h), left identity return >=> f = f, right identity f >=> return = f. These are exactly the category axioms for the Kleisli category from Ch. 4.

Scheme

List monad: nondeterminism

The list monad models nondeterministic computation. return x = [x]. bind xs f = concat (map f xs). Each element spawns a list of possibilities; bind flattens them. This is the monad that arises from the free monoid adjunction (Ch. 16).

Scheme

Writer monad revisited

The Writer monad pairs a value with a log (any monoid). return x = (x, mempty). bind (a, w) f = let (b, w') = f a in (b, w <> w'). This is the monad from Ch. 4's Kleisli category, now with all three operations explicit. The tell function appends to the log without producing a value.

Scheme

Verifying the monad laws for Maybe

Every monad law is a testable property. Left identity: bind (return a) f = f a. Right identity: bind m return = m. Associativity: the order of bind nesting does not matter. If any law fails, composition breaks and the Kleisli category is not a category.

Scheme

Notation reference

Blog / Haskell Scheme Meaning
return :: a → m a(maybe-return x)Embed a pure value
(>>=) :: m a → (a → m b) → m b(maybe-bind mx f)Bind: chain a computation
join :: m (m a) → m a(maybe-join mmx)Collapse one layer of nesting
(>=>) :: (a → m b) → (b → m c) → (a → m c)(fish f g)Kleisli composition (fish)
Nothing / Just xnothing / (just x)Maybe values
concatMap f xs(list-bind xs f)List bind = flatMap
Writer (a, w)(cons a w)Writer = value + log pair
Neighbors

Milewski chapters

Paper pages that use these concepts

  • ๐Ÿž Fritz 2020 โ€” Markov categories axiomatize the probability monad. The Giry monad (and its Kleisli category Stoch) grounds jkthe handshake between category theory and probability.
  • ๐Ÿž Staton 2025 โ€” monads structure the semantics of effectful programs

Foundations (Wikipedia)

Translation notes

This page combines material from three of Milewski's blog posts: "Monads: Programmer's Definition" (return, bind, do notation), "Monads and Effects" (IO, state, exceptions as monadic effects), and "Monads Categorically" (the endofunctor definition with η and μ). The Scheme translations omit do notation (Scheme has no syntactic equivalent) and IO (Scheme side-effects freely). The blog post proves that any type supporting bind and return is automatically a functor via fmap f m = bind m (λa. return (f a)). The fish operator (>=>) is Kleisli composition from Ch. 4: morphism composition in the Kleisli category. The three monad laws are exactly the category axioms (associativity, left and right identity) for that category. The categorical definition via join (μ) connects directly to adjunctions: if a monad M factors as R∘L for an adjunction L ⊢ R, then join = R∘ε∘L where ε is the counit.

Ready for the real thing? Read the blog post. Start with the fish operator, then see how bind and join are equivalent formulations.