Commutative Codensity Monads
Zev Shirazi
Department of Computer Science
University of Oxford
MSFP, July 2024

Sections 3,5, 6.2
Commutative Codensity Monads

8 July 2024

2 / 36

Overview & Motivation I
1. Commutative monads▶ Monads satisfying a Fubini theorem; can handle multivariable effectful
functions and dataflow graph is exchangeable▶ Linked to current approaches to categorical probability theory andprobabilistic programming and its semantics

2. Codensity monads▶ Presentation of a monad which gives us a formal setting for semantics, sinceKl(T) ⊆ [D, Set]op▶ [Van Belle, 2022] showed that several well-studied probability monads havesuch a presentation with D = FinStoch, all of which are commutative▶ Can we bake commutativity into the syntax of a probability monad using acodensity presentation?
Commutative Codensity Monads

8 July 2024

3 / 36

Overview & Motivation II
3. Exactly pointwise monoidal codensity monads▶ A codensity monad guaranteed to be commutative▶ Kleisli category is monoidal▶ We characterise these as the monads such that this formal setting in[D, Set]op still works in the commutative world (we get a formal descriptionof tensor products).

4. ∗-monads (teaser)▶ Monad of several variables which is more general than a commutative monad▶ Not always guaranteed commutativity from codensity, but always guaranteeda ∗-monad

Commutative Codensity Monads

8 July 2024

4 / 36

Contents

1. Commutative monads
2. Codensity monads
3. Exactly pointwise monoidal codensity monads
4. ∗-monads (teaser)
5. Future work and applications

Commutative Codensity Monads

8 July 2024

5 / 36

Commutative monads

dox←afx

a 7→ Tf (a)7→ µY Tf (a)a1→− TXf

X →− TYf ; a = µY Tfa

Commutative Codensity Monads

8 July 2024

6 / 36

Commutative monads: commutative effects

dox←ay←bf (x,y)

a : TX 7→ T (λλ x.(x, b))(a) : T (X × TY )7→ µX ×Y T (λλ x.T (λλ y .(x, y ))(b))(a) : T (X × Y )7→ µZ Tf (a ⊗l b)
a1→− TX

b1→− TY

f : X × Y → TZ

Commutative Codensity Monads

8 July 2024

7 / 36

Commutative monads: commutative effects

doy←bx←af (x,y)

b : TY 7→ T (λλ y .(a, y ))(b) : T (TX × Y )7→ µX ×Y T (λλ y .T (λλ x.(x, y ))(a))(b) : T (X × Y )7→ µZ Tf (a ⊗r b)a

1→− TXb

1→− TYf : X × Y → TZ

Commutative Codensity Monads

8 July 2024

8 / 36

Commutative effects: Example

if coin = headr+θ
else r − θCommutative Codensity Monads

8 July 2024

9 / 36

Commutative monads: Connection to probability
P▶ Distribution monad DX = {p : X → [0, 1] : x∈X p(x) = 1}, whose Kleislimorphisms are random functions, is commutative.
▶ More generally the Giry monad of continuous distributions (actuallymeasures) on Meas is commutative.
▶ Theory of commutative monads tied to current approaches to categoricalprobability theory.
▶ For semantics of probabilistic programming we look for commutative
probability monads on cartesian closed categories.

Commutative Codensity Monads

8 July 2024

10 / 36

Commutative monads: Categorically▶ In functional programming commutativity is a property▶ On general monoidal categories, we can define commutative monads, but weneed structure:Theorem (A. Kock, 1972)
For C a monoidal category, there is a 1-1 correspondence between commutative(strong) monads , and lax monoidal monads, i.e. monads T with natural maps
κX ,Y : TX ⊗ TY → T (X ⊗ Y )which are coherent with µ and η in addition to the monoidal structure.

Commutative Codensity Monads

8 July 2024

11 / 36

Contents

1. Commutative monads
2. Codensity monads
3. Exactly pointwise monoidal codensity monads
4. ∗-monads (teaser)
5. Future work and applications

Commutative Codensity Monads

8 July 2024

12 / 36

Pointwise codensity monads
Setting
D smallObjects X , Y , ..
Morphisms m, nF

C complete
Objects A, B, ..
Morphisms f , g , ..

SloganIf F is any functor it has a codensity monad T on C.
▶ Idea: F is a model of theory of algebraic effects, T is its largest extension
Commutative Codensity Monads

8 July 2024

13 / 36

Pointwise codensity monads
D small
Objects X , Y , ..
Morphisms m, n

F

C complete
Objects A, B, ..
Morphisms f , g , ..

▶ TA ∈ ob C
▶ h : A → FX =⇒ evh : TA → FX
▶ Fm evh = evFm h▶ (TA, evh ) is a limit over (A ↓ F )Commutative Codensity Monads

8 July 2024

14 / 36

Pointwise codensity monads
Monad structure
Unit:ηA : A → TA
unique map satisfying
ηAAh

TAevh

FX

Commutative Codensity Monads

8 July 2024

15 / 36

Pointwise codensity monads
Monad structure
Multiplication:
µA

TTA
evevh

TAevh

FX
On morphisms f : B → A:
TfTB
evhf

TAevh

FX
Commutative Codensity Monads

8 July 2024

16 / 36

Pointwise codensity monads▶ If you’re familiar with ends:
Z
TA =FX C(A,FX )X ∈ob D▶ In Haskell
newtype Codensity f a = ∀β.a → f β → f β
instance Monad Codensity f wherereturn a = λh.h am ≫= k = λh. m (λx. k x y)
▶ f is a type constructor, interpreted as a functor |C| → C
Commutative Codensity Monads

8 July 2024

17 / 36Codensity monads: A type theoryA ::=X ::=c | TAd | A → X | X =⇒ Y

Γ⊢h:A→XΓ ⊢ ev h : TA → XΓ ⊢ t : C Γ, x : A → X ⊢ k : C → XΓ ⊢ νx.k t : TA
Commutative Codensity Monads

8 July 2024

18 / 36Codensity monads: Examples▶ If F : 1 → C is the inclusion of the subobject X
TX = X C(A,X )In Set, or in enriched settings, just the continuation on X .
▶ If F is a right adjoint to L, then T is the monad induced by the adjunction
L⊣F▶ If T is the pointwise codensity monad of a functor F in our setting, thenthere’s an adjunction inducing the monad, where F ◦ A = C(A, F –):DYD

F[D, Set]opF ◦ ⊣ RanYD FCCommutative Codensity Monads

8 July 2024

19 / 36

Contents

1. Commutative monads
2. Codensity monads
3. Exactly pointwise monoidal codensity monads
4. ∗-monads (teaser)
5. Future work and applications

Commutative Codensity Monads

8 July 2024

20 / 36

Commutative codensity monads▶ In functional programming
1. Commutativity is a property
2. F is from a discrete category. Adding structure to F (e.g. in functortypeclass) can only add structure to T, not properties.

▶ In category theory, lax monoidal monad is structure▶ We can ask if F has structure, when does T▶ In particular if F is lax monoidal, i.e. has natural, coherent maps
κX ,Y : FX ⊗ FY → F (X ⊗ Y )ι : I → FIthen is T?
Commutative Codensity Monads

8 July 2024

21 / 36

Exactly pointwise monoidal codensity monads
h : A → FX

k : B → FY

κX ,Y (h ⊗ k) : A ⊗ B → F (X ⊗ Y )evh,k = evκX ,Y (h⊗k) : T (A ⊗ B) → F (X ⊗ Y )▶ F (m ⊗ n)evh,k = evFmh,Fnk▶ (T (A ⊗ B), evh,k ) is cone over (A ↓ F ) × (B ↓ F )T is exactly pointwise monoidal in degree 2 if this is a limit cone
Commutative Codensity Monads

8 July 2024

22 / 36

Exactly pointwise monoidal codensity monads
hi : Ai → FXi
i = 1, .., nnnnOOO¯
F[X1 ,..,Xn ]hi :Ai → F (Xi )i=1i=1nOi=1nOi=1i=1Ai ) → F (ev[h1 ,..,hn ] : T (Xi )N▶ F ( ni=1 mi )ev[h1 ,..,hn ] = ev[Fm1 h1 ,..,Fmn hn ]NQ
▶ (T ( ni=1 Ai ), ev[h1 ,..,hn ] ) is cone over ni=1 (Ai ↓ F )T is exactly pointwise monoidal in degree k ≥ 1 if this is a limit cone.
Commutative Codensity Monads

8 July 2024

23 / 36

Exactly pointwise monoidal codensity monads
ι : I → FI =⇒ evι : TI → FI
T is exactly pointwise monoidal in degree 0 if this is an isomorphism, and isexactly pointwise monoidal if its exactly pointwise in every degree.

Theorem (Koudenberg 2015, Weber 2016)
If T is exactly pointwise monoidal, it is commutative.
▶ In fact we can significantly weaken these conditions

Commutative Codensity Monads

8 July 2024

24 / 36

Exactly pointwise monoidal codensity monads
Lax monoidal structure:
χA,B : TA ⊗ TB → T (A ⊗ B)
is unique map satisfying
TA ⊗ TB

χA,Bevh,kevh ⊗evk

FX ⊗ FYT (A ⊗ B)

κX ,YF (X ⊗ Y )These behave
Nk a lot like pointwise codensity monads in Cat:
1. T ( i=1 Xi ) has limit structure allowing us to define all the structure of T.
2. Monoidal Kleisli category can be seen to live in [D, Set]op
3. In a formal sense (future work)
Commutative Codensity Monads

8 July 2024

25 / 36

Commutativity: Characterising exactly pointwise▶ When T is the pointwise codensity monad of F
DYD

F[D, Set]opF ◦ ⊣ RanYD FC▶ CT is equivalent to the full subcategory A ⊆ [D, Set]op of functors of theform D(A, F –), A ∈ ob C
▶ Can this picture be lifted to the commutative setting?

Commutative Codensity Monads

8 July 2024

26 / 36

Characterising exactly pointwise
DYD

F[D, Set]opF ◦ ⊣ RanYD FC▶ [D, Set]op has a monoidal structure given by Day convolution:
Z (X1 ,X2 )∈ob D×D
H ⊗Day G (−) =D(X1 ⊗ X2 , −) × HX1 × GX2▶ Ā is full monoidal closure of A (so generated by D(A, F –), for A ∈ ob C),
Commutative Codensity Monads

8 July 2024

27 / 36

Characterising exactly pointwise
Theorem (S. 2024)
T is exactly pointwise monoidal iff A is a coreflective subcategory of Ā such that
1. The coreflection i ⊣ L is oplax monoidal
2. The monoidal structure defined on A by
D(A, F –) ⊗ D(B, F –) = L(D(A, F –) ⊗Day D(B, F –)makes A monoidally equivalent to CTA⊣⊣C

Commutative Codensity MonadsĀ ⊆ [D, Set]op

8 July 2024

28 / 36

Contents

1. Commutative monads
2. Codensity monads
3. Exactly pointwise monoidal codensity monads
4. ∗-monads (teaser)
5. Future work and applications

Commutative Codensity Monads

8 July 2024

29 / 36∗-monads
SloganIf F is any functor in our setting, it has a codensity monad T▶ This doesn’t lift to the lax monoidal world ifnOAi )T(i=1Qnisn’t a limit cone over i=1 (Ai ↓ F )▶ But in our setting we still have limits(T [A1 , .., An ], ev[h1 ,..hn ] )which have interesting categorical structure.
Commutative Codensity Monads

8 July 2024

30 / 36∗-monads
SloganIf F is any lax monoidal functor in our setting, it has a codensity ∗-monad▶ ∗-monads act like monads of multiple variables/arbitrary arity▶ Instead an assignment on objects
X 7→ TX
we get an assignment of lists of objects[X1 , .., Xn ] 7→ T [X1 , .., Xn ]▶ We get multiplication maps and unit maps like in the case of monads.
Commutative Codensity Monads

8 July 2024

31 / 36∗-monads▶ ∗-monads have a version of a Kleisli category. Maps of type
X → T [Y1 , .., Yn ]Yi → T [Zi1 , .., Ziki ]i = 1, .., n

can be composed to a map of type
X → T [Z11 , .., Znkn ]▶ Furthermore this Kleisli op-multicategory is monoidal. Maps of type
X → T [Z1 , .., Zn ]Y → [W1 , .., Wm ]can be tensored to a map
X ⊗ Y → [Z1 , .., Zn , W1 , .., Wm ]Commutative Codensity Monads

8 July 2024

32 / 36

Contents

1. Commutative monads
2. Codensity monads
3. Exactly pointwise monoidal codensity monads
4. ∗-monads
5. Future work and applications

Commutative Codensity Monads

8 July 2024

33 / 36

Future work∗-monads▶ Much to be understood about ∗-monads and their generalisations fromtheoretical point of view
1. ∗-monads can be generalised for symmetric monoidal categories, or any
2-monad on Cat. Similar structures give enriched multicategories.
2. Connection to the theory of generalised multicategories by Hyland, Shulman& Crutwell▶ How can ∗-monads help model effects in functional programming?
▶ Implementation in Haskell

Codensity type theory▶ Work out a formal syntax for codensity▶ Can codensity type theory be combined with type theories for Markov
categories to provide a new kind of probabilistic programming language?
Commutative Codensity Monads

8 July 2024

34 / 36References I
Hermida, C. (2000).
Representable Multicategories.
Advances in Mathematics, 151(2):164–225.
Kock, A. (1972).
Strong functors and monoidal monads.
Archiv der Mathematik, 23(1):113–120.
Leinster, T. (2013).
Codensity and the ultrafilter monad.
Theory and Applications of Categories, 28(1):332–370.

Commutative Codensity Monads

8 July 2024

35 / 36References II
Van Belle, R. (2022).
Probability monads as codensity monads.
Theory and Applications of Categories, 38(21):811–842.
Voigtländer, J.
Asymptotic Improvement of Computations over Free Monads.
pages 388–403, Berlin, Heidelberg. Springer Berlin Heidelberg.
Weber, M. (2016).
Algebraic Kan extensions along morphisms of internal algebra classifiers.
Tbilisi Mathematical Journal, 9(1):65–142.

Commutative Codensity Monads

8 July 2024

36 / 36