Notions of Monad Strength
Philip Mulry
Department of Computer Science
Colgate University
Hamilton, New York, 13346, USA
pmulry@colgate.edu

Over the past two decades the notion of a strong monad has found wide applicability in computing. Arising out of a need to interpret products in computational and semantic settings, different
approaches to this concept have arisen. In this paper we introduce and investigate the connections
between these approaches and also relate the results to monad composition. We also introduce new
methods for checking and using the required laws associated with such compositions, as well as
provide examples illustrating problems and issues that arise.

1

Introduction

The notion of a strong monad arises in numerous applications including programming language design
and semantics, monadic interpreters, and building models of computation. The notion, originating with
Kock[3], was originally defined for symmetric monoidal closed categories. Mulry and others exploited
this idea to introduce specific kinds of strong monads to generate a wide variety of categorical computational models as well as an analysis of fixed point semantics[8]. In the work of Moggie and Wadler the
notion of a strong monad was used to define the semantics of programming languages [7], [14].
Different approaches to the notion of a strong monad have also arisen. From early on it was recognized that a strong monad, and particularly the special case of a commutative monad, was critical in
providing a means of interpreting products in a Kleisli category, and a means of providing a functorial
lifting of biproducts. More recently Manes and Mulry have focused attention on the idea that monads,
rather than being called strong which might suggest that this is a uniquely defined property of a given
monad, could be viewed as being equipped with a possibly non-unique strength of a given order. In
[6], the authors introduced the concept of a Kleisli strength of order n for arbitrary monads in an arbitrary symmetric monoidal category, demonstrated that the notion of Kleisli strength differs from Kock
strength and provided examples demonstrating that Kleisli strength takes the form of added (non-unique)
structure on a given monad, leading to the terminology of a monad equipped with a strength (H, Γ). The
authors further observed that the existence of Kleisli strength can be used to derive methods for generating (non-unique) composition of monads for a variety of monads including standard monadic data types
such as lists, trees, exceptions, reader, writer and state monads.
Different ways of defining strength lead naturally to the question of describing more fully the connections between these definitions. For instance, the definition of strength found in some examples of strong
monads used for monadic interpreters may not support products in the Kleisli category because they fail
to satisfy the laws required of a Kleisli strength. A further complication arises from the observation that
the original use of the notion by Kock assumed the monad itself was a monoidal functor, something most
monads used in computing simply are not.
This paper provides details of the relationship between these varying notions of strength and suggests
new nomenclature to distinguish between them. The paper assumes the reader is familiar with the general
A. Banerjee, O. Danvy, K.-G. Doh, J. Hatcliff (Eds):
David A. Schmidt’s 60th Birthday Festschrift
EPTCS 129, 2013, pp. 67–83, doi:10.4204/EPTCS.129.6

c P. S. Mulry

Monad Strength

68

notions of category theory, and also depends heavily on [6]. In section 2 we provide preliminaries such
as defining the notion of a Kleisli strength, and include some examples and methods for generating it.
As the examples illustrate, this notion is of independent interest and generalizes the prior notions of a
commutative monad.
Section 3 provides a brief introduction to classical commutative monads and Kock strength contrasting these concepts with that of general Kleisli strength. Also introduced is the notion of a prestrength
construction arising from the existence of map, its associated category, as well as a wide variety of
examples to help sort out the differences between the concepts.
In section 4 we restate and prove some of the previous results in Haskell syntax. In addition to providing a means of computing and using Kleisli strength and monad compositions in Haskell, it is hoped
this approach may prove more intuitive and accessible to the reader used to working in the environment
of functional programming.

2

Preliminaries

Let C, D be categories with functor F : C → D, H = (H, µ , η ) a monad in C, K = (K, ν , ρ ) a monad in
D. Note that we use categorical notation here. We write CH for the Kleisli category of H with canonical
f

ηY

f

functor ιH : C → CH , ιH (X −−→ Y ) = X −−→ Y −−→ HY .
A Kleisli lifting of functor F is a functor F : CH → DK that lifts F in the sense that the following
diagram commutes.
CH

F✲D
K

✻

✻

ιH

ιK

✲D
F
Kleisli liftings are classified exactly by natural transformations λ : FH → KF satisfying

C

F

Fη

✲ FH

❩
❩
❩ (FC)
❩
λ
❩
ρF ❩
❩
❄
❩
⑦ KF ✛
❩

✛

Fµ
(FD)

FHH

λH

❄

KFH
Kλ

❄

νF

KKF

The transformation λ is referred to as a lifting transformation. For instance, it is easy to see that
given such a λ and defining F by F( f : A → HB) = λ ◦ (F f ) results in a well-defined functor. It
should be further pointed out that liftings (and thus lifting transformations) may not be unique for a
fixed functor F, something we will demonstrate later. A simple example is the well known notion of a
monad map : CH → CK which corresponds to a Kleisli lift of the identity functor on C. This is a rather
simple explanation of a far more subtle process. An elegant and more conceptual account of the precise
correspondence and interaction between liftings and morphisms of monads can be found in [13].
While most of our discussion will take place in a cartesian closed category such as Set, some of the
following constructions and results are applicable to more general settings such as symmetric monoidal
categories V with tensor ⊗ and tensor unit I. We will make occasional use of these generalizations here.

P. S. Mulry

69

We shall use the abbreviation ×n x for x × · · · × x (n times), where x can be either an object or a map.
When x is an object and n = 0, ×n x = I. In general, ×1 x = x. We also use the same symbol for the
n-fold product functor, so that ×n (V1 , . . . ,Vn ) = V1 × · · · ×Vn .

3

Notions of Strength

Let K = (K, ν , ρ ) be a monad on V . For n ≥ 0, consider the cartesian power category V n with objects
(V1 , . . . ,Vn ) and morphisms ( f1 , . . . , fn ) : (V1 , . . . ,Vn ) → (W1 , . . . ,Wn ). K induces a monad K(n) on V n
via K (n) (V1 , . . . ,Vn ) = (KV1 , . . . , KVn ), ρ(V1 ,...,Vn ) = (ρV1 , . . . , ρVn ), ν(V1 ,...,Vn ) = (νV1 , . . . , νVn ). We denote the
resulting Kleisli category for K(n) simply as VKn , also reflecting the fact that the Kleisli construction
commutes with products in Cat.

3.1 Pre-strength
Many of the notions and examples found in the first two sections can also be found in [6], including the
notion of prestrength.
Definition 3.1 Consider the category whose objects are pairs (F, ΓF ) with F : V → V a functor and
ΓVF1 ···Vn : FV1 × · · · × FVn → F(V1 × · · · ×Vn ) a natural transformation. Such a ΓF is called a pre-strength
on F (we often drop the subscripts except when needed for emphasis). A morphism α : (F, ΓF ) → (G, ΓG )
is a natural transformation α : F → G such that the following square commutes.
αV1 × · · · × αVn
✲ GV1 × · · · × GVn
FV1 × · · · × FVn
ΓVF ···Vn

ΓVG ···Vn

1

1

❄

F(V1 × · · · ×Vn )

αV1 ×···×Vn

❄
✲ G(V1 × · · · ×Vn )

When α is such a morphism we say α preserves pre-strengths. It is obvious that this is a category
under vertical composition of natural transformations, but it is also a 2-category under the horizontal
composition of the endofunctor category of V .
Example 3.2 If F = L+ is the non-empty list monad and one defines defines ΓF via comprehensions,
namely ΓF (list1, list2) = [(a, b)|a ← list1, b ← list2], it is easy to check that ΓF is a natural transformation and forms a pre-strength of order 2. We return to this example shortly.

3.2 Kleisli strength
In [9] the idea was promoted that in the context of programming language semantics, a Kleisli lifting
provides a means of lifting a given functorial process F : C → D to the semantics residing in the corresponding Kleisli categories F : CH → DK . The associated lifting transformation mediates this process.
A special case of this corresponds to lifting the product bifunctor to the corresponding Kleisli category.
In short, if products are to be well defined in the Kleisli category CH and capable of interpreting composition of functions for computational or programming semantics as described earlier, a Kleisli lifting
of the bifunctor must exist. This has been generalized to the notion of Kleisli strength.

Monad Strength

70

Definition 3.3 A Kleisli strength on K of order n ≥ 0 is a natural transformation ΓVn ,···,Vn : KV1 × · · · ×
1
KVn → K(V1 × · · · × Vn ) which classifies a Kleisli lift ×n : VKn → VK of the n-fold product functor ×n :
V n → V . Thus Γn is a natural transformation satisfying (Γn A) and (Γn B) as shown in the diagram
below. (Note V - subscripts are dropped for readability sake.)
V1 × · · · ×Vn

ρ × ··· × ρ ✲
KV1 × · · · × KVn

❩
❩
❩
(Γn A)
❩
❩
ρ ❩
❩
❩
⑦
❩

✛ ν × ··· × ν

KKV1 × · · · × KKVn
ΓnK

(Γn B)

Γn
❄

K(V1 × · · · ×Vn )

❄

K(KV1 × · · · × KVn )
KΓn

✛

❄

ν

KK(V1 × · · · ×Vn )

For n = 0, (Γ0 A) always exists and coincides with ρI . A Kleisli strength of order 1 is the same thing
as a monad map K → K. We note that there is always at least one Kleisli strength of order 1, namely
ΓV1 = idKV . Based on the discussion of section 2, a Kleisli strength of order n is precisely a lifting
transformation for ×n .
We briefly describe a few examples of Kleisli strength. As indicated earlier, the category of sets and
total functions will be denoted Set.
Example 3.4 Let K = L be the list monad then the reverse transformation rev : L → L is a Kleisli strength
of order 1 on L. Since identity is also of order one by the above remark, this demonstrates that Kleisli
strengths are not unique.
Example 3.5 Let K = P0 be the finite power set monad. Then Γn (A1 , . . . , An ) = A1 × · · · × An is a Kleisli
strength of order n ≥ 0, where Ai ∈ P0Vi for 1 ≤ i ≤ n.
Example 3.6 Let K be the exceptions monad MX = X + Exc, with Exc any nonempty set. If a ∈ Exc,
for each n ≥ 0 the monad admits a Kleisli strength of order n Γn , where Γn (x1 , ..., xn ) = (x1 , . . . , xn ), if all
of the xi are in X , and equals a otherwise. If a 6= b where b ∈ Exc, then the new Γn generated by b differs
from the one generated by a. We return to this example shortly.
Example 3.7 Much as in the previous example, let K be the ‘add a bottom’ or lifting monad, KA = A⊥
defined on Dom, the category of (possibly bottomless) Scott domains and continuous maps [12]. Γn is a
Kleisli strength of order n (n ≥ 1) where Γn (x1 . . . xn ) = (x1 . . . xn ) if all of the xi are in X , and equals ⊥
otherwise.
Example 3.8 For a fixed A consider the exponential or reader monad M where MB = A → B. M has a
Kleisli strength of order n where Γn ( f1 . . . fn ) = λ a.( f1 (a) . . . fn (a)).
Example 3.9 Consider the M-set or writer monad KX = M × X , where M is a commutative monoid,
then Γ2 ((m1 , x), (m2 , y)) = (m1 m2 , x, y)) forms a Kleisli strength of order 2.
In the last example if M is not commutative, then Γ2 need not form a Kleisli strength of order 2.
Likewise in the next example we see list comprehensions do not generally form Kleisli strengths.
Example 3.10 Let K = L+ then the prestrength ΓK of Example 3.2 does not form a Kleisli strength of
order 2. Working clockwise on the pair ([[1, 2], [3]], [[5, 6], [7]]) in diagram (Γn B), for instance, generates
[(1, 4), (1, 5), (1, 6), ...], while counterclockwise generates [(1, 4), (1, 5), (2, 4), ...].

P. S. Mulry

71

Example 3.11 The binary tree monad V X consists of binary trees whose values (from X ) are located
in its leaves. We denote an empty tree by E, a trivial tree (i.e. a leaf) with value x by L(x) and a tree
consisting of left and right subtrees v1 and v2 by N(v1, v2). If V+ denotes the submonad of non-empty
binary trees, then the map Γ : V + A × V + B → V + (A × B) defined by Γ(t1,t2) = L(a, b) where L(a) and
L(b) are the leftmost nodes of trees t1 and t2 respectively forms a Kleisli strength of order 2 on V + .
Proposition 3.12 Let Γ2 be a Kleisli strength on K of order 2, then Γ3 = Γ2 ◦(Γ2 × 1) is a Kleisli strength
on K of order 3. The same process produces Γ4 from Γ3 , Γ5 from Γ4 , . . . producing a Kleisli strength
Γn of order n for all n ≥ 2. In a similar fashion one can also define a Kleisli strength of order 3 via
Γ3 = Γ2 ◦ (1 × Γ2 ) and similarly Γ4 = Γ2 ◦ (1 × Γ3 ) . . .. These constructions generally disagree unless
Γ2 is associative, namely Γ ◦ (Γ × 1) = Γ ◦ (1 × Γ).
Example 3.13 Let L+ be the non-empty list monad. In contrast to Example 3.10, by using a different
approach than comprehensions we can produce examples of Kleisli strength. Let f st and lst : L+ → id
choose the first (or respectively last) element of a non-empty list. Then η ◦ ( f st × f st) and η ◦ (lst × lst)
are associative Kleisli strengths of order 2.

3.3 Prestrength Construction
As the prior sections illustrate, the notion of Kleisli strength consists of additional (non-unique) structure
(Γn ) imposed on the monad. In particular, no assumption was made of the existence of an internal
map structure st : (A → B) → (MA → MB) for a monad M. The underlying category need not even
be closed. This is a common assumption in functional programming, indeed it is already built into
the specification of the functor class in Haskell, where it is denoted f map. The idea of a monad in a
category equipped with a map st : BA → (MB)MA had already been defined much earlier by Kock [3]
who called it a strong monad. Building the composition λ a.st(λ b.(a, b)) : A → (MB → M(A × B)), and
taking adjoints generates the map we denote rst : A × MB → M(A × B)), which is often referred to in the
functional programming language literature as ”the monad strength” for M (and often denoted simply by
t). In a similar fashion one can generate the map lst : MA × B → M(A × B)). This leads in turn to the
compositions
lstΓAB = rst # ◦ lst : MA × MB → M(A × B)
rstΓAB = lst # ◦ rst : MA × MB → M(A × B)
where f # a = (µ ◦ M f )(a), using the standard # notation first introduced by Manes [4]. These two
compositions can easily be checked for naturality and form what we denote as the left and right prestrength constructions, lstΓAB , rstΓAB , for the given monad. These derived pre-strengths are generally
not equal nor are they always examples of Kleisli strength as we illustrate next. In light of this last
observation, it makes sense to consider to what extent prestrength constructions support products in a
semantic setting.
For the remainder of the paper whenever we have a monad M on a cartesian closed category C
equipped with such a st we will denote (C, M, st) as a st-monad.
Example 3.14 If L+ is the non-empty list monad, the derived left prestrength lstΓ is exactly the comprehension ΓF of Example 3.2. Example 3.10 provides an easy example where (Γn B) fails for n = 2.
Similarly rstΓ, which is the reverse comprehension, does not agree with lstΓ nor does it satisfy (Γn B).
Thus neither is a Kleisli strength.

72

Monad Strength

In [3], Anders Kock assumed V to be a symmetric monoidal closed category, required K to be a
monoidal monad and ν and ρ to be V -natural. Under such assumptions Kock defined K to be commutative if lstΓ = rstΓ. Thus the previous example illustrates that even with a weaker notion of commutative
monad in a cartesian closed category, K need not be commutative. For the remainder of the paper we will
let the term commutative monad refer to this weaker notion, namely a st-monad (C, M, st) in a cartesian
closed category where the derived left and right prestrengths agree, lstΓ = rstΓ. This agrees with the
usual use of this term, found for instance in [7].

3.4 Monad semantics, cartesian products, and Kleisli Strength
In [14], Wadler introduced the notion of a monadic interpreter. This application, as well as others in
computation and programming semantics, depends on interpreting terms in the Kleisli category for a
monad. In the case of monadic interpreters there is a core interpretation which applies to all monads with
small modifications made for any particular monad. Notably, the example interpreters found there and
elsewhere lack a product construct despite its obvious role in both programming and computation. This is
no doubt due to the fact that such interpreters would have to satisfy certain laws ensuring that composition
is well defined with regard to that construct in the associated Kleisli categories. As emphasized earler,
such laws are satisfied precisely when the monad is equipped with a Kleisli strength.
Suppose we are given terms t1 ,t2 where each ti is interpreted ti : A → MBi for some monad M. The
resulting term (t1 ,t2 ) should have type A → M(B1 × B2 ). This requires the existence of a prestrength
Γ : MA × MB → M(A × B) with the resulting composition Γ◦ < t1 ,t2 >. Γ must be a Kleisli strength,
a general prestrength will not do, nor even a derived pre-strength, in order for function composition to
behave properly. It does not require that Γ be commutative however. We illustrate this point with the
next example.
Let f : A → B, g : A → C, f ′ : B → B ′ , g ′ : C → C ′ be four arbitrary functions respectively. In any
cartesian category C, it follows from the definition of product that the following two compositions (of
type A → (B ′ ×C ′ )) must agree:
1) comp1 =< f ′ ◦ f , g ′ ◦ g >: A → (B ′ ×C ′ )
2) comp2 = ( f ′ × g ′ )◦ < f , g >: A → (B ′ ×C ′ ).
Example 3.15 Let MX = X + Exc be the exceptions monad of Example 3.6, where Exc now has exactly
two elements e1 and e2. For arbitrary fixed values a in A and b in B, let f (a) = η (b) (where η is the
return method), g(a) = e2, f ′ (b) = e1 and g ′ is arbitrary, all with the same type structure as above
but where the maps are now in CM , so for instance f : A → B in CM corresponds to f : A → MB in C.
Interpreting the compositions in the Kleisli category CM , comp1 : A → M(B ′ × C ′ ) and comp2 : A →
M(B ′ × C ′ ) should agree. Using the derived left prestrength lstΓ on value a, comp1(a) = e2 while
comp2(a) = e1 and so the compositions disagree. In a symmetric fashion one can show that the derived
right prestrength also fails to guarantee equality. The reader will recall that the derived right prestrength
construction is what is usually referred to as the monad strength in the sense found in [14] and thus a
product semantics with this notion of strength will fail to be correct. In contrast either Kleisli strength in
Example 3.6 will guarantee equality of the two compositions.
The above discussion illustrates that the prestrength construction leading to the usual notion of monad
strength does not generally support products in the Kleisli category, not just for the exception monad but
for many other monads such as the list, state, continuation and selection monads. In contrast Kleisli
strengths exist for many of these monads.

P. S. Mulry

73

3.5 Classical Commutative Monads and Kleisli Strength
In the next several sections we investigate the connections between the previous results and commutative
monads as well as monad compositions, where supporting results can be found in [6]. To emphasize the
connection to prior work we briefly work with symmetric monoidal categories.
Lemma 3.16 If Γ is an arbitrary Kleisli strength of order 2 on monad K = (K, ν , ρ ), define natural
transformations lΓ, rΓ by
1⊗ρB

Γ

ρA ⊗1

Γ

lΓAB = KA ⊗ B −−−−→ KA ⊗ KB −−−AB−→ K(A ⊗ B)
rΓAB = A ⊗ KB −−−−→ KA ⊗ KB −−−AB−→ K(A ⊗ B)
Then
lΓA,KB

(rΓAB )#

ΓAB = KA ⊗ KB −−−−−−→ K(A ⊗ KB) −−−−−−→ K(A ⊗ B)

(1)

Similarly ΓAB = (lΓAB )# ◦ rΓKA,B
Note that the lemma begins with an arbitrary Kleisli strength Γ of order 2 on monad K which induces
via the unit, ρ , the maps lΓ and rΓ. In essence what the lemma states is that if we use the prestrength
construction of section 3.3, the resulting prestrengths agree with each other and generate the original
Kleisli strength. Thus the notion of Kleisli strength can be seen as a natural generalization of Kock’s
commutative monads to symmetric monoidal categories that are not necessarily closed and where the
monad is no longer assumed to be a monoidal functor. This is important as very few monads of interest
to computer science are monoidal functors and so we work instead with Kleisli strength.
Checking whether a given monad has a Kleisli strength however, namely that conditions (ΓA) and
(ΓB) hold, can often be tedious and complicated, so it would be useful to have an easier characterization
for determining when Kleisli strength exists. In general this is not known but in the special case of the
prestrength construction we can generalize a result of Kock. First a useful lemma.
Lemma 3.17 Given st-monad (C, M, st), the corresponding maps rst and lst form Kleisli lifting transformations.
The proof is a straightforward diagram chase and simply checks that the following two equations hold
(in the case of rst).
1) rst ◦ (1 × η ) = η
2) µ ◦ M(rst) ◦ rst = rst ◦ (1 × µ )
Theorem 3.18 Given st-monad (C, M, st), then the derived prestrength lstΓ is a Kleisli strength if and
only if M is commutative (lstΓ = rstΓ) in which case rstΓ is also a Kleisli strength. Likewise the symmetric statement holds for rstΓ.
Proof We look at the case of lstΓAB = rst # ◦ lst : MA × MB → M(A × B). Condition (ΓA) holds since
lstΓ(ηA × ηB ) = rst # ◦ lst ◦ (η × 1) ◦ (1 × η )
= (rst # ◦ η ◦ (1 × η ) (by 3.17)
= µ ◦ η ◦ rst (1 × η ) (by naturality of rst)
= ηA×B (by 3.17).
Condition (ΓB) holds since
lstΓ(µ × µ ) = rst # ◦ lst ◦ (1 × µ ) ◦ (µ × 1) (by definition)

Monad Strength

74
= rst # ◦ M(1 × µ ) ◦ lst ◦ (µ × 1) (naturality of lst)
= µ ◦ µ ◦ MM(rst) ◦ M(rst) ◦ lst ◦ (µ × 1) (by 3.17)
= µ ◦ µ ◦ MM(rst) ◦ M(rst) ◦ µ ◦ M(lst) ◦ lst (by 3.17)
= µ ◦ µ ◦ MM(rst) ◦ µ ◦ MM(rst) ◦ M(lst) ◦ lst (by naturality of µ )
= µ ◦ µ ◦ MM(rst) ◦ µ ◦ MM(rst) ◦ M(lst) ◦ lst (by naturality of µ )
= µ ◦ M(rst) ◦ µ ◦ µ ◦ MM(rst) ◦ M(lst) ◦ lst (by naturality of µ )
= µ ◦ M(rst) ◦ µ ◦ M(µ ) ◦ MM(rst) ◦ M(lst) ◦ lst (by property of monad)
= µ ◦ M(rst) ◦ µ ◦ M(µ ) ◦ MM(lst) ◦ M(rst) ◦ lst (since lstΓ = rstΓ)
= µ ◦ M(rst) ◦ µ ◦ µ ◦ MM(lst) ◦ M(rst) ◦ lst (by property of monad)
= µ ◦ M(rst) ◦ µ ◦ M(lst) ◦ µ ◦ M(rst) ◦ lst (by naturality of µ )
= µ ◦ µ ◦ MM(rst) ◦ M(lst) ◦ µ ◦ M(rst) ◦ lst (by naturality of µ )
= µ ◦ M(µ ) ◦ MM(rst) ◦ M(lst) ◦ µ ◦ M(rst) ◦ lst (by property of monads)
= µ ◦ M(lstΓ) ◦ lstΓ

Conversely, suppose that the derived prestrength lstΓ is a Kleisli strength where lstΓ = rst # ◦ lst.
Consider the corresponding maps lst ∗ = lstΓ ◦ (1 × η ) and rst ∗ = lstΓ ◦ (η × 1). We have that lst ∗ =
lstΓ◦(1× η ) = rst # ◦M(1× η )◦lst = µ ◦M η ◦lst = lst. Also rst ∗ = lstΓ◦(η ×1) = rst # ◦lst ◦(η ×1) =
rst # ◦ η = µ ◦ η ◦ rst = rst. Thus by the argument of Lemma 3.16, the maps rst ∗ and lst ∗ arising from
lstΓ agree in turn with rst and lst respectively and so generate both lstΓ and rstΓ which agree. Thus the
monad is commutative.
Note: The last result does not characterize whether a given monad has a Kleisli strength. For example
the state monad is not commutative but does have a Kleisli strength as we note in the next example, rather
it asserts that the derived prestrength is a Kleisli strength exactly when the monad is commutative, often
a much easier condition to check.
Example 3.19 Consider the state monad M where MA = (A × S)S . Building the left and right prestrength constructions lstΓAB , rstΓAB : MA × MB → M(A × B) we have,
lstΓAB (tA ,tb ) = λ s.let (a, sA ) = tA (s), let(b, sAB ) = tB (sA ) in (a, b, sAB )
rstΓAB (tA ,tb ) = λ s.let(b, sB ) = tB (s), let(a, sBA ) = tA (sB ) in (a, b, sBA ).
By the previous theorem since lstΓ and rstΓ don’t agree, neither is a Kleisli strength, nor commutative.
On the other hand ΓAB (tA ,tb ) = λ s.let(a, sA ) = tA (s), let(b, sB ) = tB (s) in(a, b, s) is a Kleisli strength.
Example 3.20 In Example 3.6 it was shown the exceptions monad MA = X + Exc came equipped with
different Kleisli strengths for non-trivial Exc. M is not commutative however since for a, b ∈ Exc, the
derived prestrengths are lstΓ(a, b) = a while rstΓ(a, b) = b, and so lstΓ 6= rstΓ.

3.6 Composing Monadic Data Types
As the previous sections illustrate, monads play an important role in different aspects of functional programming. Since we often wish to apply more than one monad to a particular construction, finding
circumstances where they compose is of particular interest. Monads compose exactly in the presence of
a distributive law which is defined next. Finding such laws can be difficult in general, but in the presence
of Kleisli strength a large class of these laws exists.
Definition 3.21 For monads H = (H, µ , η ) and K = (K, ν , ρ ) on category C, a distributive law of H
over K is a natural transformation λ : HK → KH for which the following diagrams commute.

P. S. Mulry

H

K

75
Hρ

✲ HK

✛

❩
❩
❩ (DL A)
❩
λ
❩
ρH ❩
❩
❄
❩
⑦ KH ✛
❩

ηK

✲ HK

❩
❩
❩ (DL C)
❩
λ
❩
Kη ❩
❩
❄
❩
⑦ KH ✛
❩

Hν
(DL B)

HKK

λK

❄

KHK
Kλ

❄

νH
✛

µK
(DL D)

KKH
HHK
Hλ

❄

HKH

λH

❄

Kµ

KHH

We now return to the problem of providing a means of composing monadic types such as m[a]. The
key point is the existence of a distributive law. As pointed out in [5], a distributive law of H over K
produces the composite monad (KH, (ν µ )(K λ H), ρη ) where the four laws above ensure the laws for
a monad hold, thus providing a means of composing monadic data types. In particular, there may be
more than one such law λ for given monads H and K and it is critical to provide λ when asserting
the composition. In particular, monads equipped with Kleisli strength play an important role in the
composition with free monadic data types. We address this next.
Theorem 3.22 Let Σ be a monadic finitary signature in V with corresponding free monad (Σ@ , µ , η ).
If K = (K, ν , ρ ) is a monad in V equipped with a family of Kleisli strengths (Γω : ω ∈ Σn ) with each Γω
of order n if ω ∈ Σn , then there exists a distributive law λ : Σ@ K → KΣ@ .
The categorical proof of this result is lengthy and will be skipped, however in section 4.1 we will
sketch a proof in Haskell. This last result, and corresponding ones associated with linear monadic finitary
signatures, generate compositions involving monadic data types such as lists, trees and exceptions which
would not exist under normal circumstances, such as the list monad composed with itself, incorrectly
claimed in [2]. As emphasized earlier, Kleisli strength is a more general notion than commutativity and
thus distributive laws can exist even for non-commutative monads. Since every commutative monad is
Kleisli strong we have the immediate corollary.
Corollary 3.23 If in Theorem 3.22 K is commutative, there exists a distributive law λ : Σ@ K → KΣ@ of
Σ@ over K.
Example 3.24 The monad K = P0 of Example 3.5 has a Kleisli strength of order n. By 3.22, there exists
a distributive law λ : Σ@ P0 → P0 Σ@ for any monadic finitary signature Σ. For instance, if Σ@ is the
binary tree monad V , then λ : V P0 A → P0VA defined by λ E = {E}, λ (L(A0 )) = {L(a) : a ∈ A0 } and
λ (N(s,t)) = {N(si ,t j ) : si ∈ λ (s),ti ∈ λ (t)} is a distributive law resulting in the composite monad P0V .
Example 3.25 Similarly, for the reader monad M of Example 3.8, there exists a distributive law λ :
Σ@ M → MΣ@ for any monadic finitary signature Σ. Now when Σ@ is V , the distributive law λ is defined
to be λ (E) = λ a.E, λ (L( f )) = λ a.(L( f a)) and λ ((N(t1 ,t2 )) = λ a.(N((λ t1 )a, (λ t2 )a)), resulting in the
composite monad MV .

Monad Strength

76

The prior results provide a roadmap for constructing composite monads. They also provide a means
for testing whether such compositions are correctly defined. The following example is a case in point.
Example 3.26 An important monad operation in Haskell is the function sequence :: [m a] → m[a] i.e. a
function with type structure LMA → MLA. Since monads are at work, it is reasonable to require that the
interpretation of this operation in the Kleisli category (for monad M) is consistent. As a functor, L acting
on function f : A → B is just the ordinary map function, i.e. map :: (a → b) → ([a] → [b]) in Haskell. If
we now take into account arbitrary monad M, does map preserve the composition of functions in CM ,
namely can L (or map) now be lifted to CM where the operation sequence comes into play? If we denote
the lift of map (or L on the function f : a → m b as f : [a] → m[b], then f is defined as sequence.(map f )
and preservation of Kleisli composition requires that the property g. f = g. f should hold, which it does
not. We supply two simple examples in Haskell next.
Example 3.27 Let M be the list monad where f n = [n, 2 ∗ n], and g n = [n, 3 ∗ n], then the compositions
g. f ([1, 3]) = [[1, 3], [1, 9], [1, 6], ...] and g. f ([1, 3]) = [[1, 3], [1, 9], [3, 3]..] disagree.
Example 3.28 Let M denote the IO monad in Haskell, f : Int → IO Char, g : Char → IO () be defined
where f (n) is defined to call getChar n-times while g is simply putChar. While both g. f and g. f will
return something of type IO[()] for a given list of integers, the resulting actions will differ. For example,
we have that g. f ([3, 1, 2]) on keyboard input abc, d, e f results in abccdde f f while g. f on the same
input generates abcde f cd f and thus the compositions do not agree.
What went wrong in these last examples? The operation sequence fails to be a distributive law
because of the choice of monads M. This also is suggestive of why past examples of the list monad
composed with itself were not correct. If the monad M comes equipped with a Kleisli strength, however,
than a distributive law exists and a consistent notion of composition is possible.

4

Applying results in Haskell

As the prior section illustrates, satisfying the laws for Kleisli strength or commutativity is critical to
correctly composing monadic data types via distributive laws. Proving that these laws hold, however, can
at times be either difficult or nonintuitive, the proof of Theorem 3.18 being a case in point. It would be
very useful if these laws could be expressed in a more accessible form, such as a functional programming
format, which might allow for easier testing and verification. Additionally, we would like to generate
concrete code that might generically build the default methods required for monad composition. In this
section we provide several results in this direction using Haskell.

4.1 Kleisli Strength and Distributive Laws in Haskell
We begin by recalling some Haskell notation. Given a monad on C, H = (H, µ , η ), we note that η
correspond to the return method in Haskell while µ : HHA → H corresponds to a join function defined
in Haskell by join a = a >>= id. The bind operation >>= is a default method for the monad class in
Haskell, but it can easily be seen to correspond categorically to (a >>= f ) = join( f map f a), or put
in more categorical notation, a >>= f = µ (H f (a)) = f # a using Manes notation. A special case of
>>= is >> defined by m >> k = m >>= λ x → k where x is not free in k.
As pointed out in [1], the do-syntax provides an intuitive and convenient way of writing an abbreviated form for applying multiple bind operations. The interpretation of do is captured in the following
two rules:

P. S. Mulry

77

do e1; e2 = e1 >> e2
do p ← e1; e2 = e1 >>= (λ p → e2)
Given st-monad (C, M, st) recall that a monad is called commutative if the left and right prestrengths
lstΓ and rstΓ generated by the pre-strength construction agree. We have immediately the following
lemma.
Lemma 4.1 M is commutative exactly when the following two do expressions agree for any pair (a, b)
in MA × MB.
do
x←a
=
do
y←b
y←b
x←a
return(x, y)
return(x, y)
Proof The reader can easily check that the left (right) do-expresssions correspond exactly to the prestrength constructions lstΓ(a, b), (rstΓ(a, b)) for the given monad M.

We now consider an alternative proof in Haskell of Theorem 3.18 of the prior section. Given monad
(C, M, st) as in the theorem, then the derived prestrength lstΓ is a Kleisli strength if conditions (ΓA) and
(ΓB) of Kleisli strength hold. Focusing on (ΓB) we have the following result.
Lemma 4.2 Applying the clockwise composition of condition (ΓB) on value (a, b) in MMA × MMB
results in the following do expression in Haskell.
do
x←a
y←b
u←x
v←y
return(u, v)
Proof
Going clockwise for (a, b) and using Lemma 4.1 we have µ ◦ M(lstΓ) ◦ lstΓ(a, b) is exactly µ ◦
M(lstΓ) applied to
do
x←a
y←b
return(x, y)
Since lstΓ is natural, M(lstΓ) ◦ return(x, y) = return ◦ lstΓ(x, y) and again using Lemma 4.1 results
in µ applied to
x←a
y←b
return(x, y)
do
u←x
v←y
return(u, v)
By monad laws, applying µ simply removes the middle return.
do

Monad Strength

78

Lemma 4.3 The counterclockwise composition of condition (ΓB) on value (a, b) in MMA × MMB results in the following do expression in Haskell.
do

x←a
u←x
y←b
v←y
return(u, v)

Proof The counterclockwise composition applied to (a, b) is just lstΓ ◦ (µ × µ )(a, b). The expression
µ (a) corresponds to the do expression
do
x←a
u←x
return u
with a similar do expression for µ (b).
Applying Lemma 4.1 gives the desired result where we drop the redundant do’s.
We now apply the previous results to prove Theorem 3.18.
Theorem 4.4 Given monad (C, M, st), then the derived prestrength lstΓ is a Kleisli strength if and only
if M is commutative
Proof By Lemma 4.3 the counterclockwise composition of condition (ΓB) on value (a, b) in MMA ×
MMB corresponds to
do

x←a
u←x
y←b
v←y
return(u, v)

If M is commutative, we can swap the middle two lines resulting in the do-expression found in
Lemma 4.2 and so condition (ΓB) holds. Showing condition (ΓA) holds is trivial and left to the reader.
Conversely if lstΓ is a Kleisli strength, then condition (ΓB) holds. Applying the values
(return x, (M return) y) to the clockwise composition generates a do expression equivalent to
do
v←y
u←x
return(u, v)
which must agree with applying the same values counterclockwise generating a do expression equivalent
to
do
u←x
v←y
return(u, v)
Since x and y were arbitrary values of type M A and M B respectively, M is commutative.
We now turn our attention to the results on distributive laws found in section 3. We use Haskell
to provide a more intuitive approach to Corollary 3.23. First we state a useful lemma that provides a
definition in Haskell of the distributive laws generated by the corollary.

P. S. Mulry

79

Lemma 4.5 Let (Σ@ , µ , η ) be the free monad of Theorem 3.22 with commutative monad (K, ν , ρ , st)
both defined on C. Then the corresponding distributive law λ : Σ@ K → KΣ@ can be defined as follows
in Haskell. For each ω ∈ Σn , λ (ω (x1 , ...xn )) =
do
a1 ← λ x1
...
an ← λ xn
return (ω (a1 , ...an ))
Proof The interested reader can check the original proof found in [6] for details of the construction of
λ which is defined recursively. The do expression is a straightforward translation of that construction.
Theorem 4.6 If in Theorem 3.22 (C, K, ρ , ν , st) is commutative, there exists a distributive law of Σ@
over K, λ : Σ@ K → KΣ@ .
Proof For ease of discussion, we use a simple example of the free polynomial monad (Σ@ , µ , η ),
namely V the non-empty binary tree monad of Example 3.11(we drop the + ) where a trivial tree (i.e.
a leaf) with value x is denoted by L(x) and a tree consisting of left and right subtrees v1 and v2 by
N(v1, v2). We have four laws to check that a distributive law exists for KV .
Focusing on law (DL B) and starting with a term N( tt1, tt2) of type V KK, going clockwise
(νV ◦ K λ ◦ λ )(N( tt1, tt2)) corresponds by Lemma 4.5 to νV ◦ K λ applied to the do expression
do
t1 ← λ tt1
t2 ← λ tt2
return (N( t1, t2))
Since return is natural, (K λ ◦ return) N( t1, t2) = return(λ (N( t1, t2))) = return applied to
do
a ← λ t1
b ← λ t2
return N( a, b)
composing with ν removes the middle return and the redundant do, resulting in the do expression
do
t1 ← λ tt1
t2 ← λ tt2
a ← λ t1
b ← λ t2
return N( a, b)

do

In a similar fashion counterclockwise composition λ ◦V (ν ) generates a do expression equivalent to
t1 ← λ tt1
a ← λ t1
t2 ← λ tt2
b ← λ t2
return N( a, b)

When K is commutative, the two middle components in the latter do expression can be swapped
resulting in the clockwise composition and so (DL B) holds. The two conditions (DL A) and (DL C)
are easily verified leaving only (DL D). Since V is a recursively defined data type, ν N(tt1,tt2) =
N(ν tt1, ν tt2). Since λ is also defined recursively, condition (DL D) follows immediately by structural
recursion. The final case of considering elements of the form (L x) easily holds for all conditions and is
left to the reader.

80

Monad Strength

4.2 Some examples in Haskell
Example 4.7 One can generalize the last result to include quotients of free monads, such as the list
monad. In this case the Haskell code for the distributive law λ : [m a] → m[a] produced whenever M is
a commutative monad is defined by Lemma 4.5 as
λ [ ] = return[ ]
λ (x : xs) = do
a←x
b ← λ xs
return (a : b)
which coincides exactly with the usual definition of sequence found in Haskell. The problems arising in
Examples 3.27 and 3.28 occurred since the monads used were the list and IO monad respectively, neither
of which is commutative.
Example 4.8 It is an easy matter to define a correct distributive law for composing binary trees over
other commutative monads such as the reader monad, λ : V (r → a) → (r → Va).
Theorem 3.23 indicates that one can build composite monadic data types for any free polynomial
monad data types over commutative monads such as powerset, bag, reader, writer(for commutative
monoid) and maybe monads. Lemma 4.5 provides a roadmap for defining the corresponding distributive
laws in Haskell. What remains is to provide an explicit definition of the bind and return operators in
Haskell so we can apply these results. We do this next.
Proposition 4.9 Given a recursive polynomial monad V over a commutative monad M one can define
the resulting composite monad MV generated by distributive law λ in Haskell where the bind operation
is defined by (a >>= f ) =
do
x←a
b ← λ ( f map f x)
return(
do
y←b
v←y
return v
)
Proof The return method (η ) for MV is trivial and simply the composition of the individual return
methods, i.e. returnM ◦ returnV . Exploiting basic propeties of a monad we arrive at a definition of bind
on the composite monad MV . The join operation join : MV MV → MV is defined by µ ◦MM(ν )◦(M λ V )
which in turn is used to define the bind operation on MV via (a >>= f ) = join◦( f map f a) where f map
denotes the action of the functor on the new composite monad. Now a straightforward diagram chase
shows that
join ◦ ( f map f ) ◦ η =
µ ◦ MM(ν ) ◦ (M λV ) ◦ ( f map f ) ◦ η =
µ ◦ MM(ν ) ◦ (M λV ) ◦ η ◦ ( f map f ) =
µ ◦ MM(ν ) ◦ η ◦ λV ◦ ( f map f ) =
µ ◦ η ◦ M(ν ) ◦ λV ◦ ( f map f ) =
M(ν ) ◦ λV ◦ ( f map f )

P. S. Mulry

81

where the latter uses of f map refer to the monad V .
So (a >>= f ) corresponds to M(ν ) applied to the do expression
do
x←a
b ← λV ( f map f x)
return(ν b)
rewriting ν as a do expression and using naturality generates the desired result.
Next we provide several examples. A key point is that no actual work is required to decipher the details
of how the operators return and bind behave for these examples since it is already determined generically
by the prior results.
Example 4.10 Exploiting the previous proposition, computing the bind method for the composite monad
Maybe[a] is straightforward. For instance
Just[2, 4, 6]) >>= f = Just[2, 4, 4, 8, 6, 12] while
Just[2, 3, 6]) >>= f = Nothing where
f n = Just([n, 2 ∗ n]) if n is even and Nothing otherwise.
Example 4.11 For the composite monad r → Va of the Example 4.8 we have that given
f a = N((t1 a), (t2 a)))
t1 a = N((L a), (L (a + 1)))
t2 a = N((L (2 ∗ a)), (L (3 ∗ a)))
where g n = λ a → N((L (2 ∗ a)), (L (4 ∗ a))) if n is even
= λ a → N((L a), (L (3 ∗ a))) otherwise,
( f >>= g)(5) = N(N(N(L 5)(L 15))(N(L 10)(L 20)))(N(N(L 10)(L 20))(N(L 5)(L 15))).
Example 4.12 Consider the M-set monad MX = C × X of Example 3.9 where C is a monoid. When C is
commutative, so is M and so we can form the composite monad MVA = C × VA. Here the definition of
λ : V (C × A) → C ×VA derived from Lemma 4.5 yields for instance
λ N( L(c1 , a), L(c2 , b)) = (c1 ∗ c2 , N( (L a), (L b))).
Likewise using Proposition 4.9, f a = (a, N( L(2 ∗ a), L(3 ∗ a))) produces
(5, N( (L 3), (L 4))) >>= f = (12 , N ( N( (L 6), (L 9)), N( (L 8), (L 12) )))
where C is the commutative monoid of integers under addition.

5

Summary and Future Work

The results of section 3 indicate that there are tradeoffs on how to utilize monads to interpret products
semantically. Derived strengths are a natural consequence of the existence of an st-monad however they
may fail to provide a correct semantics except in the exceptional case when the monad is commutative.
Kleisli strengths provide an alternative approach. They generalize the notion of commutative and are
thus applicable to a much wider array of monad used in computing while also guaranteeing that products
lift to the coresponding Kleisli categories. An important application comes up in the context of monad
composition where derived strength is not sufficient, but Kleisli strength is, to guarantee the proper composition of certain monads with polynomial monadic data types. Additional restrictions on the class

Monad Strength

82

structure of monads along the lines of commutativity or Kleisli strength will thus be required to ensure
composition of functions in Kleisli. Section 4 provides an approach to earlier results using Haskell. In
addition to providing explicit expressions that can test for the existence of Kleisli strength and distributivity, it also provides the generic code required for the default methods for a monad composition class
for the compositions investigated.
Other constructs related to composing monads arise and might profit from the approach introduced
in the paper. For instance, the previous section included an example related to the monad transformer
construction. In [11] the connection between the present work on composing monads and monad transformers is explored in more detail. Another important question is understanding when Kleisli strength
is preserved under monad composition. While an initial result can be found in [6], in [10] we provide
additional examples and results that exploit the Haskell-centric approach found in this paper.

6

Acknowlegement

This paper is dedicated to David Schmidt on the occasion of his 60th birthday. David has been a friend
and colleague for many years, someone who has shown consistent care and support for his students,
colleagues, and the research community. I wish David continued success for many years to come.

References
[1] Hukak, Peterson & Fasel (1999):
A Gentle Introduction to Haskell 98.
http://www.haskell.org/tutorial/. Manuscript.

Available at

Proceedings of the 1992 Glasgow Work[2] King & Wadler (1992):
Combining monads.
Available at
shop on Functional Programming, pp. 134–143, doi:10.1007/978-1-4471-3215-8 12.
http://homepages.inf.ed.ac.uk/wadler/topics/monads.html.
[3] Kock (1970): Monads on symmetric monoidal closed categories. Archiv der Mathematik 21(1), pp. 1–10,
doi:10.1007/BF01220868.
[4] Manes (1976): Algebraic Theories.
doi:10.1007/978-1-4612-9860-1.

Graduate Texts in Mathematics 26, Springer Verlag,

[5] Manes & Mulry (2007): Monad Compositions I: General Constructions and Recursive DisTheory and Applications of Categories 18(7), pp. 172–208.
Available at
tributive laws.
www.tac.mta.ca/tac/volumes/18/7/18-07.pdf.
[6] Manes & Mulry (2008): Monad Compositions II: Kleisli Strength. Mathematical Structures in Computer
Science 18(3), pp. 613–643, doi:10.1017/S0960129508006695.
[7] Moggi (1991): Notions of computation and monads. Information and Computation 18(3), pp. 55 – 92,
doi:10.1016/0890-5401.
[8] Mulry (1992): Strong monads, algebras and fixed points. London Math Society Lecture Series 177, pp.
202–216, doi:10.1017/CBO9780511525902.012.
[9] Mulry (1994): Lifting theorems for Kleisli categories. Springer Lecture Notes in Computer Science 802, pp.
304–319, doi:10.1007/3-540-58027-1 15.
[10] Mulry (2013): Interchange laws for monads. To appear.
[11] Mulry (2013): Monad transformers and distributive laws. To appear.
[12] Scott (1970): Outline of a mathematical theory of computation. Oxford University Computing Laboratory
Technical Monograph PRG-2(3).

P. S. Mulry

83

[13] Street (1972): The formal theory of monads.
J. Pure Appl. Algebra 2(2), pp. 149 – 168,
doi:10.1016/0022-4049(72)90019-9.
[14] Wadler (1992): Comprehending Monads. Mathematical Structures in Computer Science 2(4), pp. 461–493,
doi:10.1017/S0960129500001560.

