← back to index

Adjunctions

Bartosz Milewski · 2016 · Category Theory for Programmers, Ch. 16

Prereqs: 🍞 Ch10 (Natural Transformations), 🍞 Ch9 (Function Types). 10 min.

An adjunction L ⊢ R says two functors are "almost inverse": Hom(L(a), b) ≅ Hom(a, R(b)) naturally. The unit η embeds into the round trip; the counit ε collapses it. Every adjunction gives rise to a monad (R∘L), and every monad factors through one. Adjunctions are the engine behind free constructions, currying, and monads.

The hom-set isomorphism

Two functors L : D → C and R : C → D form an adjunction L ⊢ R when there is a natural isomorphism between hom-sets: C(L(a), b) ≅ D(a, R(b)). "Natural" means the bijection commutes with pre- and post-composition. In programming: every function L(a) → b corresponds to exactly one function a → R(b), and vice versa.

Hom(L(a), b) category D Hom(a, R(b)) category C L (free) R (forgetful)
Scheme

Unit and counit

The adjunction is equivalently defined by two natural transformations. The unit η : Id → R∘L embeds a value into the round trip. The counit ε : L∘R → Id collapses it back. They satisfy the triangular identities: ε∘L · L∘η = id and R∘ε · η∘R = id.

left triangle L LRL L εL id right triangle R RLR R ηR id
Scheme

Free/forgetful: the free monoid adjunction

The free functor L takes a set and builds the simplest monoid on it (the list, with concatenation). The forgetful functor R takes a monoid and forgets the operation, leaving just the underlying set. They form an adjunction: L ⊢ R. A monoid homomorphism from the free monoid List(a) to any monoid m corresponds to a plain function from a to the underlying set of m. The unit η wraps a single element into a one-element list.

Scheme

From adjunctions to monads

Every adjunction L ⊢ R gives a monad T = R∘L. The monad's return is the unit η. The monad's join is R∘ε∘L (apply the counit in the middle). For the free/forgetful adjunction, R∘L sends a set to the list of its elements: the list monad. return = singleton list, join = flatten.

Scheme

The state monad from the curry/uncurry adjunction

The product ⊢ exponential adjunction (curry/uncurry) gives the state monad. L(a) = (a, s), R(b) = s → b. The monad T = R∘L sends a to s → (a, s): a stateful computation. return pairs the value with unchanged state. bind threads the state through.

Scheme

Notation reference

Blog / Haskell Scheme Meaning
L ⊢ Rleft-adjunct / right-adjunctAdjunction: L is left adjoint to R
η : Id → R∘L(unit x)Unit: embed into the round trip
ε : L∘R → Id(counit pair)Counit: collapse the round trip
leftAdjunct f = R f . η(left-adjunct f)Transpose L(a)→b to a→R(b)
rightAdjunct g = ε . L g(right-adjunct g)Transpose a→R(b) to L(a)→b
Free monoid ⊢ U(extend f op id)Free/forgetful adjunction
T = R∘Lmonad-return / monad-bindMonad from adjunction
State s a = s → (a, s)(state-return x)State monad from product ⊢ exponential
Neighbors

Milewski chapters

Paper pages that use these concepts

  • 🍞 Hedges 2018 — open games compose via string diagrams in a monoidal category
  • 🍞 Capucci 2021 — parametrised optics generalize adjunctions between lenses and prisms

Foundations (Wikipedia)

Translation notes

The blog post uses Haskell's Adjunction typeclass with functional dependencies. This page uses plain Scheme functions, since Scheme has no type system to enforce the adjunction laws. The Haskell formulation defines unit, counit, leftAdjunct, and rightAdjunct with default implementations in terms of each other. Here we define them independently for each example to make the mechanics visible. The blog post also covers products as adjunctions to the diagonal functor (Δ ⊢ ×) and derives the general recipe for extracting a monad from any adjunction. The state monad derivation on this page follows that recipe for the product/exponential case. One important point from the blog post: every monad can be factored into an adjunction, but the factorization is not unique. The Kleisli and Eilenberg-Moore categories give the two extreme decompositions.

Ready for the real thing? Read the blog post. Start with the hom-set definition, then trace how the unit/counit formulation is equivalent.