Emily Riehl
Johns Hopkins University

A categorical view of computational effects

C◦mp◦se::Conference1. Functions, composition, and categories

2. Categories for computational effects (monads)

3. Categories of operations and equations (Lawvere theories)

4. Lawvere theories vs monads

Preview
Let T denote a notion of computation.

f• A T-program is a function A −→ T(B) from the set of values of type

A to the set of T-computations of type B.
• T is a monad just when it has the structure needed to turnT-programs into a category.
• The T-programs between finite types define a Lawvere theory.
• The Lawvere theory presents the operations and equations for thecomputational effect T.**If T is not finitary, these operations and equations define a different monad.

1Functions, composition, andcategories

The mathematician’s view of functions
A function, e.g.:f (x) = x2 − xalways comes with specified sets of “possible input values” and “potentialoutput values.” One writes
IfO

to indicate that f is a function with source I and target O.
Why bother with sources and targets? This data indicates when twofunctions are composable:AfBandBgC

are composable just when the target of f equals the source of g.

Composable and non-composable functions
Are the functions
2f (x) = x − xand

 y1g(y) =2composable? It depends. If
fNZandg

Z

Q

where N is the set of natural numbers, Z is the set of integers, and Q is
x2 −x. But if
the set of rational numbers then yes: (g ◦ f )(x) = 12
Mat2×2 (Z)fMat2x2 (Z)andgZQ

where Mat2×2 (Z) is the set of 2 × 2-matrices with integer coefficients
ythen no: what is the meaning of 12 if y is a matrix?

What is a category?
A category is a two-sorted structure that encodes the algebra ofcomposition. It has• objects: A, B, C . . . andfg• arrows: A −→ B, B −→ C, each with a specified source and target

so that• for any pair of composable arrows:

Bgf

ACg◦f

there exists a composite arrowidA• and each object has an identity arrow A −→Afor which the composition operation is associative and unital.

What is the point of identities?
An isomorphism consists of:fAg

B

so thatg ◦ f = idA

andf ◦ g = idB

Isomorphism invariance principle:
If A and B are isomorphic then every
category theoretic property of A is also true of B.

Examples of categories
In the category Set the• objects are (finite) sets X, Y, . . .
f• arrows are functions X −→ Y, . . .

In the syntactic category for some programming language the• objects are types X, Y, . . .
f• arrows are programs X −→ Y, . . .

Note that the same notation describes the data in any category. The
precise ontology of the objects and arrows won’t matter much.

2Categories for computational effects(monads)

Notions of computation
Let us introduce some large functions
SetTSeteach encoding some notion of computation:• list(X) := finite lists of elements of X
• partial(X) := X + {⊥}• side-effectsS (X) := [S, S × X], the set of functions from S toS×X• continuationsR (X) := [[X, R], R], the set of functions fromthe set [X, R] of functions from X to R to R
• non-det(X) := P+ (X), the set of non-empty subsets of Xp• prob-dist(X) := the set of probability functions X −→ [0, 1] sothatPx∈X p(x) = 1

T-programs
For any notion of computation T• list(X) := finite lists of elements of X
• partial(X) := X + {⊥}• side-effectsS (X) := [S, S × X], the set of functions from S toS×X• continuationsR (X) := [[X, R], R], the set of functions fromthe set [X, R] of functions from X to R to R
• non-det(X) := P(X), the set of all subsets of Xp• prob-dist(X) := the set of probability functions X −→ [0, 1] sothatPx∈X p(x) = 1f

A T-program from A to B is a function A −→ T(B), from the set of valuesof type A to the set of T-computations of type B. WritefA

Bto meanfA−→ T(B).

Programs should form a categoryf

A T-program from A to B is a function A −→ T(B), from the set of valuesof type A to the set of T-computations of type B.
The notion of monad arises from the following categorical imperative:

programs should form a category

Theorem: A notion of computation T defines a monad if* and only if thef

T-programs A

B define the arrows in a category.

*If the category of T-programs is constructed using a Kleisli triple, as depicted on the next slide, then T defines a monad.

The category of T-programs
To define the category of T-programs we need:
idA

η

AT(A)
A; a monad has unit functions A −→• a composition rule for T-computations:• identity arrows AfABfCg◦fg

Problem: A −→ T(B) and B −→ T(C)
are not composable!

gg

With a monad, any function B −→ T(C) can be extended to a functiong∗T(B) −→ T(C). Thenf

AT(B)

g∗

T(C)

g ∗ ◦fg

fdefines the Kleisli composite of A

B and B

C in the category KlT .

The category of partial-computations
For partial(X) := X + {⊥}f

• A program Af

B is a function A −→ B + {⊥}, i.e., a partial function

from A to B.
• The unit AidAincl

A is the function A −→ A + {⊥}.
g

• Any function B −→ C + {⊥} extends to a functiong∗

B + {⊥} −→ C + {⊥}by the rule g ∗ (⊥) = ⊥.
• The Kleisli compositefABg◦f

B + {⊥}gfCA

is the largest partial function from A to C.

g ∗ ◦fg∗

C + {⊥}The category of list-computations
For list(X)f• A program Af

B is a function A −→ list(B), i.e., a function fromA to lists in B.
• The unit AidA

singletonlist(A) is the function A −−−−→ list(A).
g• Any function B −→ list(C) extends to a functiong∗list(B) −→ list(C)by applying g to each term in a list of elements of B andconcatenating the result.
• The Kleisli compositefABg◦flist(B)gf

CAg ∗ ◦fg∗

list(C)is defined by application of f and g followed by concatenation.

3Categories of operations andequations (Lawvere theories)

Kleisli arrows define operations
Let n := {x1 , . . . , xn } denote the set with n elements.
An arrow 1n in the category of list-programs Kllist is• a function 1 → list(n)(by definition)• an element of list(n)(the image of the previous function).

E.g.

Arrows 11x3 x5 x2 x5

6or equivalently

x3 x5 x2 x5 ∈ list(6)n, i.e., elements of list(n), define n-ary operations.

Kleisli composites define equations between operations
In the category of list-programs Kllist , arrows 1operations.

nCompositions

n define n-ary

define equations between operations.

1mE.g.
x1 x2

12x1 x2 x3(x1 ,x2 x3 )3corresponds to the equation
x1 (x2 x3 ) = x1 x2 x3 .
Together these operations and equations define the list-theory Llist .

Models for the list-theory
A model for the list-theory Llist is:• a set A• together with a function An → A for each n-ary operation 1n• satisfying the equations determined by the compositions in thecategory of programs.
E.g.

x1 x2

12x1 x2 x3

A2(x1 ,x2 x3 )3

are modeled byλ.(x1 ,x2 x3 )λ.x1 x2
λ.x1 (x2 x3 )A

=A3

λ.x1 x2 x3

A model for the list-theory Llist is a contravariant
product-preserving functor from the category Llist of list-programs
between finite sets.

4
Lawvere theories vs monads

models for a Lawvere theory
If T is any monadic notion of computation let LT denote the category ofT-programs between finite sets. The opposite category LT op , obtainedby formally reversing the arrows, defines a Lawvere theory.
opA model is a functor LT → Set defined on objects byand carrying each arrow n
Am → An .

1

A

2

A2..
.

..
.

nAnm in the category LT to a function

algebras for a monad
If T is any monadic notion of computation an algebra for T is a set A
αtogether with a function T(A) −→ A so that the composition relations
hold:AηAidAT(A)αAT(T(A))

id∗T(A)

αTα

TATAα

A

Theorem: The category of models for the Lawvere theory LT op and thecategory of algebra for the monad T are equivalent.

monads vs Lawvere theories
A monad isT• a “notion of composition” Set −→ Setf

• so that T-programs A −→ T(B) define the arrows Af

B in acategory KlT .
The opposite of the category of T-programs between finite sets definesa Lawvere theory LT op . Conversely, any Lawvere theory defines amonad on Set.
Theorem: The category of Lawvere theories is equivalent to thecategory of finitary monads∗ on Set.
Finitary monads and Lawvere theories describe equivalent categorical encodings of universal algebra.

Advantages of Lawvere theories
Why bother with Lawvere theories if they are equivalent to monads?
• Each monad acts on just one category, whereas models of Lawvere

theories can be defined in any category with finite products — andthe construction of the category of models is functorial in botharguments.
• Lawvere theory operations can be added: any two Lawvere

theories L and L0 have a sum L + L0 — indeed the category ofLawvere theories is locally finitely presentable.
• Lawvere theory operations can be intertwined: any two Lawvere

theories L and L0 have a tensor product L ⊗ L0 .
• In practice, Lawvere theories are generated by computationally

natural operations satisfying computationally meaningful equations— e.g., exceptions, side-effects, interactive input-output, …

Continuations
All of computational effects mentioned thusfar fit into this framework for
categorical universal algebra with one exception:
Even for 2 = {>, ⊥}, the continuations monadcontinuations2 (X) := [[X, 2], 2] = P(P(X))
is not finitary. It does define a large Lawvere theory, but this is specified
with a proper class of operations.

“it appears that the continuations monad transformer should be seen as
something sui generis.”A look towards the future
In “The Category Theoretic Understanding of Universal Algebra:
Lawvere Theories and Monads”, Martin Hyland and John Power suggestthat “computational effects might be seen as an instance anddevelopment of universal algebra.” From this viewpoint:• “Continuations would not be regarded as a computational effect

but rather as a distinct notion. It would still have its own body oftheory, and one would still study the relationship between it andcomputational effects; but perhaps it would not be regarded as acomputational effect?”• “Monads appear quite directly in the study of continuations. Soperhaps the notion of monad might be seen as a generalised
semantics of continuations?”

Review
Let T denote a notion of computation.

f• A T-program is a function A −→ T(B) from the set of values of type

A to the set of T-computations of type B.
• T is a monad just when it has the structure needed to turnT-programs into a category.
• The T-programs between finite types define a Lawvere theory.
• The Lawvere theory presents the operations and equations for thecomputational effect T.**If T is not finitary, these operations and equations define a different monad.

References• Eugenio Moggi, “Computational lambda-calculus and monads”— describes monads and the category of programs• Gordon Plotkin and John Power, “Computational Effects andOperations: An Overview”— describes the connection between
Moggi’s monads and Lawvere theories• Martin Hyland and John Power, “The Category Theoretic

Understanding of Universal Algebra: Lawvere Theories andMonads”— inspired this talkThank you!