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.
Scheme
; The adjunction isomorphism: two ways to say the same thing.; leftAdjunct : (L(a) -> b) -> (a -> R(b)); rightAdjunct : (a -> R(b)) -> (L(a) -> b);; Curry/uncurry is the canonical example.; L = (- x s) "pair with s"; R = (s => -) "function from s"; C((a, s) -> b) ≅ C(a -> (s -> b))
(define (left-adjunct f)
; f : (pair a s) -> b; returns: a -> s -> b
(lambda (a)
(lambda (s)
(f (cons a s)))))
(define (right-adjunct g)
; g : a -> s -> b; returns: (pair a s) -> b
(lambda (pair)
((g (car pair)) (cdr pair))))
; Round-trip test: right then left recovers the original
(define (add-pair p) (+ (car p) (cdr p)))
(define curried (left-adjunct add-pair))
(display "curried 3 then 4: ")
(display ((curried 3) 4)) (newline)
(define uncurried (right-adjunct curried))
(display "uncurried (3 . 4): ")
(display (uncurried (cons 34)))
; Both give 7. The isomorphism is curry/uncurry.
Python
# Curry/uncurry: the product ⊣ exponential adjunctiondef left_adjunct(f):
"""(a, s) -> b becomes a -> s -> b"""returnlambda a: lambda s: f((a, s))
def right_adjunct(g):
"""a -> s -> b becomes (a, s) -> b"""returnlambda pair: g(pair[0])(pair[1])
def add_pair(p): return p[0] + p[1]
curried = left_adjunct(add_pair)
print(f"curried(3)(4) = {curried(3)(4)}")
uncurried = right_adjunct(curried)
print(f"uncurried((3,4)) = {uncurried((3, 4))}")
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.
Scheme
; Unit η : a -> R(L(a)); For product ⊣ exponential with a fixed type s:; L(a) = (a, s) R(b) = s -> b; η(a) = a -> (s -> (a, s)); = a -> (λs. (a, s))
(define (unit a)
(lambda (s) (cons a s)))
; Counit ε : L(R(b)) -> b; L(R(b)) = (s -> b, s); ε((f, s)) = f(s) "evaluate"
(define (counit pair)
((car pair) (cdr pair)))
; η embeds, ε collapses
(display "unit(42) applied to 'hello: ")
(display ((unit 42) "hello")) (newline)
; => (42 . "hello")
(display "counit((add1, 9)): ")
(display (counit (cons (lambda (x) (+ x 1)) 9))) (newline)
; => 10; Triangular identity: counit . L(unit) = id; L(unit)(a, s) = (unit(a), s) = ((λs'. (a, s')), s); counit of that = (λs'. (a, s'))(s) = (a, s) ✓
(define (round-trip pair)
(counit (cons (unit (car pair)) (cdr pair))))
(display "triangle (3 . 7): ")
(display (round-trip (cons 37)))
; => (3 . 7) — identity recovered
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
; Free monoid ⊣ Forgetful; L(a) = List(a) with append as the monoid operation; R(m) = underlying set of m (forget the operation);; Hom_Mon(List(a), m) ≅ Hom_Set(a, R(m)); A monoid homomorphism from lists is determined; by where you send each element.; Unit η : a -> List(a) (singleton list)
(define (free-unit x) (list x))
; Given f : a -> m, extend to a monoid homomorphism List(a) -> m; This is the left adjunct: folds the list using m's operation.
(define (extend f op identity)
(lambda (lst)
(fold-right (lambda (x acc) (op (f x) acc))
identity
lst)))
; Example: sum is determined by sending each number to itself
(define sum-hom (extend (lambda (x) x) + 0))
(display "sum [1,2,3,4]: ")
(display (sum-hom '(1234))) (newline)
; Product is determined by sending each number to itself
(define prod-hom (extend (lambda (x) x) * 1))
(display "product [1,2,3,4]: ")
(display (prod-hom '(1234))) (newline)
; String concat: send each char to a singleton string
(define concat-hom (extend (lambda (c) (string c)) string-append ""))
(display "concat [h,e,l,l,o]: ")
(display (concat-hom '(#\h #\e #\l #\l #\o)))
; The homomorphism is fully determined by f. That's the adjunction.
Python
# Free monoid ⊣ Forgetfulfromfunctoolsimport reduce
def free_unit(x):
"""η: a -> [a]"""return [x]
def extend(f, op, identity):
"""Lift f: a -> m to a monoid homomorphism [a] -> m"""returnlambda lst: reduce(lambda acc, x: op(acc, f(x)), lst, identity)
sum_hom = extend(lambda x: x, lambda a, b: a + b, 0)
print(f"sum [1,2,3,4]: {sum_hom([1,2,3,4])}")
prod_hom = extend(lambda x: x, lambda a, b: a * b, 1)
print(f"product [1,2,3,4]: {prod_hom([1,2,3,4])}")
concat_hom = extend(lambda c: c, lambda a, b: a + b, "")
print(f"concat ['h','e','l','l','o']: {concat_hom(['h','e','l','l','o'])}")
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
; Every adjunction L ⊣ R gives a monad T = R∘L.; Free/forgetful gives the list monad.;; T(a) = R(L(a)) = List(a); return = η : a -> [a] (singleton); join = R(ε(L)) : [[a]] -> [a] (flatten)
(define (monad-return x) (list x))
(define (monad-join xss)
(apply append xss))
; bind = join . fmap f
(define (monad-bind xs f)
(monad-join (map f xs)))
(display "return 5: ")
(display (monad-return 5)) (newline)
(display "join [[1,2],[3],[4,5]]: ")
(display (monad-join '((12) (3) (45)))) (newline)
; bind: each element spawns a list, then flatten
(display "bind [1,2,3] (x -> [x, x*10]): ")
(display (monad-bind '(123) (lambda (x) (list x (* x 10))))) (newline)
; [1, 10, 2, 20, 3, 30]; Monad laws hold because triangular identities hold.; join . return = id
(display "join . return [1,2]: ")
(display (monad-join (monad-return '(12)))) (newline)
; [1, 2]; join . fmap return = id
(display "join . map return [1,2]: ")
(display (monad-join (map monad-return '(12))))
; [1, 2]
Python
# List monad from the free/forgetful adjunctiondef monad_return(x):
return [x]
def monad_join(xss):
return [x for xs in xss for x in xs]
def monad_bind(xs, f):
return monad_join([f(x) for x in xs])
print(f"return 5: {monad_return(5)}")
print(f"join [[1,2],[3],[4,5]]: {monad_join([[1,2],[3],[4,5]])}")
print(f"bind [1,2,3] (x->[x,x*10]): {monad_bind([1,2,3], lambda x: [x, x*10])}")
# Monad lawsprint(f"join . return [1,2]: {monad_join(monad_return([1,2]))}")
print(f"join . map(return) [1,2]: {monad_join([monad_return(x) for x in [1,2]])}")
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
; Product ⊣ Exponential gives the State monad.; T(a) = R(L(a)) = s -> (a, s);; return a = λs. (a, s); bind m f = λs. let (a, s') = m(s) in f(a)(s')
(define (state-return a)
(lambda (s) (cons a s)))
(define (state-bind m f)
(lambda (s)
(let* ((result (m s))
(a (car result))
(s2 (cdr result)))
((f a) s2))))
; get: read the state
(define get (lambda (s) (cons s s)))
; put: replace the state
(define (put new-s) (lambda (s) (cons '() new-s)))
; A stateful computation: increment counter, return old value
(define (tick)
(state-bind get
(lambda (n)
(state-bind (put (+ n 1))
(lambda (_)
(state-return n))))))
(display "tick from state 0: ")
(display ((tick) 0)) (newline)
; (0 . 1) — returned 0, state became 1; Run tick twice
(define two-ticks
(state-bind (tick)
(lambda (first)
(state-bind (tick)
(lambda (second)
(state-return (list first second)))))))
(display "two ticks from 0: ")
(display (two-ticks 0))
; ((0 1) . 2) — got 0 then 1, final state 2
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.