Category Theory
Monads in Category Theory
"A monad is a monoid in the category of endofunctors" - what felt mysterious becomes routine. Monads in category theory are not a programmer's invention; they are a fundamental algebraic structure that Eilenberg and Mac Lane studied long before Haskell. They explain recursive data types, folding structures, and "computational effects" in a single language.
- **Recursive data types**: initial F-algebras are exactly recursive types (List, Tree). Fold/catamorphism is the unique homomorphism from the initial algebra. This explains why fold is "more correct" than explicit recursion
- **Haskell do-notation**: monadic `do`-blocks are syntactic sugar for Kleisli chains. The IO monad is an algebra over the IO monad; pure functions are morphisms in the Kleisli category
- **Databases**: an SQL query is a monadic chain (flatMap for JOIN). The List monad models relational algebra: cartesian product = (>>=) for lists
Предварительные знания
Monad
"A monad is a monoid in the category of endofunctors" - that formulation intimidates, but the idea behind it is simple. A monad is a way to "wrap" objects in a context (Maybe, List, IO) with two operations: "place in context" (unit/return) and "flatten a double context" (join/bind). Category theory makes this precise.
A **monad** on category C is a triple (T, η, μ), where T: C → C is an endofunctor, η: Id_C ⇒ T (the unit), μ: T² ⇒ T (the multiplication/join), satisfying: μ ∘ Tη = μ ∘ ηT = Id_T (left and right unit laws) and μ ∘ Tμ = μ ∘ μT (associativity).
**Monad as monoid**: the category of endofunctors [C, C] with the tensor product "∘" (composition) is a monoidal category. A monad is precisely a **monoid in this monoidal category**: an object T with morphisms η: I → T (unit, where I is the identity functor) and μ: T⊗T → T (multiplication) satisfying the monoid axioms. This is the source of Mac Lane's formulation.
| Monad T | T(A) | η (unit) | μ (join) |
|---|---|---|---|
| Maybe | A | null | a ↦ Just a | Just(Just a) ↦ Just a, rest ↦ Nothing |
| List | A[] | a ↦ [a] | [[a₁,...],[b₁,...]] ↦ [a₁,...,b₁,...] |
| Reader r | r → A | a ↦ const a | f: r→(r→A) ↦ r ↦ f(r)(r) |
| State s | s → (A × s) | a ↦ s ↦ (a, s) | join = run outer, then inner |
| IO | "IO action" | pure a | join = sequential execution |
Monads: from Algebra to Programming
Monads were introduced by Roger Godement in 1958 under the name "standard constructions" in the context of homological algebra. Mac Lane independently used them as "triples". Monads were brought into programming by Eugenio Moggi in 1989 as a way to model computational effects. Phil Wadler popularized them for Haskell in 1992.
What does the associativity axiom of a monad μ ∘ Tμ = μ ∘ μT mean?
Kleisli
The **Kleisli category** allows working with a monad as if T-computations were ordinary functions. Objects are the same as in C. Morphisms A → B in the Kleisli category are morphisms A → T(B) in C: "functions with an effect". Composition in Kleisli uses μ to "flatten" the double context.
The **Kleisli category** C_T for a monad (T, η, μ) has the same objects as C. A morphism A →_T B in C_T is a morphism A → T(B) in C. The identity morphism A →_T A is η_A: A → T(A). Composition g ⋆ f (where f: A →_T B, g: B →_T C) is μ_C ∘ T(g) ∘ f: A → T(C).
**The adjunction from Kleisli**: the functor F_T: C → C_T sends A to A and a morphism f: A → B to η_B ∘ f: A → T(B). The functor G_T: C_T → C sends A to T(A) and a Kleisli morphism f: A →_T B to μ_B ∘ T(f): T(A) → T(B). The pair F_T ⊣ G_T is an adjunction inducing the monad T = G_T ∘ F_T. This is the "smallest" adjunction generating T.
In Haskell, monadic computations are written in exactly the Kleisli style: `(>>=) :: m a -> (a -> m b) -> m b` is Kleisli composition. The `do` notation is syntactic sugar for Kleisli chains. Every monadic function `a -> m b` is a Kleisli morphism.
In the Kleisli category for monad T, what is the identity morphism A → A?
Eilenberg Moore
The **Eilenberg-Moore category** is another way to "unpack" a monad. Instead of Kleisli morphisms, it builds **monad algebras**: objects equipped with an operation "collapse the context". A T-algebra over (T, η, μ) is an object A with a morphism α: T(A) → A that "interprets" the context. This gives the "largest" adjunction generating T.
A **T-algebra** (algebra over monad T) is a pair (A, α: T(A) → A) satisfying: α ∘ η_A = id_A (unit law) and α ∘ μ_A = α ∘ T(α) (associativity). The category C^T of T-algebras is the **Eilenberg-Moore category**. The adjunction F^T ⊣ G^T in C^T induces the same monad T.
**The Kleisli-Eilenberg-Moore theorem**: any monad T on C arises from an adjunction, and there may be many such adjunctions. Among them there is a smallest one (the Kleisli category C_T) and a largest one (the Eilenberg-Moore category C^T). Any other adjunction generating T fits between C_T and C^T.
| Monad T | T-algebra (A, α: T(A) → A) | Category of algebras C^T |
|---|---|---|
| Maybe M(A) = A | null | (A, α) where α(null) = default ∈ A | Pointed sets |
| List L(A) = A[] | (A, α: A[] → A) | Monoids (with fold = mconcat) |
| Writer (W,·) | (A, α: W×A → A) | W-sets (W acts on A) |
| State S(A) = s→(A×s) | Complex state algebras | Category of states |
A T-algebra (A, α: T(A) → A) for the List monad is:
Algebras
**F-algebras** and **F-coalgebras** generalize the notion of an algebra in category theory. For a functor F: C → C, an F-algebra is a pair (A, α: F(A) → A) and an F-coalgebra is a pair (A, α: A → F(A)). This is a powerful approach to defining data types via their structure: lists, trees, streams.
The **initial F-algebra** is an F-algebra (μF, in: F(μF) → μF) such that for any F-algebra (A, α) there exists a unique homomorphism (fold/catamorphism): μF → A. The **final F-coalgebra** is dual: (νF, out: νF → F(νF)), receiving a unique morphism from any coalgebra.
**Lambek's theorem**: the initial F-algebra (μF, in) is an isomorphism in: F(μF) ≅ μF. So μF is a **fixed point** of the functor F. This formalizes the idea that `List<A> = Nil | Cons(A, List<A>)` is a recursive data type as the least fixed point. Dually, the final coalgebra is the greatest fixed point.
| Functor F | Initial algebra μF | Final coalgebra νF |
|---|---|---|
| F(X) = 1 + A × X | List<A> (finite lists) | Stream<A> (infinite streams) |
| F(X) = A + X × X | BinaryTree<A> | BinaryTree<A> (infinite trees) |
| F(X) = 1 + X | ℕ (natural numbers) | ℕ ∪ {∞} (extended naturals) |
| F(X) = A × X^B | Infinite B-branching trees | Functions B* → A |
A monad is a complex abstraction specific to Haskell
A monad is a basic categorical construction (an endofunctor with η and μ) found everywhere: in algebra, topology, and the theory of computation. Haskell simply made it explicit
Examples of monads: the power set (P, η: A ↦ {a}, μ: PP(A) → P(A) = union) is a monad in Set. Any adjunction G ∘ F is a monad. Monads formalize "computational effects" (Maybe = partiality, List = nondeterminism, IO = input/output), not just a programmer's invention.
By Lambek's theorem, the initial F-algebra (μF, in: F(μF) → μF) satisfies:
Key Ideas
- **Monad** (T, η, μ): an endofunctor with unit and multiplication; the axioms are the monoid axioms in the category of endofunctors
- **Kleisli category** C_T: morphisms A → B are A → T(B); identity = η; composition uses μ
- **Eilenberg-Moore category** C^T: objects are T-algebras (A, α: T(A)→A); gives the "largest" adjunction for T
- **Initial F-algebra** μF ≅ F(μF) (Lambek's theorem): a recursive data type as a fixed point of a functor
Related Topics
Monads are a central node in category theory:
- Monads in Programming — The next lesson shows concrete monads (Maybe, List, IO) and monad transformers in practice
- Adjoint Functors — Every adjunction induces a monad. Kleisli and Eilenberg-Moore are the extreme adjunctions for a given monad
Вопросы для размышления
- The List monad is the "free monoid monad". Why are the algebras of the List monad exactly monoids? Write out the T-algebra axioms for List and compare them with the monoid axioms.
- How does the Kleisli category differ from the Eilenberg-Moore category for the same monad? Give an example for the Maybe monad.
- By Lambek's theorem, List<A> ≅ 1 + A × List<A>. How does this relate to a recursive type definition in Haskell? Why is the initial algebra the "least" fixed point?