Unifying graded andparameterised monads
Dominic OrchardPhilip Wadler

Harley Eades IIIMSFP 2020
!3

The humble monad
T:ℂ→ℂjoin :: m m a -> m aT∘T𝖨𝖽μη

return :: a -> m aTT

multiplicationunit+ associativity and unitality axioms!4Graded monads
G : 𝔼 → [ℂ, ℂ]

Functor(𝔼, ∙ ,I)

(Discrete) monoidal category

Gx ∘ Gy

𝖨𝖽μx,yηG (x ∙ y)GI

multiplicationunit+ associativity and unitality axioms[Wadler&Thiemman’03 - Marriage of eﬀects and monads][Katsumata'14 - Parametric eﬀect monads and semantics of eﬀect systems]!5Graded monads for type-based effect analysis
monadic metalanguageΓ ⊢ e : MA Γ, x : A ⊢ e′ : M BΓ ⊢ do x ← e; e′ : M BΓ⊢ e:AΓ ⊢ return e : M A!6

Graded monads for type-based effect analysis
gradedmonadic metalanguageΓ ⊢ e : G x A Γ, x : A ⊢ e′ : G y BΓ ⊢ do x ← e; e′ : G (x ∙ y) BΓ⊢ e:AΓ ⊢ return e : G I A... for refining semantics
Humble state𝖲𝗍𝖺𝗍𝖾 A = 𝖲𝗍𝗈𝗋𝖾(ℒ) → A × 𝖲𝗍𝗈𝗋𝖾(ℒ)
𝗀𝖾𝗍 : (l : A ∈ ℒ) → 𝖲𝗍𝖺𝗍𝖾 A
𝗉𝗎𝗍 : (l : A ∈ ℒ) → A → 𝖲𝗍𝖺𝗍𝖾 1

vs. graded

𝖲𝗍𝖺𝗍𝖾 x A = 𝖲𝗍𝗈𝗋𝖾(𝗋𝖾𝖺𝖽𝗌(x)) → A × 𝖲𝗍𝗈𝗋𝖾(𝗐𝗋𝗂𝗍𝖾𝗌(x))
𝗀𝖾𝗍 : (l : A ∈ ℒ) → 𝖲𝗍𝖺𝗍𝖾 {r(l)} A
𝗉𝗎𝗍 : (l : A ∈ ℒ) → A → 𝖲𝗍𝖺𝗍𝖾 {w(l)} 1!7

Graded monads
G : 𝔼 → [ℂ, ℂ]

Functor(𝔼, ∙ ,I)

(Discrete) monoidal category

Gx ∘ Gy

𝖨𝖽μx,yηG (x ∙ y)GI

multiplicationunit+ associativity and unitality axioms!8

(unordered) Graded monads
G : 𝔼 → [ℂ, ℂ]

Functor(𝔼, ∙ ,I)(Discrete) monoidal category

Gx ∘ Gy

𝖨𝖽

μx,y

η

G (x ∙ y)GI

multiplicationunit+ associativity and unitality axioms

unorderedgradedmonads!9

Graded monads
G : 𝔼 → [ℂ, ℂ]

Functor(𝔼, ∙ ,I, ≤ )Strict monoidal category

Gx ∘ Gy

𝖨𝖽

Gx

μx,y

η

G (x ∙ y)GI

Gymultiplication

unit

approximation+ associativity and unitality axioms

G(h : x ≤ y)

+ monotonicity

unorderedgradedmonads!10

Parametrised monads
𝗈𝗉P : 𝕀 × 𝕀 → [ℂ, ℂ]
P(i, j) ∘ P( j, k)

𝖨𝖽μi,j,kηiP (i, k)

P (i, i)

multiplication

unit

Functor+ associativity and unitality axioms[Atkey'06/'09 - Parameterised notions of computation]!11

Parametrised monads
𝗈𝗉

P : 𝕀 × 𝕀 → [ℂ, ℂ]
P(i, j) ∘ P( j, k)
μi,j,k𝖨𝖽

ηi

P (i, k)P (i, i)

multiplicationunit+ associativity and unitality axioms[Atkey'06/'09 - Parameterised notions of computation]

Af

FunctorP(i, j) BAμi,j,k,C ∘ Pg ∘ fg

B P( j, k) CP(i, k) C

cf Floyd-Hoare logic{i} C {j}{j} C′ {k}{i} C; C′ {k}!12Parametrised monads
𝗈𝗉

P : 𝕀 × 𝕀 → [ℂ, ℂ]
P(i, j) ∘ P( j, k)

𝖨𝖽μi,j,kηiFunctor

P (i, j)P( f : i′ → i, g : j → j′)

P (i, k)P (i, i)P (i′, j′)multiplication

unit

approximation+ associativity and unitality axioms[Atkey'06/'09 - Parameterised notions of computation]+ dinaturality axioms!13

G and P: side-by-sideGx ∘ Gy

P(i, j) ∘ P( j, k)

μx,yμi,j,kG (x ∙ y)

P (i, k)𝖨𝖽𝖨𝖽ηηiGIP (i, i)

Can we unify their definitions?
!14Roadmap

2-category-gradedmonads+ generalised unit

2-categorygraded monads

unorderedgradedmonadscategory-graded monads+ generalised unit

category-gradedmonads“oidify”

discreteparameterised
monadsmonads!15

“Oidification”
1. concept shown to be equivalent to a single-object category
2. generalise that to a category with more than one object/morphism

https://ncatlab.org/nlab/show/horizontal+categorification!16

Monads are lax functors(Benabou 1967)

F:ℂ→𝔻

id = F id
Fg ∘ Ff = F(g ∘ f )⋆One object

Recall: functor axioms

One morphism
Lax functor axioms

id : ⋆ → ⋆T : 1 → 𝖤𝗇𝖽𝗈(ℂ)
One objectℂMorphisms are endofunctors
2-morphisms are nat. trans.

id ⇒ F id
Fg ∘ Ff ⇒ F(g ∘ f )+ associativity/unitality

𝔻 is a 2-category
Here natural transformations

η:id ⇒ T id
μ : Tid ∘ Tid ⇒ Tid!17

Oidifying a monad
Monad“Category-graded monad”

1𝗈𝗉

T(Benabou 1967)

𝖤𝗇𝖽𝗈(ℂ)oidification/ horizontal
categorificationℱT𝖤𝗇𝖽𝗈(ℂ)

Lax functor

η : 𝖨𝖽 ⇒ T id
μ : T id ∘ T id ⇒ T id

ηx : 𝖨𝖽 ⇒ T id x
μf,g : Tf ∘ Tg ⇒ T(g ∘ f )!18

1. Unordered graded monads are category-graded monads“Category-graded monad”

𝗈𝗉ℱ

Monoid-graded monad GT(𝔼, ∙ ,I)
G𝖤𝗇𝖽𝗈(ℂ)[ℂ, ℂ]

ηx : 𝖨𝖽 ⇒ T id x
μf,g : Tf ∘ Tg ⇒ T(g ∘ f )!19

Monoids are one-object categories are discrete monoidal categoriesx∙yI⋆xy!201. Unordered graded monads are category-graded monads
Category-graded monad

Monoid-graded monad G𝗈𝗉ℱT𝖤𝗇𝖽𝗈(ℂ)ηx : 𝖨𝖽 ⇒ T id x
μf,g : Tf ∘ Tg ⇒ T(g ∘ f )⊇1(𝔼o p,∙,I) ≡ (𝔼, ∙ ,I)
G𝖤𝗇𝖽𝗈(ℂ) ≡ [ℂ, ℂ]η⋆ : 𝖨𝖽 ⇒ G I

μx,y : G x ∘ G y ⇒ G (x ∙ y)!21

2. Graded monads are 2-category-graded monads
2-category-graded monad
Category-graded monad𝗈𝗉

T : ℱ → 𝖤𝗇𝖽𝗈(ℂ)ηx : 𝖨𝖽 ⇒ T id x
μf,g : Tf ∘ Tg ⇒ T(g ∘ f )+ 2-morphism mapping

T(h : g ⇒ f ) : T g ⇒ T f(i.e., ℱ is a 2-category)22

Pomonoids are one object 2-categories are monoidal categories

yx≤ y

⋆x

⟹

!23

2. Graded monads are 2-category-graded monads
2-category-graded monad(Ordered) Graded monad𝗈𝗉

T : ℱ → 𝖤𝗇𝖽𝗈(ℂ)ηx : 𝖨𝖽 ⇒ T id x
μf,g : Tf ∘ Tg ⇒ T(g ∘ f )T(h : g ⇒ f ) : T g ⇒ T f⊇

G : 1(𝔼o p,∙,I,≤ ) → 𝖤𝗇𝖽𝗈(ℂ)η⋆ : 𝖨𝖽 ⇒ G I
μx,y : G x ∘ G y ⇒ G (x ∙ y)G(h : x ≤ y) : G x ⇒ G y

2-morphism mapping24

Roadmap
2-categorygraded monads

unorderedgradedmonads

category-graded monads+ generalised unit

category-gradedmonads“oidify”

discreteparameterisedmonads

monads!25

3. Discrete parameterised monads are category-graded monads
𝗈𝗉P : 𝕁 × 𝕁 → [ℂ, ℂ]

where !𝕁 has only identity morphisms

Define the category of 𝕁! -“dominoes”∇(𝕁)1 = | 𝕁 | × | 𝕁 |(e.g., composition (! j, k) ∘ (i, j) =(i, k) )Define a category graded monadT : ∇(𝕁) → 𝖤𝗇𝖽𝗈(ℂ)ηi : 𝖨𝖽 ⇒ T(i, i)with !T(i, j) = P(i, j)=

μ(i,j),( j,k) : T (i, j) ∘ T ( j, k) ⇒ T (i, k) =PηiP
μi,j,k!26

Parameterised monads have some extra structure
P (i, j)P( f : i′ → i, g : j → j′)

P (i′, j′)morphism mapping (approximation)+ dinaturality axioms!27Generalised units
arises from lax natural transformations (Street, 1972)

Wide sub-category

Family of morphisms

𝕊⊆ℱ̂ηf:X→Y∈:𝖨𝖽→Tf𝕊

4. Parameterised monads are category-graded monads + !η̂Paper shows details
28

Roadmap

2-category-gradedmonads+ generalised unit

2-categorygraded monads

unorderedgradedmonadscategory-graded monads+ generalised unit

category-gradedmonads“oidify”

discreteparameterised
monadsmonads!29

Example| ℱ | = {free, critical}
lock : free → criticalunlock : critical → freeget, put : critical → critical𝗈𝗉

𝖢𝗈𝗇𝖼𝖲𝗍 : ℱ → 𝖤𝗇𝖽𝗈(ℂ)
g et : 𝖢𝗈𝗇𝖼𝖲𝗍 get S

pu t : S → 𝖢𝗈𝗇𝖼𝖲𝗍 put 1
lo ck : 𝖢𝗈𝗇𝖼𝖲𝗍 lock 1
u n lo ck : 𝖢𝗈𝗇𝖼𝖲𝗍 unlock 1

spawn : ( ∀f . 𝖢𝗈𝗇𝖼𝖲𝗍 ( f : 𝖿𝗋𝖾𝖾 → 𝖿𝗋𝖾𝖾) 1) → 𝖢𝗈𝗇𝖼𝖲𝗍 f 1

30

Conclusions• Shows us where graded & parameterisedoverlap• A more general structure that captures bothaspects: tracing + restriction

granule-project.github.io

Thank you!

Category-graded monad𝗈𝗉ℱT𝖤𝗇𝖽𝗈(ℂ)ηx : 𝖨𝖽 ⇒ T id x
μf,g : Tf ∘ Tg ⇒ T(g ∘ f )31