##### Document Text Contents

Page 1

Monad Transformers as Monoid Transformers

Mauro Jaskelioff

CIFASIS/Universidad Nacional de Rosario, Argentina

Eugenio Moggi1

DISI, Università di Genova, Italy

Abstract

The incremental approach to modular monadic semantics constructs complex

monads by using monad transformers to add computational features to a pre-

existing monad. A complication of this approach is that the operations associ-

ated to the pre-existing monad need to be lifted to the new monad.

In a companion paper by Jaskelioff, the lifting problem has been addressed

in the setting of system Fω. Here, we recast and extend those results in a

category-theoretic setting. We abstract and generalize from monads to monoids

(in a monoidal category), and from monad transformers to monoid transformers.

The generalization brings more simplicity and clarity, and opens the way for

lifting of operations with applicability beyond monads.

Key words: Monad, Monoid, Monoidal Category

1. Introduction

Since monads have been proposed to model computational effects [31, 32],

they have proven to be extremely useful also to structure functional programs

[42, 41, 18]. In these applications monads come with operations to manipulate

the computational effects they model. For example, an exception monad may

come with operations for throwing an exception and for handling it, and a

state monad may come with operations for reading and updating the state.

Consequently, the structures one is really working with are monads and a set

of operations associated to them. The monadic approach to the denotational

semantics of a programming language, which has been adapted also to other

forms of programming language semantics based on interpreters [25] or compilers

[24], consists of three steps [33, 7]:

Email addresses: [email protected] (Mauro Jaskelioff),

[email protected] (Eugenio Moggi)

1Partially supported by Italian PRIN 2008 “Metodi Costruttivi in Topologia, Algebra e

Fondamenti dell’Informatica”.

Preprint submitted to Theoretical Computer Science March 25, 2010

Page 2

2

• identify a metalanguage with computational types, to hide the interpreta-

tion of computational types and operations manipulating computations;

• define a translation of the programming language into the metalanguage;

• give a denotational semantics of the metalanguage, by interpreting com-

putational types and operations on computations using a monad and a set

of operations associated to it.

However, there is a caveat: when the programming language involves a mixture

of computational effects, the number of operations for manipulating compu-

tations grows, the monad needed to interpret computational types gets more

complex, and the semantics of operations associated to it gets more complex,

too. To tackle these issues one can adopt a modular approach, which provides

basic building blocks and constructs to build more complex blocks. Roughly

speaking, one can identify two modular approaches

• the incremental approach, taken in [25, 33, 7], uses unary constructs, called

monad transformers, which build complex monads by adding one compu-

tational feature to a pre-existing monad;

• the compositional approach, taken in [27, 15], uses binary constructs, called

monad combinations2, for combining two pre-existing monads.

Both approaches fall short in dealing with operations associated to monads.

This problem was identified in [25], which proposed a non-modular workaround,

namely to lift in an ad-hoc manner an operation through a monad transformer.

Therefore, the number of liftings grows like the product of the number of monad

transformers and operations involved. Alternatively, one may achieve modular-

ity by restricting the format of operations. For instance, algebraic operations in

the sense of [35] are easy to lift, but the monadic approach becomes of limited

applicability if all operations have to be algebraic.

The compositional approach fits with the algebraic view of computational

effects advocated in [35], and the combinations proposed in [15] give natural

ways to combine monads induced by algebraic theories and to lift algebraic

operations. However, some computational monads are not induced by algebraic

theories, and some operations on computations are not algebraic.

The incremental approach is popular among functional programmers, be-

cause monad transformers are easy to implement. However, there has been lim-

ited progress in addressing the lifting problem, until a new insight was brought

by [16, 17]. Jaskelioff gives a uniform way of lifting operations in a certain

class (which includes all the operations described in [25]) through any functo-

rial monad transformer. This lifting has been implemented in Haskell [16] and

studied in the setting of system Fω [17]. On algebraic operations it agrees with

the straigthforward lifting, and it is compatible with most of the ad-hoc liftings

found in the literature or in Haskell’s libraries.

2In the context of [15] it is more appropriate to call them theory combinations.

Page 21

21

Definition 3.1 (Operations). Given a monoid M̂ = (M, e,m) and a functor

H : Mon(Ê) - E, an H-operation for M̂ is a map op : HM̂ - M in E.

A first-order operation of arity A ∈ E for M̂ is a map op : A⊗M - M ,

i.e. an H-operation for H(−) = A⊗U(−), and such op is called algebraic when

s : A, x1, x2 : M ` op(s, x1) · x2 = op(s, x1 · x2) : M (3.1)

Definition 3.2 (Lifting). Given an H-operation op : HM̂1 - M1 for M̂1

and a monoid map h : M̂1 - M̂2, an H-operation op : HM̂2 - M2 for

M̂2 is a lifting of op along h when

HM̂2

op

- M2

HM̂1

Hh

6

op

- M1

Uh

6

(3.2)

Remark 3.3. Equation (3.1) is equivalent to

s : A, x : M ` op(s, x) = op(s, e) · x : M (3.3)

From this it is immediate to establish a bijective correspondence between alge-

braic operations op : A⊗M - M for M̂ and maps op′ : A - M

op′(s : A) : M =̂ op(s, e)

op(s : A, x : M) : M =̂ op′(s) · x

Diagram (3.2) is equivalent to the equation

s : A, x : M1 ` h(op(s, x)) = op(s, h(x)) : M2 (3.4)

when H(−) = A⊗ U(−). �

Theorem 3.4 (Unique algebraic lifting). Given h : M̂1 - M̂2 monoid

map and op : A⊗M1 - M1 algebraic for M̂1, let op] : A⊗M2 - M2 be

op] (s : A, x : M2) : M2 =̂ h(op(s, e1)) ·2 x (3.5)

then op] is the unique lifting of op along h which is algebraic for M̂2.

Proof. By definition op] is algebraic for M̂2. Let Eq be the set of equations

saying that h : M̂1 - M̂2 and op : A⊗M1 - M1 is algebraic for M̂1. Let

Eqop be Eq plus the equations saying that op : A ⊗M2 - M2 is algebraic

for M̂2 and is a lifting of op along h. The claims that op] is a lifting of op along

h and uniqueness amount to the following equations

Page 22

22

• s : A, x : M1 `Eq op](s, h(x)) = h(op(s, x)) : M2

op](s, h(x)) by definition

h(op(s, e1)) ·2 h(x) by (2.16) in Eq

h(op(s, e1) ·1 x) by (3.3) in Eq

h(op(s, x))

• s : A, x : M2 `Eqop op(s, x) = op](s, x) : M2

op(s, x) by (3.3) in Eqop

op(s, e2) ·2 x by (2.15) in Eqop

op(s, h(e1)) ·2 x by (3.4) in Eqop

h(op(s, e1)) ·2 x by definition

op](s, x)

�

Remark 3.5. An algebraic operation may have several liftings along a monoid

map. For instance, take Set with the monoidal structure given by finite products

(see Example 2.14), a monoid M̂ = (M, e, ·) and an op : M - M algebraic for

M̂ , i.e. op(x) = op′ · x where op′ = op(e). Define the monoids 2̂ =̂ ({0, 1}, 1, ∗)

and N̂ =̂ M̂ × 2̂, and consider the monoid map h : M̂ - N̂ given by

h(x) =̂ (x, 1). The unique algebraic lifting of op along h is op](x, b) = (op′ ·x, b),

a different lifting of op along h is given by op(x, b) =̂ (op′ · x, 1). �

3.1. Examples of Operations

Among the different

avours of monads, strong monads are those needed to

interpret the monadic metalanguage of [31, 32]. In this section we give examples

of strong monads (on a cartesian closed category) and associated operations,

saying whether the operations are algebraic, first-order or H-operations. There

are equivalent ways of defining strong monads on a cartesian closed category

C, we borrow the definition adopted in Haskell, and freely use simply typed

lambda-calculus as internal language to denote objects and maps in C.

Definition 3.6 (Strong Monad). A strong monad on a cartesian closed cat-

egory C is a triple M̂ = (M, retM , bindM ) consisting of

• a mapM : |C| - |C| on the objects ofC

• a family retMX : X - MX of maps withX ∈ C

• a family bindMX,Y : MX × (MY )X - MY of maps withX,Y ∈ C

such that for everya : A, f : (MB)A, u : MA and g : (MC)B

bindMA,B(ret

M

A (a), f) = f a

bindMA,A(u, ret

M

A ) = u

bindMA,C(u, λa : A. bind

M

B,C(f a, g)) = bind

M

B,C(bind

M

A,B(u, f), g)

Page 42

42

[19] G.M. Kelly. A unified treatment of transfinite constructions for free alge-

bras, free monoids, colimits, associated sheaves, and so on. Bull. of the

Aust. Math. Soc., 22(01):1–83, 1980.

[20] G.M. Kelly, J. Power. Adjunctions whose counits are coequalizers and pre-

sentations of finitary monads. J. of Pure and Appl. Algebra, 89(1–2):163–

179, 1993.

[21] G.M. Kelly, R.H. Street. Review of the elements of 2-categories. In A. Dold,

B. Eckmann, editors, Category Seminar, volume 420 of Lect. Notes in

Math.. Springer, 1974.

[22] J. Lambek. From lambda calculus to cartesian closed categories. In To H.B.

Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism,

pages 375–402. Academic Press, 1980.

[23] J. Lambek, PJ Scott. Introduction to Higher Order Categorical Logic. Cam-

bridge University Press, 1986.

[24] S. Liang, P. Hudak. Modular denotational semantics for compiler construc-

tion. In H.R. Nielson, editor, ESOP, volume 1058 of Lect. Notes in Comput.

Sci., pages 219–234. Springer, 1996.

[25] S. Liang, P. Hudak, M. Jones. Monad transformers and modular inter-

preters. In 22nd ACM SIGPLAN-SIGACT Symposium on Principles of

Programming Languages, pages 333–343, 1995.

[26] J.R. Longley. Realizability toposes and language semantics. PhD thesis,

University of Edinburgh, 1994.

[27] C. Lüth, N. Ghani. Composing monads using coproducts. In 7th ACM SIG-

PLAN International Conference on Functional Programming , pages 133–

144, 2002.

[28] S. Mac Lane. Categories for the Working Mathematician. Number 5 in

Graduate Texts in Mathematics. Springer-Verlag, 1971. Second edition,

1998.

[29] E.G. Manes. Algebraic Theories. Springer-Verlag, 1976.

[30] E.G. Manes. Implementing collection classes with monads. Math. Struct.

in Comput. Sci., 8(3):231–276, 1998.

[31] E. Moggi. Computational lambda-calculus and monads. In 4th Annual

Symposium on Logic in Computer Science, pages 14–23. IEEE Computer

Society, 1989.

[32] E. Moggi. Notions of computation and monads. Inf. and Comput., 93(1):55–

92, 1991.

Page 43

43

[33] E. Moggi. Metalanguages and applications. In Semantics and Logics of

Computation, Publications of the Newton Institute. CUP, 1997.

[34] Andrew M. Pitts. Tripos theory in retrospect. Math. Struct. in Comput.

Sci., 12(3):265–279, 2002.

[35] G.D. Plotkin, J. Power. Semantics for algebraic operations. Electr. Notes

Theor. Comput. Sci., 45, 2001.

[36] G.D. Plotkin, J. Power. Notions of computation determine monads. In

M. Nielsen, U. Engberg, editors, FoSSaCS, volume 2303 of Lect. Notes in

Comput. Sci., pages 342–356. Springer, 2002.

[37] G.D. Plotkin, M. Pretnar. Handlers of algebraic effects. In G. Castagna

[10], pages 80–94.

[38] J. Polakow, F. Pfenning. Natural deduction for intuitionistic non-

communicative linear logic. In J.-Y. Girard, editor, TLCA, volume 1581 of

Lect. Notes in Comput. Sci., pages 295–309. Springer, 1999.

[39] J. Power, E. Robinson. Premonoidal categories and notions of computation.

Math. Struct. in Comput. Sci., 7(5):453–468, 1997.

[40] D.S. Scott. Relating theories of the � -calculus. In R. Hindley, J. Seldin,

editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus

and Formalism. Academic Press, 1980.

[41] P. Wadler. Comprehending monads. Math. Struct. in Comput. Sci.,

2(4):461–493, 1992.

[42] P. Wadler. The essence of functional programming. In 9th Annual ACM

SIGPLAN-SIGACT Symposium on Principles of Programming Languages,

pages 1–14, 1992.

Monad Transformers as Monoid Transformers

Mauro Jaskelioff

CIFASIS/Universidad Nacional de Rosario, Argentina

Eugenio Moggi1

DISI, Università di Genova, Italy

Abstract

The incremental approach to modular monadic semantics constructs complex

monads by using monad transformers to add computational features to a pre-

existing monad. A complication of this approach is that the operations associ-

ated to the pre-existing monad need to be lifted to the new monad.

In a companion paper by Jaskelioff, the lifting problem has been addressed

in the setting of system Fω. Here, we recast and extend those results in a

category-theoretic setting. We abstract and generalize from monads to monoids

(in a monoidal category), and from monad transformers to monoid transformers.

The generalization brings more simplicity and clarity, and opens the way for

lifting of operations with applicability beyond monads.

Key words: Monad, Monoid, Monoidal Category

1. Introduction

Since monads have been proposed to model computational effects [31, 32],

they have proven to be extremely useful also to structure functional programs

[42, 41, 18]. In these applications monads come with operations to manipulate

the computational effects they model. For example, an exception monad may

come with operations for throwing an exception and for handling it, and a

state monad may come with operations for reading and updating the state.

Consequently, the structures one is really working with are monads and a set

of operations associated to them. The monadic approach to the denotational

semantics of a programming language, which has been adapted also to other

forms of programming language semantics based on interpreters [25] or compilers

[24], consists of three steps [33, 7]:

Email addresses: [email protected] (Mauro Jaskelioff),

[email protected] (Eugenio Moggi)

1Partially supported by Italian PRIN 2008 “Metodi Costruttivi in Topologia, Algebra e

Fondamenti dell’Informatica”.

Preprint submitted to Theoretical Computer Science March 25, 2010

Page 2

2

• identify a metalanguage with computational types, to hide the interpreta-

tion of computational types and operations manipulating computations;

• define a translation of the programming language into the metalanguage;

• give a denotational semantics of the metalanguage, by interpreting com-

putational types and operations on computations using a monad and a set

of operations associated to it.

However, there is a caveat: when the programming language involves a mixture

of computational effects, the number of operations for manipulating compu-

tations grows, the monad needed to interpret computational types gets more

complex, and the semantics of operations associated to it gets more complex,

too. To tackle these issues one can adopt a modular approach, which provides

basic building blocks and constructs to build more complex blocks. Roughly

speaking, one can identify two modular approaches

• the incremental approach, taken in [25, 33, 7], uses unary constructs, called

monad transformers, which build complex monads by adding one compu-

tational feature to a pre-existing monad;

• the compositional approach, taken in [27, 15], uses binary constructs, called

monad combinations2, for combining two pre-existing monads.

Both approaches fall short in dealing with operations associated to monads.

This problem was identified in [25], which proposed a non-modular workaround,

namely to lift in an ad-hoc manner an operation through a monad transformer.

Therefore, the number of liftings grows like the product of the number of monad

transformers and operations involved. Alternatively, one may achieve modular-

ity by restricting the format of operations. For instance, algebraic operations in

the sense of [35] are easy to lift, but the monadic approach becomes of limited

applicability if all operations have to be algebraic.

The compositional approach fits with the algebraic view of computational

effects advocated in [35], and the combinations proposed in [15] give natural

ways to combine monads induced by algebraic theories and to lift algebraic

operations. However, some computational monads are not induced by algebraic

theories, and some operations on computations are not algebraic.

The incremental approach is popular among functional programmers, be-

cause monad transformers are easy to implement. However, there has been lim-

ited progress in addressing the lifting problem, until a new insight was brought

by [16, 17]. Jaskelioff gives a uniform way of lifting operations in a certain

class (which includes all the operations described in [25]) through any functo-

rial monad transformer. This lifting has been implemented in Haskell [16] and

studied in the setting of system Fω [17]. On algebraic operations it agrees with

the straigthforward lifting, and it is compatible with most of the ad-hoc liftings

found in the literature or in Haskell’s libraries.

2In the context of [15] it is more appropriate to call them theory combinations.

Page 21

21

Definition 3.1 (Operations). Given a monoid M̂ = (M, e,m) and a functor

H : Mon(Ê) - E, an H-operation for M̂ is a map op : HM̂ - M in E.

A first-order operation of arity A ∈ E for M̂ is a map op : A⊗M - M ,

i.e. an H-operation for H(−) = A⊗U(−), and such op is called algebraic when

s : A, x1, x2 : M ` op(s, x1) · x2 = op(s, x1 · x2) : M (3.1)

Definition 3.2 (Lifting). Given an H-operation op : HM̂1 - M1 for M̂1

and a monoid map h : M̂1 - M̂2, an H-operation op : HM̂2 - M2 for

M̂2 is a lifting of op along h when

HM̂2

op

- M2

HM̂1

Hh

6

op

- M1

Uh

6

(3.2)

Remark 3.3. Equation (3.1) is equivalent to

s : A, x : M ` op(s, x) = op(s, e) · x : M (3.3)

From this it is immediate to establish a bijective correspondence between alge-

braic operations op : A⊗M - M for M̂ and maps op′ : A - M

op′(s : A) : M =̂ op(s, e)

op(s : A, x : M) : M =̂ op′(s) · x

Diagram (3.2) is equivalent to the equation

s : A, x : M1 ` h(op(s, x)) = op(s, h(x)) : M2 (3.4)

when H(−) = A⊗ U(−). �

Theorem 3.4 (Unique algebraic lifting). Given h : M̂1 - M̂2 monoid

map and op : A⊗M1 - M1 algebraic for M̂1, let op] : A⊗M2 - M2 be

op] (s : A, x : M2) : M2 =̂ h(op(s, e1)) ·2 x (3.5)

then op] is the unique lifting of op along h which is algebraic for M̂2.

Proof. By definition op] is algebraic for M̂2. Let Eq be the set of equations

saying that h : M̂1 - M̂2 and op : A⊗M1 - M1 is algebraic for M̂1. Let

Eqop be Eq plus the equations saying that op : A ⊗M2 - M2 is algebraic

for M̂2 and is a lifting of op along h. The claims that op] is a lifting of op along

h and uniqueness amount to the following equations

Page 22

22

• s : A, x : M1 `Eq op](s, h(x)) = h(op(s, x)) : M2

op](s, h(x)) by definition

h(op(s, e1)) ·2 h(x) by (2.16) in Eq

h(op(s, e1) ·1 x) by (3.3) in Eq

h(op(s, x))

• s : A, x : M2 `Eqop op(s, x) = op](s, x) : M2

op(s, x) by (3.3) in Eqop

op(s, e2) ·2 x by (2.15) in Eqop

op(s, h(e1)) ·2 x by (3.4) in Eqop

h(op(s, e1)) ·2 x by definition

op](s, x)

�

Remark 3.5. An algebraic operation may have several liftings along a monoid

map. For instance, take Set with the monoidal structure given by finite products

(see Example 2.14), a monoid M̂ = (M, e, ·) and an op : M - M algebraic for

M̂ , i.e. op(x) = op′ · x where op′ = op(e). Define the monoids 2̂ =̂ ({0, 1}, 1, ∗)

and N̂ =̂ M̂ × 2̂, and consider the monoid map h : M̂ - N̂ given by

h(x) =̂ (x, 1). The unique algebraic lifting of op along h is op](x, b) = (op′ ·x, b),

a different lifting of op along h is given by op(x, b) =̂ (op′ · x, 1). �

3.1. Examples of Operations

Among the different

avours of monads, strong monads are those needed to

interpret the monadic metalanguage of [31, 32]. In this section we give examples

of strong monads (on a cartesian closed category) and associated operations,

saying whether the operations are algebraic, first-order or H-operations. There

are equivalent ways of defining strong monads on a cartesian closed category

C, we borrow the definition adopted in Haskell, and freely use simply typed

lambda-calculus as internal language to denote objects and maps in C.

Definition 3.6 (Strong Monad). A strong monad on a cartesian closed cat-

egory C is a triple M̂ = (M, retM , bindM ) consisting of

• a mapM : |C| - |C| on the objects ofC

• a family retMX : X - MX of maps withX ∈ C

• a family bindMX,Y : MX × (MY )X - MY of maps withX,Y ∈ C

such that for everya : A, f : (MB)A, u : MA and g : (MC)B

bindMA,B(ret

M

A (a), f) = f a

bindMA,A(u, ret

M

A ) = u

bindMA,C(u, λa : A. bind

M

B,C(f a, g)) = bind

M

B,C(bind

M

A,B(u, f), g)

Page 42

42

[19] G.M. Kelly. A unified treatment of transfinite constructions for free alge-

bras, free monoids, colimits, associated sheaves, and so on. Bull. of the

Aust. Math. Soc., 22(01):1–83, 1980.

[20] G.M. Kelly, J. Power. Adjunctions whose counits are coequalizers and pre-

sentations of finitary monads. J. of Pure and Appl. Algebra, 89(1–2):163–

179, 1993.

[21] G.M. Kelly, R.H. Street. Review of the elements of 2-categories. In A. Dold,

B. Eckmann, editors, Category Seminar, volume 420 of Lect. Notes in

Math.. Springer, 1974.

[22] J. Lambek. From lambda calculus to cartesian closed categories. In To H.B.

Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism,

pages 375–402. Academic Press, 1980.

[23] J. Lambek, PJ Scott. Introduction to Higher Order Categorical Logic. Cam-

bridge University Press, 1986.

[24] S. Liang, P. Hudak. Modular denotational semantics for compiler construc-

tion. In H.R. Nielson, editor, ESOP, volume 1058 of Lect. Notes in Comput.

Sci., pages 219–234. Springer, 1996.

[25] S. Liang, P. Hudak, M. Jones. Monad transformers and modular inter-

preters. In 22nd ACM SIGPLAN-SIGACT Symposium on Principles of

Programming Languages, pages 333–343, 1995.

[26] J.R. Longley. Realizability toposes and language semantics. PhD thesis,

University of Edinburgh, 1994.

[27] C. Lüth, N. Ghani. Composing monads using coproducts. In 7th ACM SIG-

PLAN International Conference on Functional Programming , pages 133–

144, 2002.

[28] S. Mac Lane. Categories for the Working Mathematician. Number 5 in

Graduate Texts in Mathematics. Springer-Verlag, 1971. Second edition,

1998.

[29] E.G. Manes. Algebraic Theories. Springer-Verlag, 1976.

[30] E.G. Manes. Implementing collection classes with monads. Math. Struct.

in Comput. Sci., 8(3):231–276, 1998.

[31] E. Moggi. Computational lambda-calculus and monads. In 4th Annual

Symposium on Logic in Computer Science, pages 14–23. IEEE Computer

Society, 1989.

[32] E. Moggi. Notions of computation and monads. Inf. and Comput., 93(1):55–

92, 1991.

Page 43

43

[33] E. Moggi. Metalanguages and applications. In Semantics and Logics of

Computation, Publications of the Newton Institute. CUP, 1997.

[34] Andrew M. Pitts. Tripos theory in retrospect. Math. Struct. in Comput.

Sci., 12(3):265–279, 2002.

[35] G.D. Plotkin, J. Power. Semantics for algebraic operations. Electr. Notes

Theor. Comput. Sci., 45, 2001.

[36] G.D. Plotkin, J. Power. Notions of computation determine monads. In

M. Nielsen, U. Engberg, editors, FoSSaCS, volume 2303 of Lect. Notes in

Comput. Sci., pages 342–356. Springer, 2002.

[37] G.D. Plotkin, M. Pretnar. Handlers of algebraic effects. In G. Castagna

[10], pages 80–94.

[38] J. Polakow, F. Pfenning. Natural deduction for intuitionistic non-

communicative linear logic. In J.-Y. Girard, editor, TLCA, volume 1581 of

Lect. Notes in Comput. Sci., pages 295–309. Springer, 1999.

[39] J. Power, E. Robinson. Premonoidal categories and notions of computation.

Math. Struct. in Comput. Sci., 7(5):453–468, 1997.

[40] D.S. Scott. Relating theories of the � -calculus. In R. Hindley, J. Seldin,

editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus

and Formalism. Academic Press, 1980.

[41] P. Wadler. Comprehending monads. Math. Struct. in Comput. Sci.,

2(4):461–493, 1992.

[42] P. Wadler. The essence of functional programming. In 9th Annual ACM

SIGPLAN-SIGACT Symposium on Principles of Programming Languages,

pages 1–14, 1992.