Monads

Builds on

Required prerequisites, all the way down: 20

You will learn to

• Verify the monad axioms for the list (free monoid) monad, the power-set monad and the 'maybe' (exception) monad on Set.
• Construct the Kleisli and Eilenberg–Moore categories and show that each gives an adjunction inducing the monad.
• Explain how monads model computational effects, and state Beck's monadicity theorem.

Definition

• A monad on C is an endofunctor T with natural transformations η : id ⇒ T and μ : TT ⇒ T satisfying associativity and unit laws.
• An algebra for T is an object A with a morphism a : TA → A such that a ∘ η_A = id_A and a ∘ Ta = a ∘ μ_A.
• The Kleisli category of T has the same objects as C, with morphisms A → TB in C serving as its morphisms from A to B.

Theorem

• Every adjunction F ⊣ G induces the monad GF; every monad arises from an adjunction, and the Kleisli and Eilenberg–Moore adjunctions are initial and terminal among those inducing it.
• Algebras for the list monad on Set are exactly monoids.
• The category of groups is monadic over Set.

Common misconceptions

• Thinking monads come from programming; they arose in algebra and topology (as Godement's 'standard constructions', later called triples).
• Believing the Kleisli and Eilenberg–Moore categories of a monad are always equivalent.

Optional discoveries

• Formal methods Moggi (1991) showed that monads structure the semantics of computational effects; they are central in languages such as Haskell.
• ← Algebraic structures: monoids, groups and rings

Further reading

• Saunders Mac Lane, Categories for the Working Mathematician (1971)
• Emily Riehl, Category Theory in Context (2016)