A Lawvere theory is a category whose objects are natural numbers (powers of a generic object) and whose morphisms are n-ary operations. A model is a product-preserving functor L → Set. Every algebraic structure (monoids, groups, rings) is a model of some Lawvere theory. Every finitary monad arises from a Lawvere theory, and every Lawvere theory induces a monad. Lawvere theories compose better than monads: they have coproducts and tensor products where monads have no generic composition recipe.
From universal algebra to categories
Universal algebra describes algebraic structures by their operations and arities. A monoid has a binary operation (arity 2) and a unit (arity 0). A group adds a unary inverse (arity 1). Lawvere's insight: encode these arities categorically. Objects are natural numbers 0, 1, 2, 3, ... representing powers of a generic object. Morphisms n → 1 are n-ary operations. The whole theory lives in a single category.
Scheme
; A Lawvere theory is built from F^op (opposite of finite sets).; Objects = natural numbers (0, 1, 2, 3, ...); Object n = the n-fold product of a generic object.;; Morphisms n -> 1 are the n-ary operations.; Morphisms n -> m are m-tuples of n-ary operations.;; F^op already has projections (picking one of n inputs).; A Lawvere theory adds "interesting" morphisms on top.; Let's represent a theory as a list of named operations with arities.
(define (make-theory name ops)
(list name ops))
(define (theory-ops theory) (cadr theory))
; The theory of monoids: one binary op, one nullary op
(define monoid-theory
(make-theory 'monoid
'((mu . 2) ; binary operation: 2 -> 1
(eta . 0)))) ; unit element: 0 -> 1; The theory of groups: add a unary inverse
(define group-theory
(make-theory 'group
'((mu . 2) ; binary operation
(eta . 0) ; unit
(inv . 1)))) ; inverse: 1 -> 1
(display "Monoid ops: ") (display (theory-ops monoid-theory)) (newline)
(display "Group ops: ") (display (theory-ops group-theory))
; The arities are the morphisms n -> 1 that define the theory.
A model of a Lawvere theory L is a product-preserving functor M : L → Set. It maps the generic object 1 to some set a, and each n-ary operation n → 1 to a function an → a. Product-preserving means M(n) = an. Different models of the monoid theory give different monoids: integers under addition, strings under concatenation, booleans under AND.
Scheme
; A model interprets each operation as a concrete function.; Model of the monoid theory = a set + a binary op + a unit.
(define (make-model carrier mu eta)
(list carrier mu eta))
(define (model-mu m) (cadr m))
(define (model-eta m) (caddr m))
; Model 1: integers under addition
(define int-add-monoid
(make-model 'integers + 0))
; Model 2: strings under concatenation
(define string-monoid
(make-model 'strings string-append ""))
; Model 3: lists under append
(define list-monoid
(make-model 'lists append '()))
; Each model maps the same theory to different concrete operations.
(define (test-model m a b label)
(display label) (display ": ")
(display "mu(") (display a) (display ", ") (display b) (display ") = ")
(display ((model-mu m) a b))
(display " eta = ") (display (model-eta m))
(newline))
(test-model int-add-monoid 34"int-add")
(test-model string-monoid "foo""bar""string")
(test-model list-monoid '(12) '(34) "list")
; Same theory, three models. That's the functor at work.
Python
# A model of the monoid theory: carrier set + binary op + unitclass MonoidModel:
def __init__(self, name, mu, eta):
self.name = name
self.mu = mu
self.eta = eta
int_add = MonoidModel("int-add", lambda a, b: a + b, 0)
str_cat = MonoidModel("string", lambda a, b: a + b, "")
lst_app = MonoidModel("list", lambda a, b: a + b, [])
for m, a, b in [(int_add, 3, 4), (str_cat, "foo", "bar"), (lst_app, [1,2], [3,4])]:
print(f"{m.name}: mu({a}, {b}) = {m.mu(a, b)}, eta = {m.eta}")
Building LMon — the Lawvere theory for monoids
The hom-set LMon(n, 1) contains all n-ary operations you can build from the monoid axioms. For a free monoid on n generators, these are all distinct products of the generators. LMon(2, 1) includes: the unit (ignore both inputs), the two projections (return one input), the product (combine both), and all longer expressions like aba, aab, bba, ... In a free monoid, each of these is a distinct morphism.
Scheme
; L_Mon(2, 1): all binary operations in a free monoid.; With generators a, b, these are all words over {a, b}; including the empty word (unit).; Generate all words of length up to k over an alphabet
(define (words-up-to alphabet k)
(if (= k 0) '(())
(let ((shorter (words-up-to alphabet (- k 1))))
(append shorter
(apply append
(map (lambda (w)
(if (= (length w) k) '()
'())) ; only extend max-length words
shorter)
(map (lambda (w)
(apply append
(map (lambda (c) (list (append w (list c))))
alphabet)))
(filter (lambda (w) (= (length w) (- k 1)))
shorter))))))
; Simpler: enumerate morphisms 2 -> 1 as words over {a, b}; Each word is a function (a, b) -> free-monoid
(define (enumerate-ops max-len)
(define (go len)
(if (= len 0) '(())
(let ((prev (go (- len 1))))
(append prev
(apply append
(map (lambda (w)
(list (append w '(a))
(append w '(b))))
(filter (lambda (w) (= (length w) (- len 1)))
prev)))))))
(go max-len))
(define ops (enumerate-ops 3))
(display "L_Mon(2,1) up to length 3:") (newline)
(for-each (lambda (w) (display " ") (display w) (newline))
ops)
(display "Count: ") (display (length ops))
; () a b aa ab ba bb aaa aab aba abb baa bab bba bbb; Each word is a distinct morphism in the free monoid theory.
Natural transformations between models
A morphism between models is a natural transformation: a function between their carrier sets that commutes with every operation. For monoids, that is exactly a monoid homomorphism. The naturality square says: applying the operation then the function equals applying the function to each input then the operation.
Scheme
; A natural transformation between models is a monoid homomorphism.; h : M1 -> M2 such that h(mu1(a, b)) = mu2(h(a), h(b)); and h(eta1) = eta2
(define (homomorphism? h mu1 eta1 mu2 eta2 test-pairs)
(and; Preserves unit
(equal? (h eta1) eta2)
; Preserves operation (check on test pairs)
(every (lambda (pair)
(equal? (h (mu1 (car pair) (cdr pair)))
(mu2 (h (car pair)) (h (cdr pair)))))
test-pairs)))
; h : (integers, +, 0) -> (strings, string-append, ""); h(n) = n copies of "x"
(define (int->string n)
(make-string (abs n) #\x))
(display "h(0) = eta? ")
(display (equal? (int->string 0) "")) (newline)
(display "h(3+4) = h(3) ++ h(4)? ")
(display (equal? (int->string (+ 34))
(string-append (int->string 3) (int->string 4))))
(newline)
; Length is a homomorphism: (strings, ++, "") -> (ints, +, 0)
(display "len('') = 0? ")
(display (= (string-length "") 0)) (newline)
(display "len('foo' ++ 'bar') = len('foo') + len('bar')? ")
(display (= (string-length (string-append "foo""bar"))
(+ (string-length "foo") (string-length "bar"))))
; Naturality = homomorphism. Same condition, categorical language.
From Lawvere theories to monads
Every Lawvere theory L induces a monad via the free/forgetful adjunction on its models. The forgetful functor U sends each model to its carrier set. The free functor F builds the free model. The monad T = U∘F is given by the coend formula: T(a) = ∫n an × L(n, 1). For LMon, this gives the list monad: T(a) = List(a). Each element of T(a) is a word over the alphabet a, which is exactly a list.
Scheme
; The monad from the monoid Lawvere theory is the list monad.;; T(a) = โซ^n a^n ร L_Mon(n, 1);; L_Mon(n, 1) is the free monoid on n generators.; An element of a^n ร L_Mon(n, 1) is:; - a choice of n elements from a (a tuple); - a word over n generators (a morphism); The coend glues these together: the result is just; the word with generators replaced by the chosen elements.; That's a list of elements from a.; Concretely: T(a) = List(a), return = singleton, join = concat.
(define (T-return x) (list x))
(define (T-join xss) (apply append xss))
(define (T-bind xs f) (T-join (map f xs)))
; The coend in action:; Pick 3 elements from {10, 20, 30} and apply the word "aba"; a=10, b=20 -> word "aba" -> (10 20 10)
(define (apply-word word bindings)
(map (lambda (gen) (list-ref bindings gen)) word))
(display "word (0 1 0) with bindings (10 20): ")
(display (apply-word '(010) '(1020))) (newline)
; The coend identifies: different (tuple, word) pairs that; produce the same list are equivalent.; (bindings (a b), word "ab") ~ (bindings (a b c), word "ab"); because generator c is unused.; The monad operations:
(display "return 5: ") (display (T-return 5)) (newline)
(display "join ((1 2) (3) (4 5)): ")
(display (T-join '((12) (3) (45)))) (newline)
(display "bind (1 2 3) x->(x x*10): ")
(display (T-bind '(123) (lambda (x) (list x (* x 10)))))
; List monad. Same as Ch. 16's free/forgetful result.
Python
# The monad from L_Mon is the list monad.# T(a) = List(a), induced by the free/forgetful adjunction on Mon.def T_return(x):
return [x]
def T_join(xss):
return [x for xs in xss for x in xs]
def T_bind(xs, f):
return T_join([f(x) for x in xs])
# The coend: pick elements, apply a worddef apply_word(word, bindings):
return [bindings[g] for g in word]
print(f"word [0,1,0] with (10,20): {apply_word([0,1,0], [10,20])}")
print(f"return 5: {T_return(5)}")
print(f"join [[1,2],[3],[4,5]]: {T_join([[1,2],[3],[4,5]])}")
print(f"bind [1,2,3] x->[x,x*10]: {T_bind([1,2,3], lambda x: [x, x*10])}")
Side effects as Lawvere theories: exceptions
Adding a single nullary operation (0 → 1) to Fop creates the theory of exceptions. The coend collapses to T(a) = a0 + a1 = 1 + a. In Haskell: Maybe a. A nullary operation means "produce a value from nothing" which is exactly throwing an exception (returning a default failure value). More nullary operations give more exception types.
Scheme
; The Lawvere theory with one extra nullary operation: Maybe.; T(a) = 1 + a (either Nothing or Just a);; The single nullary op 0 -> 1 means:; "there's a way to produce a result from zero inputs"; = a default/failure value = Nothing.
(define (maybe-return x) (list 'just x))
(define nothing '(nothing))
(define (maybe-bind m f)
(if (eq? (car m) 'nothing)
nothing
(f (cadr m))))
; Safe division: nullary op = "divide by zero" exception
(define (safe-div a b)
(if (= b 0) nothing
(maybe-return (/ a b))))
(display "10 / 2: ") (display (safe-div 102)) (newline)
(display "10 / 0: ") (display (safe-div 100)) (newline)
; Chain: divide 100 by x, then divide result by y
(define (chain-div x y)
(maybe-bind (safe-div 100 x)
(lambda (r) (safe-div r y))))
(display "100/5/2: ") (display (chain-div 52)) (newline)
(display "100/0/2: ") (display (chain-div 02)) (newline)
(display "100/5/0: ") (display (chain-div 50))
; Maybe monad from a Lawvere theory with one nullary operation.
Python
# Maybe monad from the exception Lawvere theorydef safe_div(a, b):
return ("just", a // b) if b != 0else ("nothing",)
def maybe_bind(m, f):
return f(m[1]) if m[0] == "just"else m
print(f"10 / 2: {safe_div(10, 2)}")
print(f"10 / 0: {safe_div(10, 0)}")
print(f"100/5/2: {maybe_bind(safe_div(100, 5), lambda r: safe_div(r, 2))}")
print(f"100/0/2: {maybe_bind(safe_div(100, 0), lambda r: safe_div(r, 2))}")
print(f"100/5/0: {maybe_bind(safe_div(100, 5), lambda r: safe_div(r, 0))}")
Lawvere theories vs monads — when they diverge
Every Lawvere theory gives a finitary monad. Every finitary monad comes from a Lawvere theory. But not every monad is finitary. The continuation monad (rra) is the classic counterexample: it cannot be expressed as a Lawvere theory because it is not determined by its action on finite sets. The advantage of Lawvere theories: they compose via coproducts (combine operations from two theories) and tensor products (interleave operations). Monads have no generic composition recipe. This composability is what makes Lawvere theories a natural fit for typed wiring diagrams, where operations from different theories must plug together along typed interfaces.
Scheme
; Finitary = determined by action on finite sets.; The list monad is finitary: a list is a finite sequence.; The continuation monad is NOT finitary.;; Cont r a = (a -> r) -> r; This quantifies over ALL functions a -> r, not just finite ones.
(define (cont-return x)
(lambda (k) (k x)))
(define (cont-bind m f)
(lambda (k) (m (lambda (a) ((f a) k)))))
; callcc: capture the current continuation
(define (callcc f)
(lambda (k) ((f (lambda (a) (lambda (_) (k a)))) k)))
; Run: extract the value by passing identity
(define (run-cont m) (m (lambda (x) x)))
(display "return 5: ")
(display (run-cont (cont-return 5))) (newline)
(display "bind (return 3) (x -> return (x+1)): ")
(display (run-cont
(cont-bind (cont-return 3)
(lambda (x) (cont-return (+ x 1)))))) (newline)
; callcc: short-circuit with 42
(display "callcc short-circuit: ")
(display (run-cont
(cont-bind
(callcc (lambda (exit)
(cont-bind (exit 42)
(lambda (_) (cont-return 0)))))
(lambda (x) (cont-return (* x 10))))))
; 420 โ callcc jumps to exit, skips the (return 0); This monad has no Lawvere theory. It's not finitary.
Notation reference
Blog / Haskell
Scheme
Meaning
Fop
n → m
Opposite of the skeleton of FinSet
IL : Fop → L
(make-theory name ops)
Embedding of Fop into the Lawvere theory
L(n, 1)
(enumerate-ops k)
n-ary operations (hom-set)
M : L → Set
(make-model carrier mu eta)
Model (product-preserving functor)
Nat(M, N)
(homomorphism? h ...)
Natural transformation = homomorphism
TL a = ∫n an × L(n,1)
(T-return x) / (T-bind xs f)
Monad from Lawvere theory (coend)
Cont r a = (a → r) → r
(cont-return x) / (cont-bind m f)
Continuation monad (not finitary)
Neighbors
Milewski chapters
๐ Chapter 17 — Monads (the standard approach Lawvere theories generalize)
๐ Chapter 16 — Adjunctions (free/forgetful adjunction induces the monad)
The blog post builds Lawvere theories in five steps: FinSet → its skeleton F → Fop → the Lawvere theory L → models Mod(L, Set). This page collapses the first three steps and focuses on what the resulting category looks like (objects = arities, morphisms = operations). The coend formula TL(a) = ∫n an × L(n, 1) is presented through the list monad example rather than in full generality. The blog post also discusses the category Law of Lawvere theories, where a morphism between theories is a product-preserving functor that commutes with the embedding from Fop. We skip this level of abstraction. The key point preserved: Lawvere theories and finitary monads are equivalent descriptions of algebraic structure, but Lawvere theories compose (via coproducts and tensor products) where monads do not.
Ready for the real thing? Read the blog post. Start with the five-step construction path, then trace how the coend formula recovers familiar monads.
Lawvere theory is a category whose objects are natural numbers (powers of a generic object) and whose morphisms are n-ary operations. A model is a product-preserving functor L → Set. Every algebraic structure (monoids, groups, rings) is a model of some Lawvere theory. Every finitary monad arises from a Lawvere theory, and every Lawvere theory induces a monad. Lawvere theories compose better than monads: they have coproducts and tensor products where monads have no generic composition recipe.
typed wiring diagrams, where operations from different theories must plug together along typed interfaces.