Compound Monads and the Kleisli Category

Jeremy E. Dawson ^{⋆}

Logic and Computation Program, NICTA ^{⋆⋆} and Computer Sciences Laboratory, Australian National University, Canberra, ACT 0200, Australia

        Jeremy.Dawson@nicta.com.au  http://csl.anu.edu.au/^{∼}jeremy/

Abstract. We consider sets of monad rules derived by focussing on the Kleisli category of a monad, and from these we derive some constructions for compound monads. Under certain conditions these constructions correspond to a distributive law connecting the monads. We also show how these relate to some constructions for compound monads described previously. Keywords: compound monad, Kleisli category

1 Introduction

Monads are convenient for structuring functional programs. For example, an algorithm requiring use of a mutable state may be coded in a purely functional style using the state monad, or an algorithm involving some non-deterministic steps may be conveniently coded using the list monad. Moggi [7] shows how to describe computational activity in terms of monads. Wadler [8] shows in particular how it is easy to change a program to introduce these features if it is written in a monadic style. However, to code (equally conveniently) a program involving both these aspects requires a monad which somehow combines both the state and the list monads.

A monad consists of a type constructor and several functions (of appropriate types), which must satisfy certain rules. There are several equivalent formulations of these rules. Once we have defined the type constructor for a compound monad, it is necessary to prove the rules for the compound monad, as they do not follow automatically from the rules for the individual monads. It is important to establish that the rules hold, since to use a type constructor wrongly thought to be a monad can lead to incorrect programs – two ways of coding a function, which are thought to be equivalent, may be different. Yet the constructions can be complex, leading to errors in proofs, for example see [3, §6.4.2].

⋆ Supported by an Australian Research Council Large Grant ⋆⋆ National ICT Australia is funded by the Australian Government’s Dept of Commu-

nications, Information Technology and the Arts and the Australian Research Council through Backing Australia’s Ability and the ICT Research Centre of Excellence programs.

A monad is a category theoretic notion, and we focus on sets of rules relating to the Kleisli category of a monad, and show how these facilitate proofs of the monad rules for some compound monads.

In the rest of this section we introduce monads and the category theory that we use in the rest of the paper. In section 2 we give several sets of rules, and prove some useful results about monads. and in Appendix B we give examples of the easy use of some of these rules to certain compound monads. In section 3 we describe two constructions which are useful in defining a compound monad, and we set out the rules which must be satisfied in each case. We show how one of these constructions amounts to defining a monad in the Kliesli category of another monad. In Appendix A we show how the constructions of Jones & Duponcheel [3] are cases of ours. Section 4 concludes.

The results of this paper have been proved using the theorem prover Is-

abelle/HOL. The proofs are at http://users.rsise.anu.edu.au/^{∼}jeremy/

isabelle/monad/. While most of the proofs are not difficult, much of the work involved showing the equivalence of different sets of axioms. In this regard the “book-keeping” aspect of using a theorem prover, to keep track of which results are being assumed, and which proved, at a particular point, was of great value.

1.1 Monads

A monad is a type constructor M (which we write postfix) together with functions of the types given below, which must satisfy certain rules. If we loosely say “M is a monad”, this refers also to associated functions which will be either clear from the context, or have the names used below. Where several monads are involved, we may use subscripts to avoid ambiguity in the names of these functions. For the names of monad rules we write (for example) (E2N) to mean rule (E2) for the monad N, that is, ext_{N} unit_{N} = id.

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

This set of functions is not minimal, they are related by the rules shown below. Note that id and ∘ denote the identity function and function composition respectively, and that bind and ⊙ are written in infix notation. (Infix operators have a lower precedence than function application).

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

For M and the functions to qualify as a monad, a set of rules must be satisfied. Several sets of rules have been given. Firstly, when the functions unit, map and join are given, rules (1) to (7) must be satisfied. This is the “monoid form” presentation of an algebraic theory of Manes [6, Chapter 1, Definition 3.17]. A premonad satisfies rules (1) to (3).

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)

Then (8) defines ext in terms of join and map. At this point it is convenient to note rule (9), which clearly follows from (8) and (2).

Alternatively, a monad can be defined in terms of unit and ext. Wadler [8] shows the equivalence to analogues (in terms of bind) of rules (E1), (E2) and (E3′), which are given by Moggi [7]. This is also the “extension form” presentation of an algebraic theory of Manes [6, Chapter 1, §3, Exercise 12].

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)

If a monad is defined by giving unit, map and join, satisfying the rules (1) to (7), and if ext is defined by (8), then rules (E1), (E2), (E3′), (E4) and (E5) hold. Conversely, if a monad is defined by giving unit and ext, satisfying rules (E1), (E2) and (E3′), and if join and map are defined by (E4) and (E5), then the rules (1) to (8) hold. (Wadler states the analogous result for the formulation of rules (E1), (E2) and (E3′) in terms of bind.)

1.2 Some Category Theory

Monads have been known (sometimes under different names) as part of category theory before their use in describing computations, eg [5, 6]. A category consists of a collection of objects and a collection of arrows. Each arrow f has a source object s(f) and a target object t(f). Two arrows f and g, such that t(f) = s(g), can be composed to give another arrow which we write g ∘ f, with source s(f) and target t(g). Composition of arrows is associative. For each object α there is an identity arrow id_{α}, such that id_{α} ∘ f = f = f ∘ id_{α}. See [5] for more details.

Clearly then, if we let the objects be types (eg, α, β), and the arrows functions, such as f : α → β, we have a category T , where s(f) = α and t(f) = β.

A functor from one category to another (or to the same category) is a mapping θ which takes objects to objects and arrows to arrows, and preserves

– the sources and targets of arrows, ie s(θf) = θ(s(f)) and t(θf) = θ(t(f))

– composition of arrows, ie θ(g ∘ f) = θg ∘ θf

– identity arrows, ie θ(id_{α}) = id_{θ(α)}

If M and map satisfy the type information in §1.1 and the rules (1) and (2), then M and map give a functor θ from the category of types and functions to itself, where θ(α) = αM and θ(f) = map f. (By an abuse of terminology we will often refer to the action of a function on arrows, such as map, or ext or kl below, as a “functor”).

However there is another interesting category associated with a monad, namely the Kleisli category K_{M} (see [5, ChVI, §5]). We describe it in functional programming terms. Its objects are the types (eg, α, β), but an arrow with source α and target β is a function of type α → βM. The identity for object α is the function unit : α → αM, and composition is the function ⊙. There is a functor from the “ordinary” category T of types and functions to the Kleisli category K_{M}. We call it kl (“Kleisli lift”) and define its action (on arrows) by

kl : (α → β) → (α → βM)
kl f = unit ∘ f

The function ext is a functor from K_{M} to T (on objects, the functor takes a type α to the type α M), and we may note that the rule (E5) tells us that the composition of the functors ext and kl is the functor map. See [5, ChVI, §5, Theorem 1] for these results.

2 Axioms for a Single Monad

2.1 A Weaker Set of Monad Rules

First we give a set of monad rules (E1) to (E3) which is similar to those in §1.1, but replacing (E3′) by (E3). Note also that (E2) and (E3) express the fact that ext is a functor. Rule (E3) is apparently easier to satisfy than (E3′) since we may choose ⊙ arbitrarily: if we add to (E3) the extra requirement of (E6) then we get (E3′). But in fact (E6) can be proved from rules (E1) and (E3).

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

In fact we can prove (E6), identity and associativity in the Kleisli category, and some other useful results, from rules (E1) to (E3).

Theorem 1. 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)

Proof. (E6): By (E3), ext (g ⊙ f) ∘ unit = ext g ∘ ext f ∘ unit. Using (E1),

this simplifies to g ⊙ f = ext g ∘ f. (EI): If ext f = ext g then ext f ∘ unit = ext g ∘ unit, that is, by (E1), f = g. (A6): Using (E6), both sides are equal to ext h ∘ g ∘ f. (A1,A2,A3): One proof of these would proceed by rewriting these, using (E6)

and (E3), to eliminate all uses of ⊙. Then they follow from (E1), (E2) and the associativity of ∘ (since both sides of (A3) become ext h ∘ ext g ∘ f ). But another proof which better reflects our focus on categories and functors is to observe that in each case, by (EI), it suffices to prove ext(lhs) = ext(rhs). In each case, this may be proved using the fact that ext is a functor, ie, using (E3) and (E2). That is, we use the identity and associativity rules for id and ∘ to prove the corresponding rules for unit and ⊙. for (A1): ext (f ⊙ unit) = ext f ∘ ext unit = ext f ∘ id = ext f for (A2): ext (unit ⊙ f) = ext unit ∘ ext f = id ∘ ext f = ext f for (A3): ext (h ⊙ (g ⊙ f)) = ext h ∘ (ext g ∘ ext f) =

(ext h ∘ ext g) ∘ ext f = ext ((h ⊙ g) ⊙ f) ⊓ ⊔

The following theorem is useful later.

Theorem 2. 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

Proof. (i) ⇒ (ii): Assume (i). Then ext g ∘ map unit = g ∘ join ∘ map unit and

so, by (9) and (6), ext (g ∘ unit) = g. (ii) ⇒ (iii): is obvious. (iii) ⇒ (iv): When g = ext f, (iv) is just (E3′). (iv) ⇒ (i): Set h = id and use (E4). (iv) ⇒ (ii): Set h = unit and use (E2). ⊓ ⊔

Note also that in a monad, these properties of g are preserved under composition, that is, if they hold for g_{1} and g_{2} then they hold for g_{1} ∘ g_{2}. This can be seen for (iii) from (E3), or for (i) from (8) and (9).

Finally, we include a proof that kl is a functor [5, ChVI, §5].

Theorem 3. kl is a functor.

Proof. Clearly kl preserves identity: kl id = unit ∘ id = unit. For composition:

kl g ⊙ kl f = (unit ∘ g) ⊙ (unit ∘ f)
= ((unit ∘ g) ⊙ unit) ∘ f  (A6)
= (unit ∘ g) ∘ f = kl (g ∘ f)  (A1) □

From rules (E1) to (E3), and so (E6), we have (E3′), and so, assuming (E4) and (E5) as definitions, we can therefore assume rules (1) to (8) (Wadler[8, §2.10]). However it is now easy to outline proofs of rules (1) to (8). Using (E4) and (E5), (8) is proved using (E3′) and (E1). Using (8), (6) is just (E2). Using (8), then (E5) and (E4) respectively, (4) and (7) are special cases of Theorem 2, (iii) ⇒ (i). Using (E5) and (E4) respectively, (3) and (5) are cases of (E1). Finally, as noted earlier, (E5) shows that map = ext ∘ kl. As ext and kl are functors, so is map, which gives us (1) and (2).

2.2 Monad Rules Based on the Kleisli Category

We have proved the three rules, (A1) to (A3), which reflect that the Kleisli category is indeed a category. We may ask whether these are sufficient to establish a monad. If we could assume also (E6), then it would be easy to show rules (E1) to (E3). However, if we are (hoping to) define a monad in terms of these rules, and in terms of the functions unit and ⊙, then we can take (A5) as a definition, but that does not give us (E6).

If we add a fourth rule, (A4) (see below), governing ⊙, then that is sufficient. For, clearly, (A4) and (A5) imply (E6). Note that (A4) is the special case g = id of (A6) (shown again below) and is therefore true in any monad, see Theorem 1. Therefore we have the following theorem. Note that, if we replaced (A4) by (A4′), we would get, in effect, the “clone form” presentation of an algebraic theory of Manes [6, Chapter 1, Definition 3.2]. In fact it is easy to show (A6) directly from either (A4) or (A4′) using the associativity of ∘ or ⊙ respectively.

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)

Theorem 4. Rules (A1) to (A4) and definitions (A5), (E4), (E5) give a monad.

In Appendix B are some examples showing how easy it often is to prove the monad rules when using rules (A1) to (A4). These include two examples of compound monads, formed by starting with a monad M and developing a more complex monad from it.

2.3 A Free Theorem

In the examples in Appendix B it is trivial to prove rules (A1) to (A3); in these examples the rule (A4) is the only one of the four whose proof is not quite immediate (that is, although easy, it is tedious, involving several steps). We may therefore ask whether it is really necessary. It turns out that in typical cases it is a “free theorem” (Wadler [9]). We consider it in the “naive set-theoretic” fashion of [9, §2,§3]. The latter sections of that paper indicate the semantic complexities involved in applying such results in a setting such as a typical functional programming language, where the types cannot be regarded as sets. Therefore the application of these results to any particular functional programming language depends on the semantics of that language and its type system. First, we state a more general result. In category theoretic terms, this result it that θ is a natural transformation between the functors ( → β) and ( → γ).

Proposition 5. If θ : ∀α. (α → β) → (α → γ) is a function which is polymorphic in α, but where β and γ are fixed types, then

(i) there exists h : β → γ such that (for all f : α → β) θf = h ∘ f (ii) for all f : α → α′ and g : α′ → β, θ (g ∘ f) = θ g ∘ f

The result (i) may be explained intuitively as follows. Since θ is polymorphic in α, the coding of the function θ cannot use any information about the type α. That is, although an argument a : α to the function θf may be an integer, tree of strings, or whatever, θ (on its own) can only treat a as a “black box”. So the only thing that θf can do with a (other than ignore it) is to apply f to it.

Wadler [9, §3] shows how to obtain results of this nature about particular polymorphic functions, and we follow his approach. In particular, we write the proof as though types were sets.

Proof. Clearly the two parts are equivalent (h being θ id). We prove (ii). Wadler’s general result is θ ∼ θ, where ∼ denotes the relation appropriate to the type of the terms related, which, for θ, is ∀α. (α → β) → (α → γ). This means that for all α, α′ and relation ∼ ⊆ α × α′, for all k : α → β, k′ : α′ → β, a : α and a′ : α′, whenever k ∼ k′ and a ∼ a′, then θ k a ∼ θ k′ a′. Now k ∼ k′ means whenever x ∼ x′, for x : α and x′ : α′, then k x ∼ k′ x′.

We choose the relation ∼ ⊆ α × α′ to be a ∼ a′ ⟺ a′ = f a; the relations on (fixed) types β and γ are the identity. So we can simplify the above. We get k ∼ k′ iff, for all x : α, k x = k′ (f x), that is, k = k′ ∘ f. Then, letting k′ = g and k = g ∘ f, we have k ∼ k′. So for all a : α, we can let a′ = f a, so a ∼ a′ and θ k a ∼ θ k′ a′, that is, θ (g ∘ f) a = θ g (f a). Therefore, θ (g ∘ f) = θ g ∘ f. ⊓ ⊔

Proposition 6. Assuming that ⊙ : (β → γM) → (α → βM) → (α → γM) is polymorphic in α, the rule (A6) holds.

Proof. Given h : β → γM, define θ g ≡ h ⊙ g. Then Theorem 5(ii) gives h ⊙ (g ∘ f) = (h ⊙ g) ∘ f, as required. ⊓ ⊔

3 Compound Monad Constructions

If type constructors M and N, with associated functions, are monads, then although it is not necessarily the case that we can combine these two monads to form a third, this is sometimes possible.

Compound monads can arise naturally and be practically useful ([8], [3]). In this section we consider two constructions for compound monads and discuss the rules that need to be satisfied in each case. We note that when the conditions are satisfied for both constructions to be applicable, then we have the distributive law for monads described by Manes [6] and Barr & Wells [1]: see §3.8. In this case the monads are “compatible” [1, §9.2], and our results show how some of the conditions given in [1] for this are redundant.

3.1 Compound Monads via Partial Extension

Let M be a monad, and consider compound monads where the compound monad type is (αN)M, which we will just write as αNM. To define a compound monad NM, we will need a function ext_{NM}, so-called, presumably, because it “extends” a function f from a “smaller” domain, α, to a “larger” one, αNM. Consider, therefore, a “partial extension” function pext which does part of this job:

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

Rules (E1K) to (E3K) are sufficient to define a compound monad using such a function pext. We assume nothing about the functions ⊙_{NM} or unit_{NM}, except that they have the appropriate types. We need not assume that N is a monad, although in many examples rules (E1K) to (E3K) are proved to hold for any monad M, when setting M to the identity monad gives a monad N.

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)

By comparing (E1K) to (E3K) with (E1) to (E3) we see that we have the three rules needed for a monad N in K_{M}, the Kleisli category of M. We will refer to this monad as N_{KM}. Thus the treatment of a single monad described in §1, §2.1 and §2.2 applies to this monad. We define the counterparts of map and join, calling them kmap and kjoin: note how rules (E4K) and (E5K) correspond to (E4) and (E5). As in §2.1, we deduce (E6K), giving ⊙_{NM} in tems of pext. The various functions and theorems involved have counterparts of which examples are tabulated below, where the left-hand side shows the standard treatment (set out as for a monad N), and the right-hand side shows the monad N_{KM} 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

We will refer to the rules and results about this monad by putting “K” after the names used in §1 and §2. We also obtain rules (1K) to (8K) which are the counterparts of (1) to (8). Then, just as in §1, these seven rules, with pext and ⊙_{NM} defined from kjoin and kmap by (8K) and (E6K), are sufficient to show rules (E1K) to (E3K) and the converse definitions of kjoin and kmap in terms of pext, (E4K) and (E5K).

This monad N_{KM} in K_{M}, the Kleisli category for M, gives rise to a further Kleisli category, which we may describe as the Kleisli category for N_{KM} in K_{M}. Its identity is unit_{NM} and its composition function is ⊙_{NM} . Note also that the two rules (E2K) and (E3K) express the fact that pext is (the action on arrows of) a functor, from this compound Kleisli category to K_{M}.

kmap unit_{M} = unit_{M}  (1K)
kmap f ⊙_{M} kmap g = kmap (f ⊙_{M} g)  (2K)
unit_{NM} ⊙_{M} f = kmap f ⊙_{M} unit_{NM}  (3K)
kjoin ⊙_{M} kmap (kmap f) = kmap f ⊙_{M} kjoin  (4K)
kjoin ⊙_{M} unit_{NM} = unit_{M}  (5K)
kjoin ⊙_{M} kmap unit_{NM} = unit_{M}  (6K)
kjoin ⊙_{M} kmap kjoin = kjoin ⊙_{M} kjoin  (7K)
pext f = kjoin ⊙_{M} kmap f  (8K)

This monad can also be characterised by four rules analogous to (A1) to (A4): that is, the rules (A1K) to (A4K). We also show (A5K) and (A6K).

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)
pext g = g ⊙_{NM} unit_{M}  (A5K)
(h ⊙_{NM} g) ⊙_{M} f = h ⊙_{NM} (g ⊙_{M} f)  (A6K)

Now, to show that NM is a compound monad, we also need to show four rules analogous to (A1) to (A4), namely (A1NM) to (A4NM). Of these, the first three, (A1NM) to (A3NM), are the same as (A1K) to (A3K); only (A4NM) is different. So to show that NM (defined by unit_{NM} and ⊙_{NM} ) is a monad, we need only show (A4NM), and to do this we have available both (A4K) and (A4M).

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

Theorem 7. Assume that M is a monad and that functions pext, ⊙_{NM} and unit_{NM} of the appropriate types are given, satisfying rules (E1K) to (E3K). Then ⊙_{NM} and unit_{NM} define a monad, and, using (A5NM) to define ext_{NM},

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)

Proof. Rules (E1K) to (E3K) establish that pext, ⊙_{NM} and unit_{NM} define a monad in K_{M}, and so rules (A1K) to (A4K) are satisfied. Since M is a monad, (A4M) holds, and so we use (A4M) and (A4K) to show (A4NM) as follows:

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

(EC): By (A5M) and (A5NM) this is (E6K). (PE): By (E6NM) this is (A5K). (J1S): By Theorem 2 for M, (iii) ⇒ (i), this follows from (EC). ⊓ ⊔

In Theorem 7 we proved rules (A1) to (A4) for NM, so proving that NM is a monad. However, we note that it is also trivial to prove rules (E1) to (E3) for NM. In fact, using (EC), each rule for NM follows from the same rule for M and the corresponding rule from among (E1K) to (E3K).

We may next ask which compound monads can be constructed from such a function pext, satisfying rules (E1K) to (E3K). Taking as read the requirement that the monadic type is (αN)M, (which we will regard as implicit in the notation NM), the previous theorem provides a necessary condition, namely that (J1S) holds. In fact, this condition is also sufficient.

Theorem 8. Let M and NM be monads, such that (J1S) (see Theorem 7) holds. Then ⊙_{NM} also defines a monad in the category K_{M}, and, using (PE) to define pext, (EC) holds.

Proof. We need to show that ⊙_{NM} satisfies the four rules (A1K) to (A4K). Now (A1K) to (A3K) are the same as (A1NM) to (A3NM), which hold as NM is a monad. So we need only (A4K), which we show follows from (J1S).

(h ⊙_{NM} unit_{M}) ⊙_{M} f = ext_{M} (ext_{NM} h ∘ unit_{M}) ∘ f  (E6NM, E6M)
= ext_{M} (ext_{NM} h) ∘ map_{M} unit_{M} ∘ f  (9M)
= ext_{NM} h ∘ join_{M} ∘ map_{M} unit_{M} ∘ f  (J1S)
= ext_{NM} h ∘ f = h ⊙_{NM} f  (6M, E6NM)

Then NM is a monad in which pext is defined by (A5K); but, by (E6NM), this is equivalent to (PE). Then (EC) follows from Theorem 7 (alternatively, from (J1S) by Theorem 2 for M, (i) ⇒ (ii)). ⊓ ⊔

This shows that, given a monad M, that the compound monads NM obtainable using the construction via a monad N in K_{M} are precisely the monads NM such that (J1S) is satisfied.

3.2 Relation to the prod construction of Jones & Duponcheel

We have, in Theorems 7 and 8, shown that the compound monads which can be defined in terms of a function pext (equivalently, in terms of functions kjoin and kmap) are precisely those satisfying (J1S).

Jones & Duponcheel [3] consider only compound monads which satisfy (UC) and (MC). Note that, as shown in [3, §3], when M and N are premonads and (UC) and (MC) hold, then NM is a premonad. Assuming that M is a monad and that N is a premonad, they show how to define a compound monad given a function prod, satisfying four rules P(1) to P(4) (see Appendix A.1), and show that the compound monads NM which can be defined using prod are precisely those satisfying (J1) (equivalently, (J1′)), which is the case f = id of (J1S). In fact (MC) and (J1) are sufficient to imply (J1S). We also give a condition (E1D), which is also implied by (MC) and its case f = id, and which, assuming (UC), is equivalent to (J1S). The proof of (J1S) from (E1D) is thanks to an observation by Michael Barr (see §3.8).

unit_{NM} f = unit_{M} (unit_{N} f)  (UC)
map_{NM} f = map_{M} (map_{N} f)  (MC)
join_{M} ∘ map_{M} join_{NM} = join_{NM} ∘ join_{M}  (J1)
ext_{M} join_{NM} = join_{NM} ∘ join_{M}  (J1′)
ext_{NM} f ∘ map_{M} unit_{N} = ext_{M} f  (E1D)
join_{NM} ∘ map_{M} unit_{N} = join_{M}  (E1DI)

Lemma 9. If M and NM are monads, then

(i) (MC) and (J1) imply (J1S) (ii) (MC) and (E1DI) imply (E1D) (iii) assuming (UC), (J1S) and (E1D) are equivalent.

Proof. (i) By Theorem 2 for M, (i) ⇒ (iii), we can assume, from (J1), that join_{NM} = ext_{M} g. By Theorem 2, (iii) ⇒ (i), for any given f, it is enough to find h such that ext_{NM} f = ext_{M} h.

ext_{NM} f = join_{NM} ∘ map_{NM} f  (8NM)
= ext_{M} g ∘ map_{M} (map_{N} f)  (MC)
= ext_{M} (g ∘ map_{N} f)  (9M)

(ii) Assuming (E1DI),

ext_{NM} f ∘ map_{M} unit_{N} = join_{NM} ∘ map_{NM} f ∘ map_{M} unit_{N}  (8NM)
= join_{NM} ∘ map_{M} (map_{N} f ∘ unit_{N}) (MC, 2M)
= join_{NM} ∘ map_{M} unit_{N} ∘ map_{M} f (3N, 2M)
= join_{M} ∘ map_{M} f = ext_{M} f  (E1DI, E4M)

(iii) Let (J1S) hold; we show (E1D). Using Theorem 2 for NM, (i) ⇒ (ii),

ext_{NM} f ∘ map_{M} unit_{N} = ext_{M} (ext_{NM} f ∘ unit_{M}) ∘ map_{M} unit_{N}
= ext_{M} (ext_{NM} f ∘ unit_{M} ∘ unit_{N})  (9M)
= ext_{M} (ext_{NM} f ∘ unit_{NM}) = ext_{M} f (UC, E1NM)

Now, suppose that (E1D) holds; we show (J1S). Noe how (E1D) is used twice here.

ext_{M}(ext_{NM} f) = ext_{NM} (ext_{NM} f) ∘ map_{M} unit_{N}  (E1D)
= ext_{NM} f ∘ ext_{NM} id ∘ map_{M} unit_{N}  (E3′NM)
= ext_{NM} f ∘ ext_{M} id = ext_{NM} f ∘ join_{M} (E1D, E4M)

Thus the pext construction is applicable whenever the prod construction is, and the converse is true if we can assume that (UC) and (MC) hold. We give another useful lemma.

Lemma 10. Assume NM is constructed as in §3.1. Then each of the following is equivalent to (MC):

pext (g ∘ f) = pext g ∘ map_{N} f  (PO)
kmap (g ∘ f) = kmap g ∘ map_{N} f  (KO)

and each of the following is equivalent to (UC):

pext f ∘ unit_{N} = f  (E1K′)
ext_{NM} f ∘ map_{M} unit_{N} = ext_{M} f  (E1D)

Proof. Using (PE) and (MC), the following gives (PO).

ext_{NM} (g ∘ f) ∘ unit_{M} = ext_{NM} g ∘ map_{NM} f ∘ unit_{M}  (9NM)
= ext_{NM} g ∘ unit_{M} ∘ map_{N} f  (MC,3M)

(PO) ⇒ (KO) : kmap (g ∘ f) = pext (unit_{NM} ⊙_{M} g ∘ f) (E5K, A6M)
= pext (unit_{NM} ⊙_{M} g) ∘ map_{N} f  (PO)
= kmap g ∘ map_{N} f  (E5K)

Since pext g = kjoin ⊙_{M} kmap g by (8K), (KO) implies (PO) by (A6).

(PO) ⇒ (MC) :
map_{NM} g = ext_{NM} (unit_{NM} ∘ g)  (E5NM)
= ext_{M} (pext (unit_{NM} ∘ g))  (EC)
= ext_{M} (pext unit_{NM}) ∘ map_{M} (map_{N} g)  (PO, 9M)
= map_{M} (map_{N} g)  (EC, E2)
(E1K′):  pext f ∘ unit_{N} = pext f ⊙_{M} (unit_{M} ∘ unit_{N})  (A4′M)
= pext f ⊙_{M} unit_{NM} = f  (UC, E1K)
(E1D): ext_{NM} f ∘ map_{M} unit_{N} = ext_{M} (pext f) ∘ map_{M} unit_{N} (EC)
= ext_{M} (pext f ∘ unit_{N}) = ext_{M} f  (9M, E1K′) □

(E1K′) ⇒ (UC): set f = unit_{NM} and use (E1K)

(E1D) ⇒ (E1K′) :
pext f ∘ unit_{N} = ext_{M} (pext f ∘ unit_{N}) ∘ unit_{M}  (E1)
= ext_{NM} f ∘ map_{M}unit_{N} ∘ unit_{M}  (9M, EC)
= ext_{M} f ∘ unit_{M} = f  (E1D, E1)

Then the relationships between prod and pext are given by these equalities, which are equivalent when (PO) and (1N) hold. See Appendix §A.1 for details.

prod = pext id  pext f = prod ∘ map_{N} f

3.3 Lifting monad N to K_{M}

By a lifting of one monad to another (maybe in different categories) we understand a functor F which is also a functor between their Kleisli categories. We consider whether the monad N_{KM} in the Kleisli category K_{M} is a lifting of the monad N. This would require

F id = unit_{M}  (LI)
F (g ∘ f) = F g ⊙_{M} F f  (LO)
F unit_{N} = unit_{NM}  (LU)
F (g ⊙_{N} f) = F g ⊙_{NM} F f  (LA)

Instead of (LA), we may use (LE), or (LM) and (LJ).

F (ext_{N} f) = pext f  (LE)
F (map_{N} f) = kmap f  (LM)
F join_{N} = kjoin  (LJ)

Assuming (UC), F = kl, where kl f = unit_{M} ∘ f satisfies (LI), (LO) and (LU).

With F = kl, note that (LJ) is just (KJ) of Theorem 14, and, indeed, kl is a lifting if and only if (J2) (see §3.5) holds.

3.4 A generalisation of earlier axiom systems

We now present a generalisation of the system of axioms (1) to (8), and their equivalence to (E1) to (E5). This was motivated by the construction by Jones & Duponcheel [3, §3.3] using their function dorp (see §3.5).

We found that the rules (G1) to (G8), which are analogous to rules (1) to (8), are sufficient to establish that NM is a monad, without assuming that either N or M is even a premonad. In these rules, we make no assumptions about the functions we call ext_{NM}, join_{NM}, map_{NM}, unit_{NM} or unit_{M}.

These rules also use 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)

Theorem 11. 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)

Proof. We prove rules (E1), (E2), (E3′), (E4) and (E5) for NM; this proof corresponds almost step-by-step to the proof of these rules from (1) to (8).

(E1NM): use (G8), (G3) and (G5). (E2NM): use (G8) and (G6). (E4NM): use (G8), (G4) and (G1). (9NM): use (G8) and (G2). (8NM): use (E4NM) and (9NM). (E5NM): use (9NM) and (E2NM). (G9): use (G8) and (G1). (G11): use (G3) and (G1). (G12): use (G2) and (G1).

(G10): ext_{NM} (dunit ∘ f) = ext_{NM} (dmap f ∘ unit_{NM})  (G3)
= ext_{NM} (dmap f) ∘ map_{NM} unit_{NM}  (9NM)
= dmap f ∘ join_{NM} ∘ map_{NM} unit_{NM} (G8, G4)
= dmap f  (8NM, E2NM)
(E3′NM):  ext_{NM} (ext_{NM} g ∘ f)
= djoin ∘ dmap (djoin ∘ dmap g ∘ f)  (G8)
= djoin ∘ join_{NM} ∘ map_{NM} (dmap g ∘ f) (G2, G7)
= djoin ∘ djoin ∘ dmap (dmap g ∘ f)  (8NM, G8)
= djoin ∘ dmap g ∘ join_{NM} ∘ map_{NM} f  (G2, G4)
= ext_{NM} g ∘ ext_{NM} f  (G8, 8NM) □

The following converse result tells us when a monad NM can be defined in this way. Note that we are still not assuming that M or N is a monad.

Theorem 12. 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.

Proof. (G1): use (G10), (G11) and (E2NM). (G2): use (G10) and (9NM). (G3): use (G10) and (E1NM). (G8): use (G9), (G10), (E3′NM) and (G5). (G6): use (G8) and (E2NM). (G4)/(G7): use (G8), Theorem 2 for NM, (iii) ⇒ (i), and (G10)/(G9). ⊓ ⊔

Given a monad NM, we consider when it can be constructed using Theorem 11. First we note that if NM is constructed as in §3.1, and (UC) holds, then we can define functions dunit, dmap and djoin by (DU), (G10) and (G9). Then (G11) holds by (3M), and (G5) becomes (G5′) which holds by (E1D) (see Lemma 10) and (E2M). Thus Theorem 12 holds.

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

3.5 Relation to the dorp construction of Jones & Duponcheel

Jones & Duponcheel [3] also show how to define a compound monad using a function dorp, satisfying four rules D(1) to D(4) (see Appendix A.2), and, assuming (UC) and (MC) and that M is a premonad and N is a monad, show that the compound monads which can be defined using dorp are precisely those satisfying (J2) (equivalently, (J2′)). We show corresponding results about when a compound monad can be constructed using (G1) to (G8).

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

We first relate (J2) to the conditions of Theorem 12.

Lemma 13. Assume that NM is a monad, that M is a premonad and N is a monad, and that (UC) holds. Then (J2) (equivalently, (J2′)) holds if and only if ext_{NM} unit_{M} = map_{M} join_{N}.

Proof. ⇐: by Theorem 2 for NM, (iii) ⇒ (i).

⇒: by applying Theorem 2, (i) ⇒ (ii), to (J2′), gives

map_{M} join_{N} = ext_{NM} (map_{M} join_{N} ∘ unit_{NM})
= ext_{NM} (map_{M} join_{N} ∘ unit_{M} ∘ unit_{N})  (UC)
= ext_{NM} (unit_{M} ∘ join_{N} ∘ unit_{N})  (3M)
= ext_{NM} unit_{M}  (6N) □

With the assumptions of Lemma 13, and assuming that (J2) holds, we can define functions dunit, dmap and djoin by (DU), (G10) and (DJ), then (G9), (G11) and (G5) hold, so Theorem 12 applies.

djoin = map_{M} join_{N}  (DJ)
dunit = map_{M} unit_{N}  (DU)

Note that we have shown that either (J1) or (J2) can be used to show that Theorem 12 holds, and so NM can be constructed using Theorem 11. This is related to the interesting fact that the equality (G5′) can be proved using either (J1) or (J2), as it follows easily from (E1D) or from Lemma 13. The same holds of (DJK) (see §3.6).

Finally, if we can define a compound monad NM satisfying (G1) to (G8) by using (DJ) to define djoin, then (G9) holds by Theorem 11, and so (J2) holds.

We can define the function dorp of Jones & Duponcheel [3] in terms of dmap and vice versa, as follows, and get the results relating to D(1) to D(4). See Appendix §A.2 for details.

dorp = dmap id  dmap f = dorp ∘ map_{NM} f

3.6 When both constructions apply

We consider the situation when both the constructions of §3.1 and §3.4 apply, that is when both (J1) and (J2) hold. In this case, we have a distributive law for monads: see §3.8. We collect some results involving both constructions. Note particularly that not all the results require all the assumptions of the theorem. Indeed, it can be seen that if djoin is defined by (G9), then (DJK) has two proofs, as given, one relying on (J1) and one on (J2).

Theorem 14. Assume that NM, M and N are monads, and that (UC), (MC), (J1) and (J2) hold. Define djoin by (G9) or (DJ), dmap by (G10), dunit by (DU), pext by (A5K) or (PE), kjoin by (E4K) and kmap by (E5K). Then

dunit = ext_{M} unit_{NM}  (DUK)
djoin = ext_{M} kjoin  (DJK)
dmap f = ext_{M} (kmap f)  (DMK)
kjoin = unit_{M} ∘ join_{N}  (KJ)

Proof. Note that, by Lemma 13, any two of (J2), (G9) and (DJ) imply the third, and that, by (E6NM), (A5K) holds iff (PE) holds. By Lemma 9(i), (J1S) holds, and so Theorem 8 applies and (EC) holds.

(DUK): Use (DU), (UC) and (E5M).

(DJK): Use (G9), (EC) and (E4K).

(DMK): ext_{M} (kmap f) = ext_{M} (pext (unit_{NM} ⊙_{M} f))  (E5K)
= ext_{M} (pext (dunit ∘ f))  (E6M, DUK)
= ext_{NM} (dunit ∘ f) = dmap f  (EC, G10)
(KJ): kjoin = pext unit_{M} = ext_{NM} unit_{M} ∘ unit_{M}  (E4K, PE)
= map_{M} join_{N} ∘ unit_{M} = unit_{M} ∘ join_{N}  (Lemma 13, 3M)

(DJK): Use (DJ), (E5M) and (KJ) ⊓ ⊔

3.7 Relation to the swap construction of Jones & Duponcheel

Jones & Duponcheel [3] also show how to define a compound monad using a function swap, satisfying four rules S(1) to S(4), (see Appendix A.3), and, assuming (UC) and (MC) and that M and N are monads, show that a compound monad can be defined using swap iff it satisfies (J1) and (J2).

Given a compound monad NM satisfying (J1) and (J2), Lemma 9(i) gives (J1S), and hence, by Theorem 8, NM can be defined using kjoin and kmap. Then, defining swap = kmap id we can prove S(1) to S(4) of [3].

Conversely, given monads M and N and a function swap, we can define kmap in terms of swap as below, but to define the monad NM we also need to define kjoin, which we can do using (KJ).

The relationships between swap and kmap are given by these equalities, which are equivalent when (KO) and (1N) hold. See Appendix §A.3 for more details.

swap = kmap id  kmap f = swap ∘ map_{N} f

3.8 Relation to the distributive law for monads

Manes [6] describes a “distributive law” for monads, at Chapter 4, pages 311-2, Definition 3.6, and page 334, Exercise 6. This is also described by Barr & Wells in [1], §9.2. Under the conditions of Theorem 14, the compound monad is based on a distributive law. The distributive law, (ie, the natural transformation λ of [6] and [1]) is the polymorphic function swap. Further details are in Appendix §A.4.

When NM, M and N are monads, assuming that (MC) holds, Barr & Wells give conditions (C1) to (C5) for NM to be “compatible” with N and M. These are in effect the conditions of Theorem 14, though some of their conditions are redundant. Of their five conditions, condition (C1) is (in effect) (UC). Condition (C5) is (J2), and Lemma 13 shows that it is equivalent to (C2).

Condition (C3) is (E1DI), that is, the case f = id of (E1D), and condition (C4) is (J1), that is, the case f = id of (J1S). These also are equivalent: by Lemma 9, (ii) and (i) these are equivalent to (E1D) and (J1S) respectively, which are equivalent by Lemma 9(iii).

Barr & Wells give these conditions in category theory notation, which reveals a duality between (C2),(C5) on the one hand, and (C3),(C4) on the other. We note how (C4) and (C5), that is, (J1) and (J2), are dual in this sense. Jones & Duponcheel draw attention to a relation between (J1) and (J2), which is that they are each, in effect, of the form of (i) of Theorem 2. This relation seems quite distinct from their duality.

As Michael Barr has observed, the same duality should hold between the proofs (C2) ⇔ (C5) and (C3) ⇔ (C4), when these are written out in the category theory notation (the proof (C3) ⇒ (C4) is thanks to this observation). See Appendix §A.4 for these proofs.

4 Conclusion

By focussing on the Kleisli category of a monad and the functors to and from it we have provided simple proofs of some compound monad constructions. This provided an interesting application of Wadler’s parametricity theorem. We have described a construction which applies to several compound monads which is a functor pext from the Kleisli category of the compound monad NM, into K_{M}, the Kleisli category of M, and we have shown how this is simply a monad in K_{M}. Under further conditions, this construction is is equivalent to the prod construction of Jones & Duponcheel [3]. We have shown how the “map” function of the monad in K_{M} is similarly related to the swap construction of [3]. We developed a set of axioms generalising those of a monad to describe a way of constructing a compound monad which is similarly related to the dorp construction of [3].

Acknowledgements I thank unnamed referees for drawing my attention to the work of Manes and of Barr & Wells on a distributive law for monads, and for alterting me to the semantic issues involved in Propositions 5 and 6.

References

1. Michael Barr and Charles Wells. Toposes, Triples and Theories. Springer-Verlag,

    1983, or see http://www.cwru.edu/artsci/math/wells/pub/ttt.html
 2. Jeremy Dawson. Isabelle proofs: http://users.rsise.anu.edu.au/^{∼}jeremy/
    isabelle/monad/.

3. Mark P. Jones and Luc Duponcheel, Composing Monads, Research Report YALEU/DCS/RR-1004, Yale University, December 1993

4. Sheng Liang, Paul Hudak, and Mark P Jones. Monad Transformers and Modular Interpreters. In Symposium on Principles of Programming Languages (POPL’95), 1995, 333–343.

5. Saunders MacLane. Categories for the Working Mathematician. Graduate Texts in Mathematics, Springer, 1971.

6. Ernest G Manes. Algebraic theories. Graduate Texts in Mathematics, Springer, 1976.

7. Eugenio Moggi. Computational lambda-calculus and monads. In Proceedings of Logic in Computer Science (LICS’89), 1989.

8. Philip Wadler. The Essence of Functional Programming. In Symposium on Principles of Programming Languages (POPL’92), 1992, 1–14.

9. Philip Wadler. Theorems for free! In 4’th International Conference on Functional Programming and Computer Architecture, ACM Press, 1989, 347–359.

A Relation between our constructions and others previously described

In this section we compare our constructions with those of Jones & Duponcheel [3], and also with the distributive law for monads of Manes [6]. and Barr & Wells [1, §9.2].

Throughout this section we assume at least that M and N are premonads, and that we have functions unit_{NM} and map_{NM} for which (UC) and (MC) hold. We note that when N and M are premonads, then (UC) and (MC) give that NM is a premonad [3, §3].

A.1 Relation between the pext construction and the prod construction of Jones & Duponcheel

In this subsection we further assume that M is a monad. Under these assumptions Jones & Duponcheel [3, §3.2,§4.1] show that the compound monads NM which can be defined using prod and the four rules P(1) to P(4) are precisely those satisfying (J1).

prod ∘ map_{N} (map_{NM} f) = map_{NM} f ∘ prod  P(1)
prod ∘ unit_{N} = id  P(2)
prod ∘ map_{N} unit_{NM} = unit_{M}  P(3)
prod ∘ map_{N} join_{NM} = join_{NM} ∘ prod  P(4)

We relate prod to pext, and list other relevant equalities, with an easy lemma relating them.

prod = pext id  (PP1)
pext f = prod ∘ map_{N} f  (PP2)
pext (g ∘ f) = pext g ∘ map_{N} f  (PO)
pext f ∘ unit_{N} = f  (E1K′)

Lemma 15. (i) (PP2) holds iff (PP1) and (PO) hold. (ii) (E1K′) holds iff (E1K) holds. (iii) assuming (PP2), P(2) holds iff (E1K′) holds. (iv) assuming (PP2), P(3) is just (E2K).

Theorem 16. Assume that NM is a compound monad, for which (J1) holds. Use (PE) to define pext, and (PP1) to define prod. Then (J1S) holds, and (PP2), (PO) and P(1) to P(4) hold.

Proof. By Lemma 9(i), (J1S) holds. We now have that Theorems 8 and 7 hold, and Lemma 10 gives (PO), from which (PP2) follows. To prove P(1) and P(4), we use the following result.

pext (ext_{NM} g) = pext (g ⊙_{NM} id)  (A5NM)
= g ⊙_{NM} pext id  (E3K, E6K)
= ext_{NM} g ∘ prod  (E6NM, PP1)

From this we use (PP2), and (E5NM) and (E4NM) respectively, to get P(1) and P(4). Finally, Lemma 15 gives P(2) and P(3). ⊓ ⊔

We note that our definition of prod gives prod = pext id = ext_{NM} id ∘ unit_{M} = join_{NM} ∘ unit_{M} which is the definition used in [3, §4.1].

The following converse theorem is [3, §3.2].

Theorem 17. Let function prod be given, and define join_{NM} by join_{NM} = ext_{M} prod. Let P(1) to P(4) be satisfied. Then NM is a monad, satisfying (J1).

Proof. Define pext using (PP2). Then Lemma 15 gives (PO), (E1K) and (E2K). To define ext_{NM}, we first show the equivalence of two likely definitions.

join_{NM} ∘ map_{NM} f = ext_{M} prod ∘ map_{M} (map_{N} f)  (MC)
= ext_{M} (prod ∘ map_{N} f) = ext_{M} (pext f) (9M, PP2)

So we define ext_{NM} so that (8NM) and (EC) hold, and define ⊙_{NM} using (E6NM), from which (A5NM) follows.

(E3K):  pext (g ⊙_{NM} f) = pext (ext_{NM} g ∘ f)  (E6NM)
= prod ∘ map_{N} (join_{NM} ∘ map_{NM} g ∘ f) (PP2, 8NM)
= join_{NM} ∘ prod ∘ map_{N} (map_{NM} g ∘ f)  (2N, P(4))
= join_{NM} ∘ map_{NM} g ∘ prod ∘ map_{N} f  (2N, P(1))
= ext_{NM} g ∘ pext f  (8NM, PP2)
= ext_{M} (pext g) ∘ pext f = pext g ⊙_{M} pext f (EC, E6M)

Thus Theorem 7 applies and so ext_{NM}, ⊙_{NM} and unit_{NM} are functions of a monad NM. To show that join_{NM} and map_{NM} are the join and map functions of this monad, we need (E4) and (E5) for NM.

Since (E4NM) is clear from (8NM), it remains to show (E5NM).

ext_{NM} (unit_{NM} ∘ f) = ext_{M} (pext unit_{NM} ∘ map_{N} f)  (EC, PO)
= ext_{M} (unit_{M} ∘ map_{N} f)  (E2K)
= map_{M} (map_{N} f) = map_{NM} f  (E5M, MC)

Finally, (J1), and also (J1S), follow from Theorem 2 for M, (iii) ⇒ (i). ⊓ ⊔

A.2 Relation between the dmap construction and the dorp construction of Jones & Duponcheel

In this subsection, as well as assuming that M and N are premonads and that (UC) and (MC) hold, we further assume that M is a monad. Under these assumptions Jones & Duponcheel [3, §3.3,§4.2] show that the compound monads NM which can be defined using dorp and the four rules D(1) to D(4) are precisely those satisfying (J2). We relate dorp to dmap as shown.

dorp ∘ map_{NM} (map_{M} f) = map_{NM} f ∘ dorp  D(1)
dorp ∘ unit_{NM} = map_{M} unit_{N}  D(2)
dorp ∘ map_{NM} unit_{M} = id  D(3)
dorp ∘ join_{NM} = join_{NM} ∘ map_{NM} dorp  D(4)
dorp = dmap id  (DD1)
dmap f = dorp ∘ map_{NM} f  (DD2)

Note that, analogously to Lemma 15(i), (DD2) holds iff (DD1) and (G2) hold.

Theorem 18. Assume that NM is a compound monad for which (J2′) holds. Define djoin by (G9) or (DJ), and dmap and dunit by (G10) and (DU). Then (DJ) and (G1) to (G12) hold. Further, if dorp is defined by (DD1), then (DD2) and D(1) to D(4) hold.

Proof. (G11) holds, using (3M). The equivalence of (DJ), that is, djoin = map_{M} join_{N}, and (G9) follows from Lemma 13. Then djoin ∘ dunit = map_{M} join_{N} ∘ map_{M} unit_{N} = id, by (2M), (5N) and (1M), that is, (G5) holds. Thus the conditions of Theorem 12 are satisfied, so (G1) to (G8) also hold, as does, by Theorem 11, (G12).

Now, using (DD1), we get (DD2) from (G2). Then D(3) is just (G1), and D(4) follows from (G4), by (G8) and (8NM). Using (DU), (G3) gives D(2).

We prove D(1) by

dorp ∘ map_{NM} (map_{M} f) = dmap (map_{M} f)  (DD2)
= ext_{NM} (dunit ∘ map_{M} f)  (G10)
= ext_{NM} (map_{NM} f ∘ dunit) (MC, 2M, 3N, DU)
= map_{NM} f ∘ ext_{NM} dunit  (E5NM, E3′NM)
= map_{NM} f ∘ dorp  (G10, DD1) □

Note that our definition of dorp gives dorp = dmap id = ext_{NM} dunit, which corresponds to the definition used in [3, §4.2].

Jones & Duponcheel [3, §3.3] also show how to define a compound monad from a function dorp, satifying four rules D(1) to D(4), assuming that M is a premonad and N is a monad. They use (UC) and (MC) as definitions, and defining join_{NM} by

join_{NM} = map_{M} join_{N} ∘ dorp  (JD)

They show that in such a compound monad, (J2) holds. We can prove this theorem via rules (G1) to (G8) and Theorem 11. However in doing so, we have to prove (4NM) on the way to proving (G4) which is rather unsatisfying.

Theorem 19. [3, §3.3] Let N be a monad and M a premonad. Define unit_{NM} and map_{NM} by (UC) and (MC). Define djoin and dunit by (DJ) and (DU). Let the function dorp satisfy D(1) to D(4), and define dmap by (DD2). Define join_{NM} by (JD). Then NM is a monad satisfying (G1) to (G12) and (J2).

Proof. (sketched: also proved in Isabelle). Firstly, note that NM is a premonad. From that fact, using (DD2), we can get (DD1) from (1NM), (G2) from (2NM), (G3) from (3NM) and D(2), while (G1) is just D(3).

(G5): Use (DJ), (DU), (2M), (5N) and (1M).

(G6): Use (DJ), (UC), (G2), (G1), (MC), (2M), (6N) and (1M).

We use (G8) as a definition, noting also that (8NM) holds, as

join_{NM} ∘ map_{NM} f = map_{M} join_{N} ∘ dorp ∘ map_{NM} f  (JD)
= djoin ∘ dmap f  (DJ, DD2)

From (G8) and (G1) we get (G9).

To prove (G4) and (G7) we derive initially

djoin ∘ dmap map_{M} g = map_{M} join_{N} ∘ map_{NM} g ∘ dorp (DJ, DD2, D(1))
= map_{M} (join_{N} ∘ map_{N} g) ∘ dorp  (MC, 2M)
= map_{M} (ext_{N} g) ∘ dorp  (8N)

Then, to get (G7), we set g = join_{N} in this to get, on the right-hand side,

map_{M} (ext_{N} join_{N}) ∘ dorp = map_{M} (join_{N} ∘ join_{N}) ∘ dorp  (7N, 8N)
= djoin ∘ map_{M} join_{N} ∘ dorp = djoin ∘ join_{NM}  (2M, DJ, JD)

and we set g = map_{N} f in it to get, by a very similar argument, using (4N) instead of (7N), djoin ∘ dmap map_{NM} f = map_{NM} f ∘ join_{NM}. Rewriting using (G8) and (8NM), we have (4NM). Thus the property of h that join_{NM} ∘ map_{NM} h = h ∘ join_{NM} holds for h = dorp, by D(4), and for h = map_{NM} f, above. So it is easy to see that this property holds for their composition, h = dorp ∘ map_{NM} f, which, again using (G8) and (8NM), gives us (G4).

Thus Theorem 11 applies. As we now have both (G9) and (DJ), Lemma 13 shows that (J2) holds. ⊓ ⊔

A.3 Relation between the kmap construction and the swap construction of Jones & Duponcheel

Throughout this section we make the assumptions of §A.1 and of §A.2. That is, we assume that M and N are monads, and that (UC) and (MC) hold. Under these assumptions Jones & Duponcheel [3, §3.4,§4.3] show that the compound monads NM which can be defined using swap and the four rules S(1) to S(4) (where prod and dorp are defined in terms of swap as shown) are precisely those satisfying (J1) and (J2).

swap ∘ map_{N} (map_{M} f) = map_{NM} f ∘ swap  S(1)
swap ∘ unit_{N} = map_{M} unit_{N}  S(2)
swap ∘ map_{N} unit_{M} = unit_{M}  S(3)
prod ∘ map_{N} dorp = dorp ∘ prod  S(4)
prod = map_{M} join_{N} ∘ swap  dorp = ext_{M} swap

swap = kmap id  (KS1)
kmap f = swap ∘ map_{N} f  (KS2)
kmap (g ∘ f) = kmap g ∘ map_{N} f  (KO)

Note that, analogously to Lemma 15(i), (KS2) holds iff (KS1) and (KO) hold.

Theorem 20. With the assumptions and definitions of Theorem 14, further define swap from kmap by (KS1). Then S(1) to S(4) hold.

Proof. By Lemma 9(i), Theorem 8 applies. So by Lemma 10, (KO) and so (KS2) hold. So S(3) is just (1K). Now by (E5K), (E6M) and (DUK), kmap f = pext (unit_{NM} ⊙_{M} f) = pext (dunit ∘ f), so swap = pext dunit and, by (E1K′), swap ∘ unit_{N} = dunit and S(2) follows.

We show S(1), after simplifying it using (KS2), as follows:

kmap (map_{M} f) = kmap ((unit_{M} ∘ f) ⊙_{M} id)  (E5M, A5M)
= kmap (unit_{M} ∘ f) ⊙_{M} kmap id  (2K)
= (kmap unit_{M} ∘ map_{N} f) ⊙_{M} swap  (KO, KS1)
= ext_{M} (unit_{M} ∘ map_{N} f) ∘ swap  (1K, E6M)
= map_{NM} f ∘ swap  (E5M, MC)

Now, for S(4) we first use our definitions of dorp and prod. By (DD1) and (DMK), dorp = ext_{M} (kmap id), and by (E5K) let kmap id be pext g, so we have

prod ∘ map_{M} dorp = pext (ext_{M} (kmap id))  (PP2)
= pext (pext g ⊙_{M} id)  (A5M)
= pext g ⊙_{M} pext id  (E3′K)
= ext_{M} (kmap id) ∘ prod  (PP1, E6M)

Finally, to show S(4) precisely as it is stated, we need to check that the various definitions of prod and dorp are consistent. By our definitions,

prod = pext id = kjoin ⊙_{M} kmap id  (PP1, 8K)
= ext_{M} kjoin ∘ swap = map_{M} join_{N} ∘ swap (E6M, KS1, DJK, DJ)
dorp = dmap id = ext_{M} (kmap id) = ext_{M} swap  (DD1, DMK, KS1)

so our definitions are consistent with those used above in stating S(4). ⊓ ⊔

We showed in the proof above that swap = pext dunit which is consistent with the definition of swap used in [3, §4.3].

Conversely, from S(1) to S(4), (KS2) and (KJ) it is possible to prove the rules of (1K) to (7K) directly. These proofs have been done in Isabelle, see [2], functor fromSwap. Alternatively, see Jones & Duponcheel [3, §3.4] for proofs from S(1) to S(4) that NM is a monad.

Another interesting result is that both sides of S(4) equal swap ⊙_{NM} swap. The key step to prove it is to modify the proof of S(4) above, to give

prod ∘ map_{M} dorp = pext (pext g ⊙_{M} id)  (as above)
= pext (pext g) ⊙_{M} kmap id  (9K)
= pext swap ⊙_{M} swap = swap ⊙_{NM} swap (KS1, E6K)

A.4 A distributive law for monads

Manes [6] describes a “distributive law” for monads, at Chapter 4, pages 311-2, Definition 3.6, and page 334, Exercise 6. This is also described by Barr & Wells in [1], §9.2, where rules (D1) to (D4) are given. His natural transformation λ is also the polymorphic function swap. Translating these rules into our terminology, and calling (D1) to (D4) (BWD1) to (BWD4), we have

swap ∘ map_{N} unit_{M} = unit_{M}  (BWD1)
swap ∘ unit_{N} = map_{M} unit_{N}  (BWD2)
swap ∘ map_{N} join_{M} = join_{M} ∘ map_{M} swap ∘ swap  (BWD3)
swap ∘ join_{N} = map_{M} join_{N} ∘ swap ∘ map_{N} swap  (BWD4)

Of these, (BWD2) and (BWD4) are the diagrams in [6, Definition 3.16], and (BWD1) and (BWD3) are the diagrams in Exercise 6 on page 334 of [6]. He additionally specifies that swap is a natural transformation.

Theorem 21. With the assumptions and definitions of Theorem 20, (BWD1) to (BWD4) hold and swap is a natural transformation.

Proof. From Theorem 20 we have S(1) to S(4). That swap is a natural transformation is just S(1), and (BWD2) and (BWD1) are just S(2) and S(3). We can translate (BWD3) to kmap (id ⊙_{M} id) = kmap id ⊙_{M} kmap id, an instance of (2K). To prove (BWD4), we have, by Theorem 2 for K_{M}, (iii) ⇒ (i), and (E5K),

pext (kmap id) = kmap id ⊙_{M} kjoin
= kmap id ⊙_{M} unit_{M} ∘ join_{N}  (KJ, A6M)
= swap ∘ join_{N}  (KS1, A1M)

Now pext (kmap id) = prod ∘ map_{N} swap which is, by the expression for prod in §A.3 above, equal to the right-hand side of (BWD4). ⊓ ⊔

Conversely, from S(1) and (BWD1) to (BWD4), (KS2) and (KJ) it is possible to prove the rules of (1K) to (7K), and the resulting compound monad satisfies (J1) and (J2) . These proofs have been done in Isabelle, see [2], functors

fromSextDL and fromSextF.

For monads N, M and NM, where (MC) is assumed, Barr & Wells [1, §9.2] give five conditions, (C1) to (C5), for the existence of a distributive law, but in fact (C2) ⇔ (C5) and (C3) ⇔ (C4), as noted in §3.8. These conditions are given below, as are the proofs of these equivalences, in the category theory notation.

Michael Barr has observed that there is a duality between (C2,C5) and (C3,C4), when these are written in category theory notation, and so the same duality should hold between the proofs of implications between these conditions. The proof (C3) ⇒ (C4) is due to this observation. Interestingly, while the proofs are dual in a notational sense, the reasons for each step of the proofs are not so.

We indicate the correspondence between the category theory notation and the notation of this paper.

μ  join_{NM} : αNMNM → αNM
μF  join_{NM} : αF NMNM → αF NM
μ, μ_{1}, μ_{2}  join_{NM}, join_{N}, join_{M}
η, η_{1}, η_{2}  unit_{NM}, unit_{N}, unit_{M}
T, T_{1}, T_{2}  map_{NM}, map_{N}, map_{M}
T = T_{2}T_{1}  map_{NM} = map_{M} ∘ map_{N}  (MC)
μ ∘ ηT = id  join ∘ unit = id  (5)
μ ∘ T η = id  join ∘ map unit = id  (6)
μ ∘ T μ = μ ∘ μT  join ∘ map join = join ∘ join  (7)

We first list the conditions (C1) to (C5).

η = T_{2}η_{1} ∘ η_{2} = η_{2}T_{1} ∘ η_{1}  (C1)
μ ∘ T η_{2}T_{1} = T_{2}μ_{1}  (C2)
μ ∘ T_{2}η_{1}T = μ_{2}T_{1}  (C3)
μ_{2}T_{1} ∘ T_{2}μ = μ ∘ μ_{2}T_{1}T  (C4)
T_{2}μ_{1} ∘ μT_{1} = μ ∘ T T_{2}μ_{1}  (C5)

Finally we show the proofs of equivalence. Note the duality between the notations of the proofs. Steps with no reasons given rely on either T or T_{i} being functors (T (ϕ ∘ ψ) = T ϕ ∘ T ψ) or on the definition of composition of natural transformations ((ϕ ∘ ψ)T = ϕT ∘ ψT). Observe how the duality between the proofs also uses the duality between rules (5) and (6), and the self-duality of rule (7) (see the table above). But also note the duality between the specific uses made of the naturality of η_{1} and of μ.

(C4) ⇒ (C3): μ ∘ T_{2}η_{1}T = μ ∘ (μ_{2} ∘ T_{2}η_{2}) T_{1}T ∘ T_{2}η_{1}T  (6 for T_{2})

= μ ∘ μ_{2}T_{1}T ∘ T_{2}η_{2}T_{1}T ∘ T_{2}η_{1}T
= μ ∘ μ_{2}T_{1}T ∘ T_{2} (η_{2}T_{1} ∘ η_{1}) T
= μ ∘ μ_{2}T_{1}T ∘ T_{2}ηT  (C1)
= μ_{2}T_{1} ∘ T_{2}μ ∘ T_{2}ηT  (C4)
= μ_{2}T_{1} ∘ T_{2} (μ ∘ ηT) = μ_{2}T_{1}  (5 for T)

(C3) ⇒ (C4): μ_{2}T_{1} ∘ T_{2}μ = μ ∘ T_{2}η_{1}T ∘ T_{2}μ  (C3)

= μ ∘ T_{2} (η_{1}T ∘ μ)
= μ ∘ T_{2} (T_{1}μ ∘ η_{1}T^{2})  (η_{1} natural)
= μ ∘ T μ ∘ T_{2}η_{1}T^{2}
= μ ∘ μT ∘ T_{2}η_{1}T^{2}  (7 for T)
= μ ∘ μ_{2}T_{1}T  (C3)

(C5) ⇒ (C2): μ ∘ T η_{2}T_{1} = μ ∘ T T_{2} (μ_{1} ∘ η_{1}T_{1}) ∘ T η_{2}T_{1}  (5 for T_{1})

= μ ∘ T T_{2}μ_{1} ∘ T T_{2}η_{1}T_{1} ∘ T η_{2}T_{1}
= μ ∘ T T_{2}μ_{1} ∘ T (T_{2}η_{1} ∘ η_{2}) T_{1}
= μ ∘ T T_{2}μ_{1} ∘ T ηT_{1}  (C1)
= T_{2}μ_{1} ∘ μT_{1} ∘ T ηT_{1}  (C5)
= T_{2}μ_{1} ∘ (μ ∘ T η) T_{1} = T_{2}μ_{1}  (6 for T)

(C2) ⇒ (C5): T_{2}μ_{1} ∘ μT_{1} = μ ∘ T η_{2}T_{1} ∘ μT_{1}  (C2)

= μ ∘ (T η_{2} ∘ μ) T_{1}
= μ ∘ (μT_{2} ∘ T^{2}η_{2}) T_{1}  (μ natural)
= μ ∘ μT ∘ T^{2}η_{2}T_{1}
= μ ∘ T μ ∘ T^{2}η_{2}T_{1}  (7 for T)
= μ ∘ T T_{2}μ_{1}  (C2)

B Some examples using rules (A1) to (A4)

In this section we give some examples of monads which are easily shown to be monads using rules (A1) to (A4).

The two examples in §B.2 and §B.3 are (in different senses) compound monads. In both cases M is an arbitrary monad; we don’t explicitly use the monad N, but proceed directly to define the compound monad N_{M}. The simple monad N will be a special case of N_{M}, which could be obtained by setting M to be the identity monad (in which unit, ext, map and join are all the identity function).

B.1 Example: the Continuation Monad

The continuation monad (eg, [8, §3.1]) is given by αK = (α → Ans) → Ans, where Ans is a fixed type, so α → βK = α → (β → Ans) → Ans. We use the function C, of type (γ → δ → Ans) → (δ → γ → Ans), defined by C f x y = f y x. Note that C (C f) = f, so C is 1-1, and C x = C y ⇒ x = y. Then we define ⊙_{K} by C (g ⊙_{K} f) = C f ∘ C g, and unit_{K} by C unit_{K} = id.

The ⊙ rules are then easily proved. For each rule lhs = rhs, as C is 1-1, it suffices to prove C (lhs) = C (rhs).

for (A1): C (f ⊙_{K} unit_{K}) = C unit_{K} ∘ C f = id ∘ C f = C f for (A2): C (unit_{K} ⊙_{K} f) = C f ∘ C unit_{K} = C f ∘ id = C f for (A3): C (h ⊙_{K} (g ⊙_{K} f)) = (C f ∘ C g) ∘ C h =

C f ∘ (C g ∘ C h) = C ((h ⊙_{K} g) ⊙_{K} f)

It is simple but tedious to confirm (A4) directly. We now check that this definition corresponds to the usual ones. Using (A5), we get

unit_{K} a c = C id a c = id c a = c a , and

ext_{K} g k c = (g ⊙_{K} id) k c = C (C id ∘ C g) k c = (C id ∘ C g) c k = C id (C g c) k = id k (C g c) = k (λf. g f c)

Both of these agree with the definitions in [8, §3.1].

B.2 Example: the Compound State Monad

Let M be a monad. Let State be a fixed type, representing, for example, a program state. Then the state monad is given by the type αS = State → α∗State (where α ∗ β denotes a pair type). This represents a computation which takes a program state and returns a result of interest and a new state. The “compound” state monad is given by the type αS_{M} = State → (α ∗ State)M. (Note that because αS_{M} is neither αSM nor αMS, §3.1 and following are not relevant to this example, which perhaps should not be called a “compound monad”). If, for example, M is the list monad, S_{M} could be used to represent a nondeterministic program, which may behave in any of a number of possible ways, each way returning a result and new state.

To show that this is a monad, we use the functions curry and unc

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

noting that these are mutually inverse (so, in particular, unc is 1-1). Consider a function f : α → βS_{M}. Then unc f is of type α ∗ State → (β ∗ State) M. Given that M is a monad, it is easy to see how to compose functions of such a type – we define ⊙_{SM} and unit_{SM} by

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

The ⊙ rules are then easily proved. For each rule lhs = rhs, as unc is 1-1, it suffices to prove unc (lhs) = unc (rhs). The proofs use the corresponding rules for the 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)

It is simple but tedious to confirm (A4) directly. We need only check that this definition corresponds to the usual ones. Using (A5),

unit_{SM} a s = curry unit_{M} a s = unit_{M} (a,s) , and

ext_{SM} k m s = (k ⊙_{SM} id) m s = curry (unc k ⊙_{M} unc id) m s =

(ext_{M} (unc k) ∘ unc id) (m,s) = ext_{M} (λ(a, t). k a t) (m s)

Both of these agree with the definitions in [4, §7.1] (modified to switch the members of pairs).

B.3 Example: the Compound Reader Monad

Again, let M be a monad. Let Env be a fixed type. Then the environment, or reader, monad is given by the type Env → α (evaluating any monadic value also involves reading the environment). The reader monad is given by the type αR = Env → α, and the compound reader monad ([4, §7.2], [3, §6.3]) is given by αR_{M} = Env → αM = (αM)R.

To show that this is a monad, we define a function ap_{e} f a = f a e (for e : Env), of type (γ → Env → δ) → (γ → δ). In similar proofs earlier, we had a function which was 1-1; here we need to use the property

(∀e.ap_{e} f = ap_{e} g) ⇒ f = g

We define ⊙_{RM} and unit_{RM} by

(g ⊙_{RM} f) a e = (ap_{e} g ⊙_{M} ap_{e} f) a
unit_{RM} a e = unit_{M} a

that is,

ap_{e} (g ⊙_{RM} f) = ap_{e} g ⊙_{M} ap_{e} f
ap_{e} unit_{RM} = unit_{M}

The ⊙ rules are then easily proved. For each rule lhs = rhs, it suffices to let e be arbitrary, and then to prove ap_{e}(lhs) = ap_{e}(rhs). The proofs use the corresponding rules for the monad M.

for (A1) and (A2):

ap_{e} (f ⊙_{RM} unit_{RM}) = ap_{e} f ⊙_{M} ap_{e} unit_{RM} = ap_{e} f ⊙_{M} unit_{M} = ap_{e} f ap_{e} (unit_{RM} ⊙_{RM} f) = ap_{e} unit_{RM} ⊙_{M} ap_{e} f = unit_{M} ⊙_{M} ap_{e} f = ap_{e} f

for (A3): ap_{e} (h ⊙_{RM} (g ⊙_{RM} f)) = ap_{e} h ⊙_{M} (ap_{e} g ⊙_{M} ap_{e} f) = (ap_{e} h ⊙_{M} ap_{e} g) ⊙_{M} ap_{e} f = ap_{e} ((h ⊙_{RM} g) ⊙_{RM} f)

It is straightforward to confirm (A4) directly. We need only check that this definition corresponds to the usual ones. Using (A5),

unit_{RM} a e = unit_{M} a , and
ext_{RM} k m e = (k ⊙_{RM} id) m e = (ap_{e} k ⊙_{M} ap_{e} id) m =
(ext_{M} (ap_{e} k) ∘ ap_{e} id) m = ext_{M} (λa. k a e) (m e)

Both of these agree with the definitions in [4, §7.2].

C Examples of the Compound Monad Constructions

C.1 Example: the Compound Exception Monad

The exception (or error) monad is given by

              datatype α E = Ok of α | Err of string

with unit_{E} a = Ok a.

With M an arbitrary monad we define the compound monad αEM by

pext f (Ok a) = f a  (pext-Ok)
pext f (Err msg) = unit_{M} (Err msg)  (pext-Err)

(Letting M be the identity monad gives us the definition of ext_{E}, for then pext is ext_{E}). We also define unit_{EM} and ⊙_{EM} by (UC) and (E6K). Then we prove the pext axioms (E1K) to (E3K) as follows. (E1K) is just (pext-Ok). Using the definitions just mentioned, we get (E2K) from

pext unit_{EM} (Ok a) = unit_{EM} a = unit_{M} (Ok a) pext unit_{EM} (Err msg) = unit_{M} (Err msg)

and using these definitions and also (E6M) we get (E3K) from

pext (g ⊙_{EM} f) (Ok a) = (pext g ⊙_{M} f) a  (pext-Ok, E6K)
= ext_{M} (pext g) (f a)  (E6M)
= ext_{M} (pext g) (pext f (Ok a))  (pext-Ok)
= (pext g ⊙_{M} pext f) (Ok a)  (E6M)
pext (g ⊙_{EM} f) (Err msg) = unit_{M} (Err msg)  (pext-Err)
= pext g (Err msg)  (pext-Err)
= ext_{M} (pext g) (unit_{M} (Err msg))  (E1)
= ext_{M} (pext g) (pext f (Err msg)) (pext-Err)
= (pext g ⊙_{M} pext f) (Err msg)  (E6M)

C.2 Other Examples; Isabelle Proofs

Example: the Compound Writer Monad Let Monoid be a type representing a monoid, where we use 0 for the identity value and + for the associative binary operation. Then let αW = (Monoid ∗ α) and αW M = (αW)M. A function f : α → βW represents a function from α to β which also produces some output m of type Monoid; when ext_{W} f acts on (acc, a), where acc represents output already accumulated, the output m is added to that in acc. That is, if f a = (m, b), then ext_{W} f (acc,a) = (acc + m, b). Naturally, unit_{W} a = (0, a).

The compound writer monad is given by

pext f (acc,a) = map_{M} (λ(m,b). (acc + m, b)) (f a)

That is, the addition of the new output m to the accumulated output acc is done “under the hood” of the monad M. This makes the proof of the axioms for pext more difficult, and we omit them. (Jones & Duponcheel [3, §6.5.1] also omit proofs for this monad).

Example: the Compound Reader Monad This was discussed in §B.3. We write the monad type as αNR, where R takes the place of M in our general results. Note that, here, the monad R is fixed, while N is arbitrary. The pext construction applies to this compound monad, but to use it, we need to show

(i) that R is a monad (ii) that N is a monad (iii) that the axioms for pext, (E1K) to (E3K), hold

Our treatment of compound monads using the pext axioms requires, as such, only (i) and (iii), but we need (ii) to prove (iii). These proofs are, however, not difficult, and are omitted.

Isabelle Proofs The proofs in this paper and the proofs for the compound reader and writer monads were performed using the theorem prover Isabelle, and are available at [2], or from the author’s home page.

Jones & Duponcheel, [3, §6.4], discuss the compound list monad – α list M is a monad provided that M is a commutative monad, and they give proofs of this. We also have Isabelle proofs of the pext axioms for the compound list monad.