Composition of Monads

Jeremy E. Dawson

Logic & Computation Programme  Automated Reasoning Group
National ICT Australia  Computer Sciences Laboratory

Res. Sch. of Inf. Sci. and Eng. Australian National University

Jeremy.Dawson@nicta.com.au     http://rsise.anu.edu.au/∼jeremy

2006 1

Types of monad functions

unit: α → αM
map : (α → β) → (αM → βM)
join : αMM → αM
ext : (α → βM) → (αM → βM)
bind : αM → (α → βM) → βM
⊙ : (β → γM) → (α → βM) → (α → γM)

Examples for the list monad

let g 1 = [1], g 3 = [1, 2, 3], etc

unita = [a]
map f [x, y, z] = [f x, f y, f z]
join[[u, v], [w], [x, y]]= [u, v, w, x, y]
ext g [2, 0, 4] = [1, 2, 1, 2, 3, 4]

2006 2

Relationships between monad functions

m bind f = ext f m
ext f = join ∘ map f
join = ext id
map f = ext (unit ∘ f)
g ⊙ f = ext g ∘ f
ext g = g ⊙ id

2006 3

Monad rules for unit, map and join

map id = id  (1)
map f ∘ map g = map (f ∘ g)  (2)
unit ∘ f = map f ∘ unit  (3)
join ∘ map (map f) = map f ∘ join  (4)
join ∘ unit= id  (5)
join ∘ map unit= id  (6)
join ∘ map join = join ∘ join  (7)
ext f = join ∘ map f  (8)
ext (g ∘ f) = ext g ∘ map f  (9)

2006 4

Examples of monad rules

join ∘ unit= id  (5)
join[[3, 5, 7]] = [3, 5, 7]
join ∘ map unit= id  (6)
join[[3], [5], [7]] = [3, 5, 7]
join ∘ map (map f) = map f ∘ join  (4)

[[u, v], [w], [x, y]] \begin{matrix}[[u′, v′], [w′], [x′, y′]] \\ [u, v, w, x, y] \end{matrix} [u′, v′, w′, x′, y′]

join ∘ map join = join ∘ join  (7)

[[[u, v], [w]], [[x], [y, z]] \begin{matrix}[[u, v, w], [x, y, z]] \\ [[u, v], [w], [x], [y, z]] \end{matrix} [u, v, w, x, y, z]

2006 5

Monad rules for unit, ext and ⊙

ext f ∘ unit= f  (E1)
ext unit= id  (E2)
ext (ext g ∘ f) = ext g ∘ ext f  (E3′)
join = ext id  (E4)
map f = ext (unit ∘ f)  (E5)

ext f ∘ unit = f  (E1)
ext unit = id  (E2)
ext (g ⊙ f) = ext g ∘ ext f  (E3)
g ⊙ f = ext g ∘ f  (E6)

2006 6

A useful theorem

Theorem 1 In a monad the following are equivalent (i) ext g = g ∘ join (ii) g = ext (g ∘ unit) (iii) there exists f such that g = ext f (iv) for all h, ext (g ∘ h) = g ∘ ext h Refer monad rules (E4), (7), (E5) and (4)

2006 7

Identity and associativity in the Kleisli category K_{M}

Theorem 2 Assuming rules (E1) to (E3)

g ⊙ f = ext g ∘ f  (E6)
(h ⊙ g) ∘ f = h ⊙ (g ∘ f)  (A6)
ext f = ext g ⇒ f = g  (EI)
f ⊙ unit= f  (A1)
unit ⊙ f = f  (A2)
h ⊙ (g ⊙ f) = (h ⊙ g) ⊙ f  (A3)

the Kleisli category K_{M}: objects are types — α, β, etc an arrow from α to β is a function of type α → βM identity arrow on α is unit: α → αM composition is ⊙ : (β → γM) → (α → βM) → (α → γM), so g from β to γ and f from α to β compose to give g ⊙ f, from α to γ Rules (A1) to (A3) give the properties required for a category.

2006 8

Monad Rules Based on the Kleisli Category K_{M}

f ⊙ unit= f  (A1)
unit ⊙ f = f  (A2)
h ⊙ (g ⊙ f) = (h ⊙ g) ⊙ f  (A3)
(h ⊙ id) ∘ f = h ⊙ f  (A4)
h ⊙ (unit ∘ f) = h ∘ f  (A4′)
ext g = g ⊙ id  (A5)
(h ⊙ g) ∘ f = h ⊙ (g ∘ f)  (A6)

2006 9

The State Monad

Let State be a fixed type, eg, the program state. Let αS = State → α ∗ State unit_{S} a s = (a, s) (g ⊙_{S} f) a s = let (b, s′) = f a s in g b s′

Proof tedious, but use unc (inverse is curry, so both 1-1)

curryg x y = g (x, y)  unc f (x, y) = f x y

So for f : α → βS, unc f : α ∗ State → (β ∗ State) M. for (A1) and (A2):

unc (f ⊙_{S} unit_{S}) = unc f ∘ unc unit_{S} = unc f ∘ id = unc f unc (unit_{S} ⊙_{S} f) = unc unit_{S} ∘ unc f = id ∘ unc f = unc f

for (A3): unc (h ⊙_{S} (g ⊙_{S} f)) = unc h ∘ (unc g ∘ unc f) =

(unc h ∘ unc g) ∘ unc f = unc ((h ⊙_{S} g) ⊙_{S} f) 2006 10

The Compound State Monad

Let M be any monad. Define αS_{M} = State → (α ∗ State)M. We can define ⊙_{SM} and unit_{SM} by

unc (g ⊙_{SM} f) = unc g ⊙_{M} unc f
unc unit_{SM} = unit_{M}

Then the proofs are easy, using corresponding rules for monad M. for (A1) and (A2): unc (f ⊙_{SM} unit_{SM}) = unc f ⊙_{M} unc unit_{SM} = unc f ⊙_{M} unit_{M} = unc f unc (unit_{SM} ⊙_{SM} f) = unc unit_{SM} ⊙_{M} unc f = unit_{M} ⊙_{M} unc f = unc f for (A3): unc (h ⊙_{SM} (g ⊙_{SM} f)) = unc h ⊙_{M} (unc g ⊙_{M} unc f) =

(unc h ⊙_{M} unc g) ⊙_{M} unc f = unc ((h ⊙_{SM} g) ⊙_{SM} f)

Other definitions more complicated, and proofs correspondingly so. 2006 11

A free theorem ??

Still need to prove (A4),

(h ⊙ id) ∘ f = h ⊙ f f : α → βM h : β → γM

Can we use Wadler’s “free theorems”? Idea is that h ⊙ : (α → βM) → α → γM is polymorphic in α, so in applying h ⊙ f to a : α, can only apply f to a, and then do something else, call it g. That is, h ⊙ f = g ∘ f, so

(h ⊙ id) ∘ f = (g ∘ id) ∘ f = g ∘ f = h ⊙ f

Is this valid?

2006 12

Other Monads

List monad: αL = α list Reader monad: αR = param → α Writer monad: αW = α × output Error monad: αE = α option (SOME a for success, NONE for failure) These can form compound monads with an arbitrary monad M in different ways: αMR, αW M, αEM αE can represent termination of a program with a result, or non-termination αEL represents corresponding non-deterministic program operation αLE also represents such a program for considering total correctness: if it may fail to terminate then never mind what else it might do, it is a failure. αLE is also a compound monad

2006 13

Compound Monads via Partial Extension

compound monad type is (αN)M = αNM. To define a compound monad NM, need ext_{NM}, “extending” a function f from a “smaller” domain, α, to a “larger” one, αNM. Consider a “partial extension” function pext which does part of this job:

ext_{NM} : (α → βNM) → (αNM → βNM)
pext : (α → βNM) → (αN → βNM)

Then ext_{NM} f = ext_{M} (pext f). Rules (E1K) to (E3K) are enough to define NM. About ⊙_{NM} or unit_{NM}, assume only they have the right types. Need not assume that N is a monad.

2006 14

Monad rules for a compound monad using pext

pext f ⊙_{M} unit_{NM} = f  (E1K)
pext unit_{NM} = unit_{M}  (E2K)
pext (g ⊙_{NM} f) = pext g ⊙_{M} pext f  (E3K)
kjoin = pext unit_{M}  (E4K)
kmap f = pext (unit_{NM} ⊙_{M} f)  (E5K)
g ⊙_{NM} f = pext g ⊙_{M} f  (E6K)

These are just the rules needed for a monad N in K_{M} 2006 15

Correspondence between monad N and monad N in K_{M}

id : α → α  unit_{M} : α → αM
unit_{N} : α → αN  unit_{NM} : α → αNM
map_{N} : (α → β) → αN → βN  kmap : (α → βM) → αN → βNM
join_{N} : αNN → αN  kjoin: αNN → αNM
ext_{N} : (α → βN) → αN → βN  pext : (α → βNM) → αN → βNM
ext_{N} g = g ⊙_{N} id  pext g = g ⊙_{NM} unit_{M}
g ⊙_{N} f = ext_{N} g ∘ f  g ⊙_{NM} f = pext g ⊙_{M} f
join_{N} = ext_{N} id  kjoin= pext unit_{M}
map_{N} f = ext_{N} (unit_{N} ∘ f)  kmap f = pext (unit_{NM} ⊙_{M} f)
ext_{N} f = join_{N} ∘ map_{N} f  pext f = kjoin ⊙_{M} kmap f
h ⊙_{N} f = (h ⊙_{N} id) ∘ f  h ⊙_{NM} f = (h ⊙_{NM} unit_{M}) ⊙_{M} f

2006 16

To show NM is a monad, using the pext rules

f ⊙_{NM} unit_{NM} = f  (A1K)
unit_{NM} ⊙_{NM} f = f  (A2K)
h ⊙_{NM} (g ⊙_{NM} f) = (h ⊙_{NM} g) ⊙_{NM} f  (A3K)
(h ⊙_{NM} unit_{M}) ⊙_{M} f = h ⊙_{NM} f  (A4K)

To show NM is a monad, want namely (A1NM) to (A4NM). But (A1NM) to (A3NM) same as (A1K) to (A3K); only (A4NM) is different. So need only (A4NM); to get it, have both (A4K) and (A4M).

(h ⊙_{NM} id) ∘ f = h ⊙_{NM} f  (A4NM)
(h ⊙_{M} id) ∘ f = h ⊙_{M} f  (A4M)
(h ⊙_{NM} id) ∘ f = ((h ⊙_{NM} unit_{M}) ⊙_{M} id) ∘ f  (A4K)
= (h ⊙_{NM} unit_{M}) ⊙_{M} f = h ⊙_{NM} f  (A4M, A4K)

2006 17

What characterises such compound monads?

Such compound monads NM satisfy

ext_{NM} f = ext_{M} (pext f)  (EC)
pext f = ext_{NM} f ∘ unit_{M}  (PE)
ext_{M} (ext_{NM} f) = ext_{NM} f ∘ join_{M}  (J1S)

Note, (J1S) of the form of Theorem 1(i). Conversely, if M and NM are monads, and (J1S) holds, then ⊙_{NM} also defines a monad in K_{M}, and, using (PE) to define pext, (EC) holds. Proof uses that (A1K) to (A3K) same as (A1NM) to (A3NM); shows (A4K) and (EC) from (J1S) using Theorem 1.

2006 18

A more general set of rules

Three more functions of the following types:

dunit : αM → αNM
dmap : (α → βM) → (αNM → βNM)
djoin : αNNM → αNM
dmap unit_{M} = id  (G1)
dmap (f ∘ h) = dmap f ∘ map_{NM} h  (G2)
dmap f ∘ unit_{NM} = dunit ∘ f  (G3)
djoin ∘ dmap (dmap f) = dmap f ∘ join_{NM}  (G4)
djoin ∘ dunit= id  (G5)
djoin ∘ dmap unit_{NM} = id  (G6)
djoin ∘ dmap djoin = djoin ∘ join_{NM}  (G7)
ext_{NM} f = djoin ∘ dmap f  (G8)

2006 19

These also give a monad NM

Theorem 3 Assume rules (G1) to (G8). Then ext_{NM}, join_{NM}, map_{NM} and unit_{NM} give a monad NM, where also

djoin = ext_{NM} unit_{M}  (G9)
dmap f = ext_{NM} (dunit ∘ f)  (G10)
unit_{NM} = dunit ∘ unit_{M}  (G11)
map_{NM} f = dmap (unit_{M} ∘ f)  (G12)

Conversely, for a compound monad NM, when is this construction applicable? Theorem 4 Assume that NM is a monad. Also assume that rules (G5) and (G9) to (G11) hold. Then the remaining rules among (G1) to (G8) hold.

2006 20

When is the construction applicable?

How to use Theorem 4? Assume (UC).

unit_{NM} f = unit_{M} (unit_{N} f)  (UC)
dunit= map_{M} unit_{N}  (DU)
ext_{NM} unit_{M} ∘ map_{M} unit_{N} = id  (G5′)

If (J1S) and the pext construction hold, then define functions dunit, dmap and djoin by (DU), (G10) and (G9). Then (G11) holds by (3M), and (G5) becomes (G5′) which holds: the proof uses ext_{NM} f = ext_{M}(pext f). So Theorem 4 applies.

2006 21

On the other hand …

ext_{NM} (map_{M} join_{N}) = map_{M} join_{N} ∘ join_{NM}  (J2′)

Note (J2′) is also of the form of Theorem 1(i). If N is a monad and M a premonad, and (J2′) holds, then ext_{NM} unit_{M} = map_{M} join_{N} (proved from Theorem 1). In this case (G5)/(G5′) also hold, by a seemingly different proof.

ext_{NM} unit_{M} ∘ map_{M} unit_{N} = map_{M} join_{N} ∘ map_{M} unit_{N}

= map_{M} (join_{N} ∘ unit_{N}) = map_{M} id = id

So again Theorem 4 applies. Common feature: ext_{NM} unit_{M} is of the form ext_{M} f, so Theorem 1 applies.

2006 22

When both (J1S) and (J2′) hold

If both (J1S) and (J2′) hold, and both M and N are monads, then we have a distributive law for the monads M, N and NM.

2006 23