Download Monad Transformers as Monoid Transformers PDF

TitleMonad Transformers as Monoid Transformers
LanguageEnglish
File Size328.1 KB
Total Pages43
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.

Similer Documents