An Abstract View of Programming Languages1
Eugenio Moggi
Lab. for Found. of Comp. Sci.
University of Edinburgh
EH9 3JZ Edinburgh, UK
em@lfcs.edinburgh.ac.uk
June 1989

1These Notes were produced at Stanford University as part of the course CS 359

taught in Spring Term 1989. A special thank to John Mitchell, who made my visit
to Stanford possible, and to all students who attended the course and provided usefulfeedback.

Abstract
The aim of these course notes is to show that notions and ideas from Category
Theory can be useful tools in Computer Science, by illustrating some recent applications to the study of programming languages based on the principle \notionsof computation as monads". The main objective is to propose a uni ed approachto the denotational semantics of programming languages. The category-theoretic
notions introduced in the course will be presented with speci c applications inmind (so that they will not sound too abstract) and guidelines for linking abstract
and concrete concepts will be stressed.

Contents
1 Introduction

2

2 A review of some category-theoretic concepts

7

3 Notions of computation as monads

12

4 Denotational Semantics and monads

25

1.1 Why Category Theory : : : : : : : : : : : : : : : : : : : : : : : : :1.2 Overview of the course : : : : : : : : : : : : : : : : : : : : : : : : :2.1 2-categories : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :3.1 Calculi and programming languages : : : : : : : : : : : : : : : : :3.2 Notions of computation as monads : : : : : : : : : : : : : : : : : :3.2.1 A justi cation for monads : : : : : : : : : : : : : : : : : : :3.2.2 A simple metalanguage : : : : : : : : : : : : : : : : : : : :3.2.3 Extending the metalanguage : : : : : : : : : : : : : : : : :4.1 Some examples of monad constructions : : : : : : : : : : : : : : : :4.1.1 Exceptions : : : : : : : : : : : : : : : : : : : : : : : : : : :4.1.2 Side-e ects : : : : : : : : : : : : : : : : : : : : : : : : : : :4.1.3 Continuations : : : : : : : : : : : : : : : : : : : : : : : : : :4.1.4 Variable sets and dynamic allocation : : : : : : : : : : : : :4.1.5 Communication and interleaving : : : : : : : : : : : : : : :

1

3
5
7

12
16
17
20
21
27
30
31
34
35
38

Chapter 1
Introduction
The aim of this course is to show that notions and ideas from Category Theory canbe useful tools in Computer Science for formulating de nitions and theories
and structuring complex concepts, by illustrating some recent applications
to the study of programming languages ([Mog89b, Mog89a])1. To motivate theuse of Category Theory made in these notes, I nd particularly enlightening few
passages from Chapter 2 of [Mos89], where Mosses gives an overview of Denotation
Semantics focusing not only on its achievements, but also on its failures.

Successes:
 mathematical models for programming languages (compare with opera-

tional and axiomatic approach) canonical de nition of the meaning of programs (denotational model)
 documents the design of a programming language establishes a standard for implementations, but does not specify the techniques used in implementations
 provides a basis for reasoning about the correctness (but not the complexity) of programs - either directly or indirectly, like in LCF (see [GMW79])
 promotes insight regarding concepts underlying programming languages(design with formal semantics in mind)

There is another application that I would have liked to consider in this course, namely thestudy data-re nement via natural transformations (see [HJ]). However, I did not feel con dent
enough to present this subject, where work is still in progress.
1

2

Failures:
 the denotations of simple expressions, e.g. integer expressions, might haveto be changes, when the programming language is extended (see Page 70
of [Mos89])
 Denotational Semantics is feasible for toy programming languages, butdoes not scale up easily to real programming languages (see Page 106of [Mos89])
 it is not feasible to re-use parts of the description of one programming
language into another (see Page 106 of [Mos89]).
Mosses stresses as a major shortcoming of Denotational Semantics the lack ofmodularity. One would like to consider various features of programming languages in isolation, so that a study of them is feasible, but then one has to face
the problem of putting the peaces together to form complex theories for real programming languages. In Logic it is fairly straightforward to put theories together,and Type Theory has exploited this for studying di erent type constructions in
isolation and then combine them to form complex typed languages, however: types are not the only feature of programming languages, actually in simple
imperative languages types are the easy part
 there are complex concepts, e.g. that of topological group, that are notobtained by putting together the concepts of group and topological space inthe obvious way
There should be various ways of composing theories/concepts, and a study ofsuch compositions is of great importance for using a structured approach to
the developement of concepts.

1.1 Why Category Theory
Category Theory developed mainly from Algebraic Topology through a process ofabstraction, and after some of the fundamental notions had been properly formulated it has been applied to various areas of Mathematics (for our applications theconcepts used in Categorical Logic, the study of Logic through Category Theory,
will be particularly useful). These applications have sometimes required/suggested
new fundamental notions.

What does Category Theory o er:
 a way of thinking and general guidelines3 an abstract view of objects, which hide the internal structure{ set ! object{ function ! morphism
and focus on how objects interrelate a syntax independent view of languages/theories (suggested by Categorical Logic)

What to do for using Category Theory
 reformulate intuitive ideas or mathematical concepts in category-theoretic

term, e.g. datatype constructors as adjoint functors.
 device languages, formal systems or logics to provide a more friendly interface to technical achievements/concepts (category-theoretic or whatever)and to make them usable by a wider number of people, e.g. lambda calculus
as formal system for cartesian closed categories (see [Sco80]).
In order to give the user some exibility, it is important to allow extensionsof languages and additions of axioms. So formal systems should describe
entailment relations rather than speci c theories.
In Computer Science, like in Physics, theories have to be tested. Category Theory in itself cannot be tested, because it is not about Computer Science. What has
to be judged is the way computer science concepts are linked to category-theoretic
ones, and what advantages (if any) are obtained by going through Category Theory.

Why not other theories. There are other theories that may take the metarole played by Category Theory: Universal Algebra, Logic, Type Theory. Noneof them reach the level of abstraction possible in Category Theory, and some ofthem has not accumulated enough technical tools or general methodologies to copewith a wide range of situations (spanning several elds of mathematics). However,these theories can be better than Category Theory for more speci c applications.

The three levels. A concept can be viewed at three di erent levels: intuitive, where the concept is usually explained by examples, but has notbeen formalised or made precised mathematical, where the concept has been rigorously de ned, so that theexamples given at the lower level t into it4 abstract, where the mathematical concept has been abstracted from thecontext in which it was made precise, and therefore can be instanciated into
other contexts (not considered before)
The existence of the rst two levels does not require much justi cation. However,the need of an abstract level (and of Category Theory) has not always been recognised in Mathematics, because it looks like delaying the solution of a problem byreformulating it in a more abstract terms. The de nition of topological group,
exempli es why one need the concept of group at a more abstract level (group ina category), in order to export it from the context of sets to that of topologicalspaces.

1.2 Overview of the course
1. A Categorical Manifesto (see [Gog89]) with a textbook on Category Theory(e.g. [Mac71, Gol79, BW85]):
 basic concepts of Category Theory
 their manifestations in areas related to Computer Science methodological guidelines
The paradigm of Categorical Logic (see [KR77]) applied to programming
languages
2. Feature 1: notion of computation as monad (see [Mog89b])
 how the idea developed
 a justi cation of why monads
 a language for monads and tensorial strength how to achieve modularity: monad morphisms and monad constructions
 Denotational Semantics (see [Sch86]) revisited
3. Feature 2: the distinction types/programs and program modules (see [Mog89a])
 the type-theoretic explanation and basic ideas ([Mac86, HM88])
 a critique of the type-theoretic explanation: programming languages as
indexed-categories
 higher order modules
4. Composition of features, the inadequacy of the Categorical Logic paradigm
and the need of the abstract level (see [Mog89a]): programming languages
as objects of a 2-category5 category ! object
 functor ! 1-morphism natural transformation ! 2-morphism

6Chapter 2
A review of some category-theoretic
concepts
 textbooks: rst four chapters of [Mac71] or tutorial chapter of [Pie88]
 Category Theory as methodology: [Gog89]
 an overview of Categorical Logic (see [KR77])

2.1 2-categories
In the simplest form of categorical doctrine (see [KR77]), the one for algebraic
theories, the identi cation
 theory as category model as functor
 homomorphism as natural transformationis already unsatisfactory, because we really relate theories to categories with distinguished nite products and models to functors preserving nite products on
the nose, and more generally
 theory as category with additional structure model as structure preserving functor
 homomorphism as natural transformation : : :The vagueness of \with additional structure" demand a more radical step, which
abstracts from the category of small categories (with some additional structures) in
the same way as the de nition of category abstract from its paradigmatic example:
the category of sets.
7

The most natural outcome of this abstraction is the notion of 2-category, where
the category structure is enriched with a notion of morphism between morphisms ,mimicing the properties of natural transformations. We recall the de nitions of
2-category, 2-functor and 2-natural transformation, i.e. the Cat-enriched analogueof category, functor and natural transformation (see [Kel82]).
De nition 2.1.1 A 2-category C is a Cat-enriched category, i.e.
 a class of objects Obj(C ) for every pair of objects c1 and c2 a category C (c1; c2)
 for every object c an object idc of C (c; c) and for every triple of objects c1, c2
and c3 a functor compc1 ;c2 ;c3 from C (c1 ; c2)  C (c2; c3 ) to C (c1; c3) satisfying
the associativity and identity axioms{ comp( ; comp( ; )) = comp(comp( ; ); ){ comp(id; ) = = comp( ; id)
CC

Notation 2.1.2 An object f of C (c1; c2) is called a 1-morphism, while an arrow is called a 2-morphism. We write ; for comp( ; )
f1

c1

# 1

!
!

f2

# 2

c2

f1; f2!
!

f2
f1
and  for composition of 2-morphisms
f1
0

c1

0

# 1

# 1; 2c3 7 ! c1;

f1; f2
0

!

f1

0

!
!

c3

!

! c2 7 ! c1 # 1  2 c2
# 2
!
f
2
!


f2
Example 2.1.3 The paradigmatic example of 2-category is Cat itself (see [Mac71]): the objects are categories
 the 1-morphisms are functors and ; is functor composition,
 the 2-morphisms are natural transformations and ; and  are respectively
horizontal and vertical composition of natural transformations.
8De nition 2.1.4 A 2-functor F from C1 to C2 is a mapping
f

c

!

#
f

Ff

!

0

# F

F

c in C1

7 ! Fc0Ffwhich commutes with identities, ; and  .

0!

Fc in C20!

De nition 2.1.5 If F1 and F2 are 2-functors from C1c to C2, then a 2-naturaltransformation  from F1 to F2 is a family hF1c ! F2cjc 2 Obj(C1)i of 1morphisms in C2 s.t.

cj j
jj ! jj# #cc

! j F2c j
jj F! jj
c
# #
! F2c

F1c

j j
jj F! jj
# #

=)

1

2

F1c

0

0

0

0

i.e. the functors c ; F2 and F1 ; c from C1 (c; c ) to C2(F1c; F2c ) are equal for everyc and c in Obj(C1).
0

0

0

0

Remark 2.1.6 There are a lot of other concepts related to 2-categories that haveno counterpart for categories: modi cations, pseudo-functors, lax-functors, : : : (see[KS74]). Unfortunately the notation and terminology is far from standard.
The incorrect formulation of the paradigm of Categorical Logic was the motivating example for introducing 2-categories, so that it can be reformulated (moreabstractly) as: theory as object (of a 2-category) model as 1-morphism
 homomorphism as 2-morphism
An useful observation is that, in a 2-category we can reformulate abstractly a substantial part of category theory, so that even in such an abstract reformulation we
can still rely on category-theoretic concepts. Adjunctions, comma categories, monads, split brations are all examples of 2-categorical concepts, i.e. they make sense
in any 2-category. However, other concepts cannot be captured 2-categorically:
opposite categories, adjunctions with parameters (used to de ne exponentials),
dinatural transformations. We consider other two examples where 2-categories
are particularly appropriate.
9Term rewriting. We have seen that an algebraic language can be viewed as acategory, with terms as morphisms and substitution as composition. To consider
term rewriting in this framework, one can view a rewriting rule as a morphismfrom the redex to the contractum, e.g.

add0: (0 + n) =) n: N ! N
add1: s(m) + n =) s(m + n): N  N ! N
Exercise 2.1.6.1 Describe the rewriting of s(0 + n) to s(n) as a 2-morphism.
Intuitively vertical composition corresponds to apply a rewriting to the contractumof another rewriting. Horizontal composition amounts to take a term M in acontext C [ ], perform two independent rewritings, one of M and the other of C [ ],then take as contractum of C [M ] the contractum of C [ ] with the hole replacedby the contractum of M .

Programming languages with type-constructors and polymorphic functions. [HJ] proposes a reinterpretation of the paradigm of Categorical Logic interms of data-re nement , more generally in terms of an implementation relation
between two semantics for the same programming language: programming language as category denotational semantics as functor
 re nement as natural transformation
The paper divides a programming language in an inner part, with only basic
types and operations whose interpretation has to be supplied by the user, and anoutter part, which specify type constructors (as endofunctors) and polymorphic
operations (as natural transformations between endofunctors) with a xed interpretation in every denotational semantics. However, it seems natural to let theuser specify also the implementation of type constructors (e.g. List) and polymorphic functions (e.g. reverse). The paradigm proposed by Hoare should bereformulated as follows: programming language as 2-category (with nite products)1
 denotational semantics as 2-functor (preserving nite products)
 re nement as lax-natural transformation
1

This allows type constructors with any arity.

10

Intuitively, in the programming language L as a 2-category 1-morphisms are names
for type constructors (with a given arity) and 2-morphisms are names for polymorphic functions. If L has only one object (for simplicity), then a denotation semantics from L to Cat should map the only object of L to a category C , 1-morphisms
to endofunctors on C , 2-morphisms to natural transformation, by respecting thearities.
Finally, to justify the choice of lax-natural transformations, we have to ask how
does the simple view of a language as a category t in the more general one, of alanguage as a 2-category, and then check whether the general notion of re nement
specialises to natural transformations.
Given a category Path(G) freely generated from a graph G, we can identify itwith the 2-category with nite products Free(G) freely generated from an object
L, 1-morphisms a: 1 ! L for each node of G and 2-morphisms f : a =) b for eachedge from a to b in G.
Exercise 2.1.6.2 For any graph G, prove that 2-functors F : Free(G) ! Cat preserving nite products are in one-one correspondence with functors from Path(G)to some category C (take C to be F (L)).
Given two 2-functors F1; F2: Free(G) ! Cat, corresponding to functors F1: Path(G) !
C1 and F2: Path(G) ! C2, prove that lax-natural transformations from F1 to F2
are in one-one correspondence with pairs hU;  i, where U : C1 ! C2 is a functor and : F1; U !: F2 is a natural transformation.
Prove that 2-categories, 2-functors and lax-natural transformations are a 2category, so the abstract paradigm for programming languages works also in this
case.
0

0

11

Chapter 3
Notions of computation as monads
We present a category-theoretic semantics of computations . An application of thissemantics is the computational -calculus , a modi cation of the typed -calculus(in particular of -conversion), which is correct for proving equivalence of programs and independent from any speci c notion of computation (see [Mog89b]).
A promising area of application for this semantics is the Denotational Semantics
of programming languages, since it suggests new ways to structure such semantics.
We review some criticisms that can be moved to the -calculus and the ways
it has been used for proving equivalence of programs: -conversion is not correct w.r.t. operational semantics
 the type constructors of LCF , an extension of the -calculus based on denotational semantics, are not the most natural one form the point of viewof programming languages (call-by-value or call-by-name). In particular,
there are problems in establishing a clear relation between denotational andoperational semantics.
 modi cations of the -calculus based on operational considerations are correct, but they lack a completeness result.

3.1 Calculi and programming languages
The direct connections between the pure -calculus (i.e. the subject of [Bar81])
and functional programming languages sometimes do not go beyond the binding
mechanism of -abstraction (see [McC62, Lan64]). This is not surprising if welook at the history of the type free lambda calculus (Preface of [Bar81]): \Around1930 the type free lambda calculus was introduced as a foundation for logic andmathematics. Due to the appearance of paradoxes, this aim was not ful lled,
however. Nevertheless a consistent part of the theory turned out to be quite
successful as a theory of computations. It gave an important momentum to earlyrecursion theory and more recently to computer science. : : : As a result of these12developments. the lambda calculus has grown into a theory worth studying
for its own sake. People interested in applications may also nd the pure calculus useful, since these applications are usually heuristic rather thandirect. : : : "Types arise in various applications, for instance they are a common featureof many programming languages, in logic they can be identi ed with formulae,in (cartesian closed) categories they correspond to objects. As shown in [Sco80],\nothing is lost in considering type free theories just as special parts of typed
theories". For this reason, we give more emphasis to the typed -calculus (andmore generally typed languages), as it provides a more exible and structured
basis for applications than the pure -calculus.

Call-by-value, call-by-name and the -calculus

In [Plo75] call-by-value and call-by-name are studied in the setting of the lambda
calculus: this study exempli es very clearly the mismatch between the pure calculus and (some) programming languages.
From an operational point of view, a programming language is completely
speci ed by giving the set Prog of programs and the evaluation mechanism
Eval: Prog * Prog, i.e. a partial function mapping every program to its resulting
value (if any).
In the setting of the lambda calculus, programs are identi ed with the(closed) -terms (possibly with extra constants, corresponding to somefeatures of the programming language). The evaluation mechanism induces a congruence relation  on -terms, called operational equivalence, and a calculus is said to be correct w.r.t.  when M = N(derivable in the calculus) implies M  N .
Plotkin's intention is to study programming languages, therefore he accepts theevaluation mechanism and looks for the corresponding calculus .
The -calculus is not correct w.r.t. call-by-value operational equivalence, therefore it cannot be used to prove equivalence of programs. Starting from this observation, Plotkin introduces the v -calculus and shows that it is correct w.r.t.
call-by-value operational equivalence. However, to prove the Church-Rosser andStandardisation theorems Plotkin proceeds by analogy and re-uses some techniques already applied to the -calculus. In the case of call-by-name the situation
is much simpler, since only the  axiom is not correct w.r.t. call-by-name operational equivalence.
The idea of starting from operational considerations, and then develop a calculus has been followed by several people to take account of mor complex featuresof programming languages like non-determinism, side-e ects, control-mechanisms(see [Sha84, FFKD86, MT89]).
13

The partial -calculus

The p-calculus is a formal system presented in [Mog86] and (with minor di erences) in Chapter 4 of [Ros86], which is sound and complete w.r.t. interpretationin partial cartesian closed categories .
While the v-calculus is discovered by operational considerations, and his only
criterion for judging a calculus is its correctness w.r.t. the operational semantics(but in general there are plenty of correct calculi), the p-calculus is discoveredby model-theoretic considerations, namely as the unique calculus which is soundand complete w.r.t. a certain class of models.
The terms of the p-calculus are typed -terms, and the formal system is for deriving one-sided sequents x1: 1; : : :; xm: m:A1; : : :; An =) A0, where x1: 1; : : :; xm: mis a type environment and the Ai are either existence statements (E(t)) or equivalences (t1  t2). The (type free) p -calculus proves more equivalences than the
v -calculus (e.g. (x:x)(yz)  yz), nevertheless it is still correct w.r.t. call-by-value
operational equivalence.
In [Mog88] various modi cations of the p-calculus are considered that aresound and complete w.r.t. other classes of models, e.g. classical type structures of(monotonic) partial functionals.

Logics for computable functions and domain theory

The use of logics for proving correctness of programs was pioneered in [Flo67,
Hoa69]. The programming languages considered in these early approaches arevery simple (while programs) and the formal languages of expressing properties ofprograms are a mixture of programming language and predicate calculus (Hoare's
triples). The main feature of these logics, e.g. Hoare's logic, is that they areprogramming language dependent and support a structured methodology
for proving correctness, i.e. properties are proved by induction on the structure of
programs.
We are interested in a di erent kind of approach, based on logics for reasoning
about mathematical structures that provide models for (functional) programming
languages. Such a logic is programming language independent, but potentially it can be used to prove properties of programs (like equivalence or correctness). To exploit this potentiality the logic has to be exible, so that one candescribe how a particular programming language is interpreted in a certain mathematical structure. More precisely, its language should be extendible (to include
the features of a programming language), it should be possible to add (non-logical)
axioms (to axiomatise the properties of these features) and the logic itself should
be uncommitted (so that any programming language can be axiomatised ).
The need for a mathematical semantics of programming languages led to the
Scott-Strachey approach to denotational semantics and the development of domain theory (see [Sco70, SS71, Sco76, Plo81]). Denotational semantics takes an
14

abstract view of computations , based on continuous functions between certain
spaces of partial elements (cpos), rather than partial recursive functions (on thenatural numbers).
A rst attempt at a logic for reasoning about cpos and continuous functions was
the logic for computable functions (see [Sco69]), which was subsequently extended to the polymorphic predicate -calculus PP (see [GMW79, Pau85]).
The idea is rst to consider an extension of the typed -calculus suitable for the(cartesian closed) category of cpos and continuous functions (the intended model ),by adding constants for xed-point operators and least elements , and then to axiomatise some properties of the intended model, like xed point induction, in a(classical) rst order logic, whose formulae are built up from inequations between
-terms (M  N ).
In PP programs are identi ed by -terms and properties (of a programs)
are ordinary rst order formulae. As pointed out at Page 9 of [Sco69], PP
(as well as the logic of partial elements) is a theory of partial functions based
on total functions: \: : : classical type theory supposes total (everywhere de ned)functions, while algorithms in general produce partial functions. We do not wish
to reject a program if the function de ned is partial { because as everyone knows
it is not possible to predict which programs will loop and which will de ne total
functions. The solution to this problem of total vs. partial functions is to makea mathematical model for the theory of partial functions using ordinary total
functions." More precisely, divergence is represented by the least element (?)
of a cpo and a partial (recursive) function f : N * N becomes a strict function
f :N ! N .
There are various criticisms that can be made to PP (and domain theory),
more or less related to the way partial functions are represented:
 while programs (and similar programming languages) have a simple settheoretic semantics as partial functions from stores to stores, but their denotational semantics (based on cpos and continuous functions) is comparatively
clumsy .
 the way of expressing termination (existence ) of a program (partial element)t is indirect \t 6= ?" and intuitionistically incorrect, according to [Sco79].
 the (choice and) interpretation of type constructors is based on the typed calculus (i.e. a theory of total functions), rather than considerations about(real) programming languages. For instance, in a lazy programming language the values of type 1  2 are pairs of unevaluated expressions and[ 1  2] should be the lifted product ([[1]  [ 2] ) , while in a eager programming language the values of type 1  2 are pairs of values and [ 1  2]should be the smash product [ 1] [ 2] .
These considerations on domain theory and PP (among others) led Gordon
Plotkin to take a di erent approach to denotational semantics, based on con?

?

?

?

15

tinuous partial functions, and to reformulate PP using intuitionistic logic

of partial elements on top of a suitable term language, called metalanguage (see[Plo85]).
The metalanguage is a typed functional language with a rich collection oftypes (products, coproducts, partial function spaces and recursive types), it has
an operational semantics, based on eager evaluation, and a denotational semantics, according to which types denote cpos (possibly without a least element)
and terms denote continuous partial functions. The two semantics are related bya correspondence theorem between (operational) termination and (denotational)
existence, inspired by a similar result due to Martin-Lof (see [ML83] and Chapter
6 of [Abr87]).
The choice of eager evaluation makes it easier to translate programming languages into the metalanguage correctly , i.e. so that the operational and denotational semantics obtained via the translation are the intended ones. In fact, it
is straightforward to translate lazy programming languages into typed eager programming languages, while the reverse translation is in general impossible (or atleast very clumsy).
Since many programming languages can be correctly translated into the metalanguage, it is not necessary to extend the metalanguage for accommodating them,and a logic for reasoning about them can be derived from that for the metalanguage, while in PP it has to be axiomatised , by creating a new theory. For thesame reason, the correspondence theorem between operational and denotationalsemantics, unlike similar results for the -calculus (e.g. [Wad76]), has direct application to programming languages.

3.2 Notions of computation as monads
It is important to clarify what is the intuitive meaning assigned to \notions ofcomputation", since the word computation is rather overloaded. We consider acomputation as the denotation of a program, while a more ne grained (operational approach) considers a computation as a possible execution sequence
for a program. In the latter case the attribute \possible" is necessary to accountfor non-deterministic or probabilistic programs.
We give a categorical semantics of computations, but also this claim requires
some explanation, since a categorical semantics can be given at di erent levels of
abstractions:
1. execution sequences can be viewed as (enriched) categories, where objects
are events and morphisms are relations between them, (like causality or adelay, (see V. Pratt).
2. programs can be viewed as categories (with an initial state), where objects
are states (or histories) and morphisms are transitions (or pieces of execution16

sequences). This approach corresponds to transition systems.
3. programs or execution sequences can be viewed as objects of a category,
whose morphisms can be, for instance, mappings from the events of an execution sequence s1 to events in another execution sequence s2 satisfying
certain properties. This approach has been applied to de ne categorically,e.g. as products or coproducts, some operations on programs or execution
sequences (see V. Pratt, J. Meseguer, : : : ).
4. nally programs can be viewed as morphisms of a category, whose objects
are types. This is the view taken by Denotational Semantics.
We take the denotational view, and consider programs as morphisms in a category.
To be precise a complete program should be identi ed with an element, i.e. amorphism with domain the terminal object, while a program in an environment
corresponds to a morphism.
By \notion of computation" we mean a qualitative description of the denotations of programs in a certain programming language, rather than the interpretation function itself. Examples of notions of computations are:
1. computations with side e ects, where a program denotes a map from a store
to a pair, value and modi ed store.
2. computations with exceptions, where a program denotes either a value or an
exception.
3. partial computations, where a program denotes either a value or diverges.
4. nondeterministic computations, where a program denotes a set of possible
values.

3.2.1 A justi cation for monads

In order to justify the use of monads for modelling notions of computations weadopt the following intuitive understanding of programs: a program is a function from values to computations.
1. First we take a category C as a model for functions and develop on top
a general understanding of values and computations. More precisely we
introduce a unary operation T on the objects of C , which map an object A,
viewed as the set of values of type  , to an object TA corresponding to theset of computations of type  .
2. Then a program from A to B , i.e. which takes as input a value of type A
and after performing a certain computation will return a value of type B ,can be identi ed with a morphism from A to TB in C .
17

3. Finally, we identify a minimum set of requirements on values and computations so that programs are the morphisms of a suitable category.
These three steps lead to Kleisli triples for modelling notions of computation andKleisli categories for modelling categories of programs.
De nition 3.2.1 A Kleisli triple over C is a triple (T; ; ), where T : Obj(C ) !
Obj(C ), A: A ! TA, f : TA ! TB for f : A ! TB and the following equations
hold: A = idTA A ; f = f
 f ; g = (f ; g )
















Remark 3.2.2 Intuitively A is the inclusion of values into computations andf is the extension of a function f from values to computations to a function
from computations to computations, which rst evaluates a computation and thenapplies f to the resulting value. Although it seems natural to require that A is amono, we will not do so, since it causes several technical problems.
The axioms for Kleisli triples amounts exactly to say that programs form acategory, the Kleisli category CT , where the set CT (A; B ) of morphisms from A
to B is C (A; TB ), the identity over A is A and composition of f followed by g
is f ; g . Intuitively f ; g takes a value a and applies f to produce a computation
fa, then it executes/evaluates the computation fa to get a value b, and nally itapplies g to b to produce a computation.


Exercise 3.2.2.1 De ne suitable Kleisli triples (over the category of sets) tomodel the following notions of computations: total computations: TA = A
 partial computations: TA = A
 non-deterministic computations: TA = P (A) computations with side-e ects: TA = (A  S )S , where S is a set of states/stores computations with exceptions: TA = A + E , where E is a set of exceptions
 computations with continuations: TA = RRA , where R is a set of possible?

results18

 computations for communicating processes:
TA = P:A + 1 + (Act  P ) + (P  P )where Act is a set of actions (with an involution operation  and a silent action  , to model communication). Intuitively an element of P , called process,can be either a value (in CCS there are no values), or Nil (which represent
deadlock), or an action followed by a process, or a non-deterministic choice
between two processes
 computations with complexity: TA = (A  N ), i.e. a program is interpretedby the a pair giving the nal result and the time required to compute it
What kind of Kleisli triples would you use to model partial computations withside-e ects or computations with side-e ects and exceptions? Try also other combinations.
For adjunctions we saw that there are several equivalent de nitions, but only
one of them is phrased in such that can be easily generalised to arbitrary 2categories. For this reason we introduce monads (called also triples), which areequivalent to Kleisli triples but are de ned only in terms of functors and naturaltransformations.
De nition 3.2.3 A monad over C is a triple (T; ; ) s.t.

jCj
jCj
T ; T jj ! jj T
id jj ! jj T
# #
# #
C
C
(T ; )   = (; T )   and (T ; )   = idT = (; T )  .
C

Proposition 3.2.4 There is a one-one correspondence between Kleisli triples andmonads.
Proof Given a Kleisli triple (T; ; ), the corresponding monad is (T; ; ), where
T is the extension of the function T to an endofunctor by taking T (f : A ! B ) =(f ; B ) and A = idTA.
Conversely, given a monad (T; ; ), the corresponding Kleisli triple is (T; ; ),where T is the restriction of the functor T to objects and (f : A ! TB ) = Tf ; B .










A general theorem about monads says that they are all induced by adjunctions,
namely a monad over C is always of the form (F ; G; ; F ; ; G), where (F; G; ; )is an adjunction from C to some other category D. Actually there are two general
constructions, that given a monad over C return an adjunction inducing thatmonad. We will use only the construction due to Kleisli; however, the EilenbergMoore construction as well as additional information on monads can be found in
most textbooks on Category Theory (see [Mac71, BW85]).
19

Proposition 3.2.5 Given a monad (T; ; ) over C , or equivalently a Kleisli

triple, the quadruple (FT ; GT ; ; ), de ned below, is an adjunction from C to the
Kleisli category CT which induces the monad (T; ; ): FT : C ! CT is the functor mapping A to A and f : A ! B to f ; B GT : CT ! C is the functor mapping A to TA and f 2 CT (A; B ), i.e. f : A !
TB in C , to f : IdC !: FT ; GT is  of the Kleisli triple, since T = FT ; GT
 : GT ; FT !: Id T is the natural transformation s.t. A = idTA 2 CT (TA; A)

C

3.2.2 A simple metalanguage

One may consider formal systems (for reasoning about computations) motivatedby two di erent objectives: reasoning about programming languages and reasoning
about programs (in a xed programming language).
When reasoning about programming languages one has di erent monads overthe same category C (for simplicity), one for each programming language, andthe main aim is to study how they relate to each other. So it is natural to basea formal system on a metalanguage for C , where monads are treated as unary
type-constructors.
When reasoning about programs one has only one monad T , because the programming language is xed, and the main aim is to prove properties of programs.
In this case the obvious choice for the term language (of a formal system) is the
programming language itself, i.e. a language for CT . However, the expressivenessof the programming language is adequate, only if the monad T satis es the mono
requirement, because then it is possible to express equality of values in terms ofequality of computations and an unary predicate over computations (similar to
the existence predicate in the logic of partial elements), whose extension is the setof values.
In this section we take the rst approach, while [Mog89b] takes the second
one. We introduce a metalanguage, whose terms denote morphisms in a category
C . The aim of this section is to focus only on the crucial ideas of the interpretation,and the language has been oversimpli ed (for instance terms have exactly one freevariable and the only assertions are equations) in order to de ne its interpretationin any category with a monad (T; ; ).
The metalanguage is parametric in a signature (i.e. a set of base types andunary function symbols), therefore its interpretation in a category with a monadis parametric in an interpretation of the symbols in the signature.
 Given an interpretation [ A] for any base type A, i.e. an object of C , thenthe interpretation of a type  : : = A j T is an object [  ] of C de ned in
the obvious way, namely [ T ] = T [  ] .
20

 Given an interpretation [ f]] for any unary function f of arity 1 ! 2, i.e.
a morphism from [ 1] to [ 2] in C , then the interpretation of a well-formed
term x:  ` e:  is a morphism [ x:  ` e:  ] from [  ] to [  ] in C de ned byinduction on the derivation of x:  ` e:  (see Table 3.1).
 On top of the term language we consider equations, whose interpretation is
0

0

0

0

as usual (see Table 3.2).

Remark 3.2.6 The let-constructor is very important semantically, since it corre-

sponds to composition in the Kleisli category CT . Moreover, (letT x=e in e ) cannot
be reduced to the more basic substitution (i.e. e [x: = e]), which corresponds tocomposition in C , without collapsing CT to C .
In the -calculus the let-constructor is usually treated as syntactic sugar for(x:e )e, and this can be done also in the c-calculus, but it relies on function
spaces, that are not more primitive than a notion of computation.
000

3.2.3 Extending the metalanguage

The metalanguage introduced in the previous section is far too simple to do anything useful. We discuss the additional structure require on the category C inorder to interpret also algebraic terms. Other extensions of the metalanguage do
not present problems, e.g. it is straightforward to incorporate functional types,
sums and products. The next critical extension is the introduction of dependent
types (that we will not discuss).
The standard requirement on a category C for interpreting algebraic terms isthat it must have nite products, so that the interpretation of a function symbol ofarity  !  is a morphism from [ ( )]] (i.e. [ 1] : : :[ n] ) to [  ] and similarly theinterpretation of a well-formed term x1: 1; : : :; xn: n ` e:  is a morphism from[ ( )]] to [  ] . However, products are not enough, to interpret (letT x=e in e ),when e has other free variables beside x (see [Mog89b]). The additional structure
we need is given by a natural transformation which relates products and monad.
De nition 3.2.7 A strong monad over a category C with nite products is
a monad (T; ; ) together with a natural transformation tA;B from A  TB to
T (A  B ) s.t.
t1;A1  TA! T (1  A)
0

0

@
rTA@@

&

21

j
jj TrA#TARULE SYNTAX
var
x:  ` x: let

f: 1 ! 2
[ ]T

SEMANTICS= id[  ]x:  ` e1: T1= g1
x1: 1 ` e2: T2= g2
x:  ` (letT x1=e1 in e2): T2 = g1; g2
x:  ` e1: 1
x:  ` f(e1): 2
x:  ` e: 
x:  ` [e]T : T= g1
= g1; [ f]]= g= g ; [  ]

0

0

0

Table 3.1: Terms and their interpretation

RULE SYNTAXSEMANTICSeq
x: 1 ` e1: 2= g1
x: 1 ` e2: 2= g2
x: 1 ` e1 = e2: 2 () g1 = g2
Table 3.2: equations and their interpretation

22

tA B;C(A  B )  TC

j
A;B;TC jj#
A  (B  TC )



idA  tB;C

! A  T (B  C )and which satis es also the following diagrams:
idA B

AB



j

idA  B jj#
A  TB"
idA  B jj
j
A  T 2B
where r and

tA;B
tA;TB

! T ((A  B )  C )j
jj T A;B;C#
tA;B C! T (A  (B  C ))


! AB
j
jj A B#! T (A  B )"jj A Bj
T tA;B
2! T (A  B )! T (A  TB )are the natural isomorphisms

 rA: 1  A ! A
 A;B;C : (A  B )  C ! A  (B  C )The tensorial strength t induces a natural transformation A;B from TA  TB to
T (A  B ), namely
A;B = cTA;TB ; tTB;A; (cTB;A; tA;B )where c is the natural isomorphism cA;B : A  B ! B  A
The morphism A;B has the correct domain and codomain to interpret the pairingof a computation of type A with one of type B (obtained by rst evaluating
the rst argument and then the second). There is also a dual notion of pairing,~A;B = cA;B ; B;A; TcB;A (see [Koc72]), which amounts to rst evaluating thesecond argument and then the rst. With this additional structure available we
can interpret algebraic terms, in particular the let-constructor (see Table 3.3).
At this point it is easy to give a sound and complete formal system for proving
equality of algebraic terms interpreted in a strong monad. The inference rules forsuch a formal system can be partitioned in two (see Table 3.4):
 general rules of equational logic
 the inference rules for let-constructor and types of computations


23

RULE SYNTAXSEMANTICS
let` e1: T1
= g1
; x1: 1 ` e2: T2= g2` (letT x1=e1 in e2): T2 = hid[ ] ; g1i; t[ ] ;[ 1] ; g2

Table 3.3: Interpretation of let

We write [x: = e] for the substitution of x with e in and (letT x=e in e) for(letT x1=e1 in (: : : (letT xn=en in e) : : :)), where n is the lenght of the sequence x(and e). In particular, (letT ;=; in e) stands for e.
` e: 
; x:  ` Asubst
` A[x: = e]
= is an congruence relationass ` (letT x2=(letT x1=e1 in e2) in e) = (letT x1=e1 in (letT x2=e2 in e)): T
provided x1 is not free in e

` (letT x1=[x2]T in e) = e[x1: = x2]: T
T. ` (letT x=e in [x]T ) = e: T

let.

Table 3.4: Inference rules

24Chapter 4
Denotational Semantics andmonadsWe have identi ed a precise abstract concept corresponding to a notion of computation, now we want to consider possible applications to the Denotational Semantics of programming languages. In the introduction we pointed out that a major
shortcoming of Denotational Semantics is the lack of modularity, which prevent
gluing together semantics for toy languages into a semantics for a complex language. Having an abstract notion of computation, rather than a bunch of examples
for it, will provide the key step towards modularity, namely parametrisation w.r.t.
a notion of computation.
To give semantics to a complex language L we propose a stepwise approach,which starts from a monad (notion of computation) corresponding to a toy sublanguage of L and then at each step applies a monad constructor which add one
feature to the language. To make this approach precise we introduce a category
Mon(C ), whose objects are monads (over a given category C ), and identify monadconstructors with endofunctors over Mon(C ).
De nition 4.0.8 Given two monads (T; T ; T ) over C and (S; S ; S ) over D,
a monad-morphism from the rst: to the second monad is a pair (U; ), where
U : C ! D is a functor and : T ; U ! U ; S is a natural transformation s.t. :
UAT
UTA
UA
! U (TA)U (T 2A)

j
A jj
& #

j
jj TA
#

@@
@

S
UA

S (UA)-@SUA @@

25

S (U (TA))

jjj SA#S 2(UA)

Remark 4.0.9 We said that a programming language with (unary) type construc-tors and polymorphic operations can be viewed as a freely generated 2-category,
and that lax natural transformations are the appropriate morphisms between models of such a language. If we take the free 2-category L(Mon) with one monad,then there is a one-one correspondence between monads in Cat and 2-functors
from L(Mon) to Cat, this extend to a one-one correspondence between monadmorphisms and lax natural transformations between the corresponding 2-functors
from L(Mon) to Cat.
This correspondence is very useful as guideline for nding the correct notionof morphism for monads with additional structure. For instance, when T is themonad for non-determinism, one can de ne a natural transformation orA : TA 
TA ! TA, corresponding to non-deterministic choice. Then one can de ne thelanguage for non-determinism as the free 2-category with one monad and a 2morphism or satisfying certain equations.
As pointed out before, this 2-categorical view of programming languages canmodel only types and operations that are covariant and natural , so functional
types and evaluation are outside its scope. Furthermore, it is arguable whether
the component of the natural transformation  should be morphisms in D or something di erent, e.g. relations in D. What follows should be treated as a general
methodology for having modularity in Denotational Semantics, with the warningthat some technical details have been simpli ed, in particular the de nition ofmonad morphism may not be a satisfactory formalisation of what is a relation
between notions of computation (programming language semantics).
Monad morphisms not only give a functor U from C to D, they also induce afunctor U from CT to DS , which extends U from functions to programs.
Proposition 4.0.10 Thereis a one-one correspondence between monad morphisms (U;  ) from (T; T ; T ) over C to (S; S ; S ) over D and pairs of functors(U; U ) s.t. the following diagram commutes
U




C
j
FT jj
#
CT

!D
j
jj FS
#
! DS

U



where FT and FS are the left adjoints given by the Kleisli construction.

Proof We sketch only the correspondence:
 given a monad morphism (U; ), we de ne U : CT ! DS as the functor
mapping A to UA and f 2 CT (A; B ), i.e. f : A ! TB in C , to (Uf ); B . We26

claim that the pair (U; U ) satis es the diagram, in factU
f: A ! B
!
Uf


j
FT jj
#

j
jj FS
#

f ; BTS! U (f ; BT ); B = (Uf ); UBUS for monadwhere the equation follows from the axiom U (BT ); B = UBmorphisms.
 given a pair (U; U ) satis es the diagram, we de ne : T ; U !: U ; S as thenatural transformation s.t. A = U (idTA), which is a morphism from U (TA)to S (UA) in D.
The de nition of monad morphism given above is very general. Since we areinterested only in relating monads or strong monads over some xed category C ,we simplify the de nition by requiring U to be the identity functor on C (as donein [BW85]).
De nition 4.0.11 Given two strong monads (T; T ; T ; tT ) and (S; S ; S ; tS )over the same category C , a simpli ed strong monad morphism from the
rst to the second monad is a natural transformation : T !: S s.t. :
tTA;B
AT
TA
2
A
! TA
TA
A  TB! T (A  B )j
idA jj
#

A

j
A jj
#
! SA
S

A

j
jj (; )A
#

SA

j
idA  B jj#
A  SBS 2A

jjj A B#
! S (A  B )


tSA;B

4.1 Some examples of monad constructions

In this section we x a category C with enough datatypes, e.g. the category ofsets or cpos, and consider the category Mon(C ) of (strong) monads over C andsimpli ed (strong) monad morphisms. We will de ne several endofunctions F on
Obj(Mon(C )), by abstracting from domain-theoretic constructions for giving semantics to programming languages (see [Sch86, Mos89]) and address the following
questions: can F be extended to an endofunctor F over Mon(C )?
27 is there a natural transformation from IdMon( ) to F ? Which intuitively

means that every T -computation can be viewed as an F (T )-computation via
a monad morphism from T to F (T ). A monad constructor F is expected tohave such property, when its action on T is to add some features.
 If associated to T there are some additional operations, i.e. natural transformations, is there a way of lifting them to F (T )?
C

Remark 4.1.1 The rst two questions come together, since if we were not inter-

ested in establishing relations between monads, but only in constructing them,
then endofunctions would be completely satisfactory. On the other hand, to establish relations among monads it is important to have canonical ways of liftinga relation between T and S to a relation between F (S ) and F (T ).
The last question is of paramount importance for a modular approach to Denotational Semantics. For instance, if we have the monad T of exceptions withadditional operations for raising and handling exceptions, then when we add sidee ects (by applying a monad constructor F ), we would like to derive in a canonicalway the operations for raising and handling exceptions in F (T ) from those de ned
over T , as well as introducing in a canonical way the operations for manipulating
stores. There is a related question that we have not been able to address properly,
yet. If an operation op in F (T ) is derived canonically from an operation op in T ,what axioms can be inferred for op given a set of axioms satis ed by op?
00

We introduce some general terminology for operations associated to a monad,that will be used to discuss operations associated to the monad constructor for
exceptions as well as lifting of operations from T -computations to T -computations
with additional features.
Notation 4.1.2 We x a countable set of type variables .
 The metavariable  range over the following sets of type expressions: 2 Type: : = 1 j A j j T ( ) j  A j 1  2
where the symbols A are objects of C , is a variable in and T is an
uninterpreted type constructor.
 Given an interpretation for T , i.e. anS endofunctor S over C , the type expression  will denote a functor [  ] from C to C . Moreover, a naturaltransformation  from S to S induces a natural transformation  from[  ] S to [  ] S .
 An operation op ofS arity 1S !: 2 on the endofunctor S is a natural transformation from [ 1] to [ 2] .
0

0

28

 Given: an operation op of arity 1 !: 2 on S and a: natural transformation
: S ! S , we say that an operation op of arity 1 ! 2 on S is a lifting of000

op along  i the following diagram commutes:
op[ 1] S! [ 2] S

j
 jj
#
1

[ 1] S

op

0

j
jj 
#

2

0

! [ 2] S

0 Given an: endofunctor F on Mon(C ) and for every S an operation opS ofarity 1 ! 2 on F (S ), we say that the operation constructor op is naturali for every monad morphisms : S ! S the following diagram commutes:
0[  ] F (S)1j(F) jj#
1

opS

! [ 2] F (S)jjj (F)
#opS! [ 2] F (S )20

[ 1] F (S )00

 Given an endofunctor F on Mon(C ) and a natural transformation F : IdMon( ) !:of arity 1 !: 2 along
F , we say that F is a natural lifting of operations:
F i for every monad S and operation op: 1 ! 2 on S opF is a lifting ofFC

op along S andop[ 1] S! [ 2] S

j
 jj
#
1

[ 1] Sop00

[  ] F (S)

j
jj 
#

1

2

! [ 2] S

0jimplies (F) jj
#
1

opF

! [ 2] F (S)jjj (F)
#op F! [ 2] F (S )2[ 1] F (S )000

We give a very general theorem on the existence of natural liftings for operations of very simple arities.
Proposition 4.1.3 Let  0 be a metavariable ranging over the set of type expressions without T , i.e.

 0 2 Type0: : = 1 j A j j  0A j  01   02if F is an endofunctor on Mon(C ) and F : IdMon( ) !: F is a natural transformation, then there is a natural lifting of operations of arity  0 !:  along  F .
C

29

Proof Given an operation op:  0 !:  on S , we de ne its lifting opF along SF as
the natural transformation opF = op; SF  . This is a lifting of op along SF because
SF  0 is the identity (as T does not occur in  0). Moreover, it is natural because
for every monad morphisms : S ! S the following diagram commutes:
SF 
S
[]
! [  ] F (S)
0

j
 jj
#

[]S

SF 
0

0

j
jj (F)
#! [  ] F (S )0

The above result is rather unsatisfactory, because we want to consider operations
that takes computations as parameters (like handle below). However, it seems
that better results can be achieved only by relying on some special property of themonad constructor under investigation.

4.1.1 Exceptions

The monad constructor for exceptions (compare with 9.2 of [Sch86]) is particularly simple and enjoys nice mathematical properties. It is also a strong monadconstructor provided coproducts distribute over products, which is always the casein a cartesian closed category.
De nition 4.1.4 Given a monad T = (T; T ; T ) the monad Texcp of T -computations
with exceptions is de ned as follows: Texcp( ) = T ( + E ) ATexcp (a) = [inl(a)]T , i.e. ATexcp = inl; AT +E
 TAexcp (c) = (letT x=c in (case x of c: T (A + E ) ) c j e: E ) [inr(e)]T )), i.e.

TAexcp = ([idT (A+E); inr; AT +E ])A monad morphism  : S ! T induces a monad morphism excp: Sexcp ! Texcp,
namely excp A = A+E
For every monad T there are two monad morphisms Texcp: T ! Texcp andexcp : Texcpexcp ! Texcp which make the monad constructor for exceptions into amonad over Mon(C ) Texcp has A-component T (inl): TA ! T (A + E ) excp
T has A-component T ([id; inr]): T ((A + E ) + E ) ! T (A + E )30For every monad T there
are two operations on Texcp, raise: E !: T ( ) and:handle: E  T ( )  T ( ) ! T ( ), that are natural in T : raise(e) raises the exception e.
 handle(e; c1; c2) evaluates c2 and if this evaluation raises e, then it evaluates
c2. This operation can be de ned only if E has a decidable equality, i.e. amorphism eq: E  E ! 1 + 1 s.t. eq(e1; e2) = inl() i e1 = e2.
Finally we give sucient conditions on arities for the existence of natural liftings of operations of those arities along excp.
Proposition 4.1.5 If 1 is an out-type and 2 is anin-type (see Table 4.1), thenthere is a natural lifting of operations of arity 1 !: 2 along  excp.

Proof Let : ! Type be a substitution mapping a type variable either toitself or to : + E , this induces (in the obvious way) an endofunctor[ ] on C .
:Let in: Id ! [ ] be the natural transformation s.t. inf : f ! [ ] (f ) is either
inl: f ! f + E (when ( ) = + E ) or the identity of f (when ( ) = ).
If  is an out-type, then there is a natural transformation out s.t. the following
diagram commutes(SF )
S[]! [  ] Sexcp@
in; [  ] S@@&jjj out#[  []]]S
Conversely, If  is an in-type, then there is a natural transformationin in the:
opposite direction.
Therefore, given an operation op: 1 ! 2 on S , we can de ne
opexcp : 1 !: 2 on Sexcp to be out1  ([[] ; op)  in2 .

Remark 4.1.6 The monad constructor for exceptions is very well-behaved in com-

parison to those for side-e ects and continuations. We have chosen to introduce
it rst and highlight its properties in order to set an ideal standard.

4.1.2 Side-e ects

We present a very general monad for side-e ects, which will be instanciated tomonads that are more appropriate for giving semantics to programming languages.
This construction depends on a set S . For simplicity we work in the category ofsets.
De nition 4.1.7 Given a monad T = (T; T ; T ) the monad Tseff of T -computations
with side-e ects is de ned as follows:
31

PROPERTIES
case  of E ! ~
~ !  E
 E ! ~in typeout type
1
yes
yes
yes
yes
A
no
yes
yes
yes
( ) =
no
yes
yes
yes
( ) = + E
yes
yes
no
yes
E
E
E
T ( ) yes~ !  + E ~ !  + E  ! ~ ^ E ! ~
1  2 ^iE ! ~i ^i~i ! iE + E ^i~i ! iE^iiE ! ~i A E ! ~
~ !  E~ !  E
 E ! ~~ !  E + E

We write ~ for the functor [  []]]T (where  [] is the -substitution instance of  )and  E for the functor [  ] TE .
To determine whether the type expression  is an in-type one should look at theentry in row  and column in-type, if it is yes or the immediate subexpressions of satisfy the properties speci ed in the entry, then  is an in-type, otherwise it
may not be.
The auxiliary properties E ! ~ and ~ !  E + E are needed to test whether T ( )is an in-type or out-type.
Table 4.1: Inductive de nition of in-type and out-type32

 Tseff ( ) = (T (  S ))S ATseff (a) = (s: S:[ha; si]T ) TAseff (c) = (s: S:(letT hc1; s1i=cs in c1s1))
A monad morphism : S ! T induces a monad morphism seff : Sseff ! Tseff ,namely seff A = AS S
For every monad T there is one monad morphism Tseff : T ! Tseff Tseff has A-component (Tseff )A(c) = (s: S:(letT a=c in [ha; si]T ))Remark 4.1.8 There is no simple way to turn the monad constructor for sidee ects into a monad over Mon(C ).

We give sucient conditions on arities for the existence of natural liftings ofoperations of those arities along seff .
Proposition 4.1.9 If  1 is a type expression without nesting of T , i.e.

 1 2 Type1: : = 1 j A j j T ( 0) j  1A j  11   12then there is a natural lifting of operations of arity  1 !: T ( ) along  seff .

Proof Let : ! Type be the substitution mapping a type variable to  S ,this induces (in the obvious way) an endofunctor[ ] on C . For every  0 there isa natural transformation in 0: : 0  S !:  0[] (exercise).
Given an operation op:  1 ! T ( ) on S (for simplicity
we take  1 to be  01 :
seff
T ( 02) which is paradigmatic) we can de ne op :  1 ! T ( ) on Sseff to be

opseff (x; c) = (s: S:op (in 01 (x; s); T (in 02)(fs)))
In order to introduce operations on Tseff natural in T , we have to specialise
the parameter S : stores S = U L (compare with Table 2.26 of [Mos89]). This monad model
programs using a xed set L of locations (for simplicity we have not placed
any type restriction on the values storable in a given location, any valueof type U can be stored in any location). Before executing a program
these locations have already a value, either an input data or some garbage.
There are two operations associated with this monad lookup: L ! TU andupdate: L  U ! T 1
33

{ lookup(l) return the contents of location l.
{ update(l; u) updates the contents of location l with u.
 input S = U (compare with Table 2.31 of [Mos89]). This monad model

programs that can input (but not output) data. This semantics is calledbatch in [Mos89], because it does not capture the interleaving between internal computations and input of data. There is one operation associated withthis monad read: 1 ! TU
{ read() read the rst character in the input le and removes it fromsuch le. To de ne read when the input is empty we can either raise
an exception (if T allows that) or return a default value in U .
 output S = U (compare with Table 2.31 of [Mos89]). This monad model
programs that can output (but not input) data. Also this semantics iscalled batch , because it does not capture the interleaving between internal
computations and output of data. There is one operation associated withthis monad write: U ! T 1{ write(u) append the character u to the output le.


4.1.3 Continuations

Continuations are a very general technique used in Denotational Semantics, basedon the idea that if you tell to a piece of program what to do next, then it will tell
you what is the result of the program. This construction takes as parameter a set
R of possible results, or better what can be observed of an entire program, and it
makes sense to take a very small R, e.g. the terminal object 1.
De nition 4.1.10 Given a monad T = (T; T ; T ) the monad Tcont of T -computations
with continuations is de ned as follows: Tcont( ) = (TR)(TR) ATcont (a) = (k: (TR)A :ka)A TAcont (c) = (k: (TR)A :c(h: (TR)(TR) :hk))

Remark 4.1.11 There is no way to make the monad constructor for continuations
into an endofunctor, because Tcont is both covariant and controvariant in T . Because of this one should apply the monad constructor for continuations with someconstraint. In fact, if S and T are related via a monad morphism, there is no
relation between Scont and Tcont which mirrors the one between S and T .
For every monad T there is one monad morphism Tcont: T ! Tcont
34 Tcont has A-component (Tcont)A (c) = (k: (TR)A :(letT a=c in ka))

Remark 4.1.12 It does not make sense to ask whether cont is a natural transformation, because the monad constructor for continuations is not a functor.

We give a simple guideline for using the monad constructor for continuations: start with a simple monad T , e.g. partial computations or non-determinism
 add continuations, so that we have Tcont and a morphism Tcont from T to
Tcont
 add other features modelled by an endofunctor F , so that we can lift Tcont
to a morphism from F (T ) to F (Tcont)
We do not address the issue of lifting operations on T along Tcont.

Exercise 4.1.12.1 cont
Prove that any operation of arity  0  (T )A !: (T ) on T
can be lifted along T .

4.1.4 Variable sets and dynamic allocation

The idea of variable set, i.e. an object of a functor category SetK , has been
proposed by Reynolds, Oles (and others) for capturing the variability of the set of
locations in programming languages like (idealised) ALGOL. However, variables
sets arises in many other situations. For instance, an ML-program, during its
execution, may allocate memory or declare new exceptions. So the set of memory
cells and the set of declared exceptions grow with the number of execution steps.
Similarly, to execute a call=cc or note(c):e (see Talcott) one has to declare a
new name and bind it to the current continuation. A reasonable choice for K
would be the partial order on natural numbers, or natural numbers (viewed assets) with injective maps as morphisms. Intuitively, an element of k 2 K tells us
how many locations there are at that stage. In this section we consider a strong
monad for allocating a new element of a variable set , which can be used as building
block to de ne more complex monads. This construction depends on the following
parameters:
 a category K , an endofunctor F : K ! K , a natural transformation : IdK !:F a variable set L, i.e. a functor L: K !
Set, a global element new of F ; L,i.e. a natural transformation new: 1 !: F ; L
The objects of K should be thought as stages k, providing some information on thecomputation, in particular on the number of locations created so far. Intuitively,
F and  describe the change caused by the allocation of a new element, namely
35

if we start from a stage k allocation causes a transition k from k to a new stage
Fk. At the level of SetK the allocation of a new element transforms a variableset:
A into the variable set F ; A and the natural transformation (; A): A ! F ; A tell
us what are the elements of A after allocation (i.e. F ; A) that were in A before.
Finally, new corresponds to the newly allocated element.
Remark 4.1.13 We have considered the category Set of sets, but what follows
applies to a wide class of categories. An intrinsic limitation of the model above,
suggested by the intuitive explanation, is that the only variability we can capture
is monotonic (a typical feature of Intuitionistic Logic and its Kripke Semantics).
There are some extra requirements on L and new, that seem appropriate if L haveto be understood as a set of names with a decidable equality and new has to be areally new name: if f : k ! k in K , then L(f ) must be an injective map, so that if two names
are di erent at stage k they stay di erent also at later stages
 the element newk of L(Fk) should not be in the image of L(k) along ; L,
i.e. newk is di erent from any element existing before allocation.
These assumptions are not necessary to de ne the strong monad below, but they
are important to de ne operations like update or handle.
De nition 4.1.14
The strong monad T = (T; T ; T ; tT ) for allocation over theKcategory Set is de ned as follows: (TA)(k) = n: N:A(F nk)
if f : k ! k , then (TA)(f )(hn; ai) = hn; A(F nf )ai AT (k)(a) = h0; ai TA (k)(hm; hn; a 2 A(F m+nk)ii) = hm + n; ai00 tTA;B (k)(ha; hn; b 2 B (F nk)ii) = hn; h(n; A)k(a); bii

There is one operation associated with this monad alloc: 1 ! TL alloc(k)() = h1; newk ()i, intuitively alloc makes one F -step in K , from k
to Fk, and picks up the newly allocated element in L(Fk).
Example 4.1.15 The de nition of alloc may look suspicious, because it returns
always the same new element, so one may expect that the denotation ofei  (letT l1=alloc in (letT l2=alloc in [li]T ))does not depend on i. However, the tensorial strength tT renames the locations
created before the last allocation (see requirements on L and new stated in Remark refadd-prop). We give a simple example of strong monad for allocation,
where the expression above have di erent interpretations for di erent i (exercise):36 take K to be the category of natural numbers (viewed as sets, i.e. n =f0; : : :; n 1g) with injective maps as morphisms
 take F to be the endofunctor s.t. F (n) = n + 1 and given an injection
i: m ,! n, then the injection F (i): m + 1 ,! n + 1 extends i to n + 1 bymapping m to n
 take  to be the natural transformation s.t. n: n ,! n + 1 is the inclusionof n into n + 1
 take L: K ! Set to be the inclusion functor of K into Set and newn = n
Prove that in this model L !;L F ; L new 1 is a coproduct diagram (in particlar
newn is not in the image of L(n)) and that [ ei] n = h2; n + ii. On the other hand,
if we take K to be the partial order of natural numbers and F (n) = n + 1 (nmust be the unique morphism from n to n + 1), then there is no way to choose L
and new so that newn is not in the image of L(n).
Instead of de ning a strong monad we should have de ned a strong monadconstructor, which takes a strong monad T over the category C and returns astrong monad Tallc over C K .
Exercise 4.1.15.1 Let (TallcA)(k) = T (n: N:A(F nk)), prove that this can beKextended to a functor from Mon(C ) to Mon(C ). Investigate whether there areother possibilities for Tallc which can be extended to a functor.
Prove that a monad T over C induces a monad T K over SetK (hint: de ne a
2-endofunctor that does the job).
Discuss lifting of operations on T for the monad constructors Talloc and T K .
The monad for allocation is very simple, but if we apply to it the appropriatemonad constructor for stores, namely S = U L (L is the variable set equipped withthe operation alloc), then we can models dynamic memory allocation. Similarly,
to model dynamic declaration of exceptions (as in ML), we have simply to apply
the monad constructor for exceptions (with E = L).
Exercise 4.1.15.2 Reynolds and Oles have been considering functor categories
to model a stack discipline for memory allocation. this means that we are notallowed dynamic allocation of memory that once created cannot be deallocated.
Consider an operation block: U  (TA)L !: TA. Intuitively block(u; (l:e)) is a
block, which declares a new variable l initialised with u, computes a value of type
A and at the end deallocate l. Can you de ne block on the monad of stores overthe functor category SetK ? What kind of assumptions do you need on U and A
for de ning such operation? Hint: we consider the strong monad TA = (A  S )Swith S = U L and require U and A to be constant sets (i.e. U = U K for someset U ). Note that the endofunctor G = SetF preserves limits and colimits and; A: A ! F ; A is a natural transformation from the identity functor on SetK to
G. De ne the following auxiliary operations37

 evalnew: B L ! GB subnew : B L  B ! GB
 incl: G(C B) ! (GC )GBUL L
LL
To de ne block amounts to give a morphism from U  U  ((A  U ) ) toA  U L , or equivalently to GA  (GU )L (because A and U are constant), namely:(subnew  evalnew); G(eval); (GA  (incl; (GU );L))4.1.5 Communication and interleaving

In this section we consider monad constructions that use covariant domain equations. We remind the universal property characterising the least solution to acovariant domain equation in a category C .
De nition 4.1.16 If F is an an endofunctor on C , then a least x point for F isa morphism : FA ! A s.t. for every : FB ! B there exists unique f : A ! B
making the following diagram commutes:
FA
!A

j

j
jj f
#

Ff jj

#

FB
!B
Because of its universal property : FA ! A is actually an isomorphism. It may
well be the case that an endofunctor does not have a least x point, for instancethe powerset functor does not (because of a cardinality argument), but the nite
powerset functor (where only nite subsets are allowed) does have a least x
point. A sucient condition for existence of least x points is that the category C
must have an initial object and colimits of !-chains, and the endofunctor F must
preserve such !-colimits.
The general pattern followed so far for de ning a (strong) monad constructor
F is to express the (strong) monad F (T ) in the metalanguage for T . To keep
this pattern we add a type constructor for recursive types (see the BNF for type
expressions below) and corresponding term constructors (see Table 4.2):
 2 Type: : = 1 j A j j T ( ) j ( : ) j  A j 1  2

Remark 4.1.17 Under fairly general assumptions on the category C and the func-

tor T , every type expression  induces a functor, denoted by  , from C to C .
Actually, if T is a strong monad, then there is a canonically de ned tensorial
38

strength tX; : X   !  [X ] (where X is the substitution mapping to X  )for each functor  . This tensorial strenght is used to interpret the metalanguagein Table 4.2, and to de ne a stronger requirement on a least x point : FA ! A
for a strong endofunctor F , namely that for every : X  FB ! B there exists
unique f : X  A ! B making the following diagram commutes:
XX  FA
!X A

j
j
jj f
h1; F [X ]f i jj##
X  FB! B
where F [X ](f : X  A ! B ) is the morphism tFX;A; Ff from X  FA to FB .

Interactive input and output

In the section on side-e ects we introduced two monads for batch input and output,
here we de ne their interactive counterpart (compare with Table 2.33 of [Mos89]).
De nition 4.1.18 Given a monad T = (T; T ; T ) the monads TiI and TiO of
T -computations with interactive input and output are de ned as follows:
 TiI (A) =  :T (A + ( U ))
 TiO(A) =  :T (A + (U  ))Intuitively, a computation with interactive input may either compute a value or
wait for some input and then resume the computation, while a computation withinteractive output may either compute a value or output some data and thencontinue the computation.
Exercise 4.1.18.1 Complete the de nition of TiI and TiO and prove that thesemonad constructors are endofunctors. Prove that (TiI )iO (A) and (TiO)iI (A) are
isomorphic.
De ne monad morphisms from T to TiI and TiO . What can you say aboutlifting of operations for T along these monad morphisms?
There is one operation read: 1 ! TU associated with the monad TiI and one
operation write: U ! T 1 associated with the monad TiO:
 read() = intro([inr(u: U:[inl(u)]T )]T ) write(u) = intro([inr(hu; [inl()]T i)]T )Exercise 4.1.18.2 De neO a monad morphism from TiO to the monad for batch
output TbO = (T (A  O)) , where O is the set U of nite sequences of elementsin U . How are the two write operations related?


39GEN RULE
var` x: 

f: 1 ! 2

` e1: 1` f(e1): 2

TYPE

INTRO RULE

ELIM RULE

T ( )` e: 
` [e]T : T

` e1: T1
; x1: 1 ` e2: T2` (letT x1=e1 in e2): T21` : 100

1  2

` e1: 1` e2: 2
` he1; e2i: 1  2

` e: 1  2
` i(e): 1

A; a: A ` e: ` (a: A:e):  A` ea: A` e:  A` e(ea): ( : )

` e:  [ : = ( : )]` intro(e):  :

; x:  [ : = ] ` e: 
` e: ( : )` rec(x:e; e): 

Table 4.2: Term expressions

40

Interleaving semantics for CCS

In this section we give a monad constructor for CCS with value passing (comparewith 12.4 of [Sch86]). To justify the domain equation used in the de nition of Tccs
we recall the syntax for CCS terms with value passing and the intended meaningof each operation:

p 2 Process: : = Nil j :p j !u:p j ?x:p(x) j p1 or p2 j p1 jp2 j p n
where range over the set Port of port identi ers (unlike the set Act of actions,
there is no involution operation or silent action for Port) and u range over a set
U of transmittable values. Intuitively, a process, can be: Nil the deadlocked process :p a process which makes an internal indivisible action and becomes p
 !u:p a process which output u on the port and becomes p
 ?x:p(x) a process which wants to input a value from port and becomep(x). Note that p(x) may contain x free, like !x:Nil, and that x get boundedby ?. One may also consider additional operations that use values to de neprocesses.
 p1 or p2 the process which may become either p1 or p2
 p1jp2 the parallel composition of p1 and p2. This involves not only arbitrary
interleaving of actions from p1 with actions from p2, but also communicationof values between the two processes.
 p n the process p with port hidden, i.e. can be used only for internal
communications.
The domain equation below consider the rst ve operations as constructors forde ning processes, while the remaining one have to be de ned (by induction on
the structure of Tccs (A)).
De nition 4.1.19 Given a monad T = (T; T ; T ) the monads Tccs of T -computations
with CCS is de ned as follows: TccsA =  :T (A + 1 + + (Port  U ) + (Port  U  ) + (  ))Exercise 4.1.19.1 Complete the de nition of Tccs. Prove that Tccs can be de ned

by adding incrementally the following features to T -computations (show also thatthe order in which they are added is irrelevant):

 deadlock Tnil(A) = T (A + 1)
41 internal indivisible action Tiia(A) =  :T (A + ) interactive input Tin(A) =  :T (A + (Port  U ))
 interactive output Tout(A) =  :T (A + (Port  U  ))
 non-deterministic choice Tor(A) =  :T (A + (  ))De ne monad morphisms from T to each of the monads for the ve incremental
steps and discuss lifting of operations for T along these monad morphisms.

To deserve the name Tccs the monad constructor for CCS must make available all
the operations on processes:
 Nil: 1 !: T ( ) deadlock  : T ( ) !: T ( ) internal indivisible action
 !: Port  U  T ( ) !: T ( ) output
 ?: Port  (T )U !: T ( ) input
 or: T ( )  T ( ) !: T ( ) non-deterministic choice j: T ( 1)  T ( 2) !: T ( 1  2) parallel composition
 n: Port  T ( ) !: T ( ) hidding of ports

Exercise 4.1.19.2 Give the interpretation for the seven operations on Tccs speci-

ed above. Consider two additional operations on processes seq (p1; p2) and alternate(p1; p2 ).
Intuitively, seq(p1; p2) is sequential composition, i.e. it executes p1 and then (whenp1 has nished) p2 , while alternate(p1; p2) alternates one action of p1 with one of p:2(starting from p1). Give an interpretation for the operations seq : T ( 1)  T ( 2 ) !
T ( 2) and alternate: T ( 1)  T ( 2) !: T ( 1  2) on Tccs (hint: seq is an instanceof let. alternate is underspeci ed, i.e. there are several possible de nitions, and it
is already de nable on Tiia).

42

Bibliography[Abr87]

S. Abramsky. Domain Theory and the Logic of Observable Properties.
PhD thesis, University of London, 1987.
[Bar81] H.P. Barendregt. The Lambda Calculus: Its Syntax and Semantics.
North Holland, 1981.
[BW85] M. Barr and C. Wells. Toposes, Triples and Theories. Springer Verlag,
1985.
[FFKD86] M. Felleisen, D.P. Friedman, E. Kohlbecker, and B. Duba. Reasoning
with continuations. In 1st LICS Conf. IEEE, 1986.
[Flo67] R. Floyd. Assigning meaning to programs. In Schwartz, editor, Proc.
Symp. in Applied Math., 1967.
[GMW79] M.J.C. Gordon, R. Milner, and C.P. Wadsworth. Edinburgh LCF:
A Mechanized Logic of Computation, volume 78 of Lecture Notes in
Computer Science. Springer Verlag, 1979.
[Gog89] J. Goguen. A categorical manifesto. to appear as Oxford PRG technicalreport, 1989.
[Gol79] R. Goldblatt. Topoi, The Categorical Analysis of Logic. North Holland,
1979.
[HJ]
C.A.R. Hoare and H. Jifeng. Natural transformation and data re nement. draft December 7, 1988.
[HM88] R. Harper and J. Mitchell. The essence of ML. In 15th POPL. ACM,
1988.
[Hoa69] C.A.R. Hoare. An axiomatic basis for computer programming. C.
ACM, 12, 1969.
[Kel82] G.M. Kelly. Basic Concepts of Enriched Category Theory. Cambridge
University Press, 1982.
43

[Koc72]

A. Kock. Strong functors and monoidal monads. Archiv der Mathematik, 23, 1972.
[KR77] A. Kock and G.E. Reyes. Doctrines in categorical logic. In J. Barwise,
editor, Handbook of Mathematical Logic, volume 90 of Studies in Logic.
North Holland, 1977.
[KS74] G.M. Kelly and R.H. Street. Review of the elements of 2-categories.
In A. Dold and B. Eckmann, editors, Category Seminar, volume 420
of Lecture Notes in Mathematics. Springer Verlag, 1974.
[Lan64] P.J. Landin. The mechanical evaluation of expressions. Computer
Journal, 6(4), 1964.
[Mac71] S. MacLane. Categories for the Working Mathematician. Springer
Verlag, 1971.
[Mac86] D. MacQueen. Using dependent types to express modular structures.
In 13th POPL. ACM, 1986.
[McC62] J. McCarthy. The LISP 1.5 Programmers' Manual, 1962.
[ML83] P. Martin-Lof. The domain interpretation of type theory. In P. Dybjer, B. Nordstrom, K. Petersson, and J. Smith, editors, Workshop
on the Semantics of Programming Languages. Chalmers University ofTechnology, Goteborg, Sweden, 1983.
[Mog86] E. Moggi. Categories of partial morphisms and the partial lambdacalculus. In Proceedings Workshop on Category Theory and Computer
Programming, Guildford 1985, volume 240 of Lecture Notes in Computer Science. Springer Verlag, 1986.
[Mog88] E. Moggi. The Partial Lambda-Calculus. PhD thesis, University of
Edinburgh, 1988.
[Mog89a] E. Moggi. A category-theoretic account of program modules. In Proceedings of the Conference on Category Theory and Computer Science,
Manchester, UK, Sept. 1989, volume 389 of Lecture Notes in Computer
Science. Springer Verlag, 1989.
[Mog89b] E. Moggi. Computational lambda-calculus and monads. In 4th LICS
Conf. IEEE, 1989.
[Mos89] P. Mosses. Denotational semantics. Technical Report MS-CIS-89-16,
Dept. of Comp. and Inf. Science, Univ. of Pennsylvania, 1989. to appear
in North Holland Handbook of Theoretical Computer Science.
44

[MT89][Pau85][Pie88][Plo75][Plo81][Plo85][Ros86][Sch86][Sco69][Sco70][Sco76][Sco79][Sco80][Sha84]I. Mason and C. Talcott. Programming, transforming, and proving withfunction abstractions and memories. In 16th Colloquium on Automata,
Languages and Programming. EATCS, 1989.
L.C. Paulson. Interactive theorem proving with cambridge lcf: a user's
manual. Technical Report 80, Univ. of Cambridge, Computer Laboratory, 1985.
B.C. Pierce. A taste of category theory for computer scientists. Technical Report CMU-CS-88-203, Carnegie-Mellon Univ., Dept. of Comp.
Sci., 1988.
G.D. Plotkin. Call-by-name, call-by-value and the -calculus. Theoretical Computer Science, 1, 1975.
G.D. Plotkin. Postgraduate lecture notes in domain theory (incorporating the \pisa notes"). Edinburgh Univ., Dept. of Comp. Sci., 1981.
G.D. Plotkin. Denotational semantics with partial functions. Lecture
Notes at C.S.L.I. Summer School, 1985.
G. Rosolini. Continuity and E ectiveness in Topoi. PhD thesis, University of Oxford, 1986.
D.A. Schmidt. Denotational Semantics: a Methodology for Language
Development. Allyn & Bacon, 1986.
D.S. Scott. A type-theoretic alternative to CUCH, ISWIM, OWHY.
Oxford notes, 1969.
D.S. Scott. Outline of a mathematical theory of computation. Technical
Report PRG-2, Oxford Univ. Computing Lab., 1970.
D.S. Scott. Data types as lattices. SIAM Journal of Computing, 5,
1976.
D.S. Scott. Identity and existence in intuitionistic logic. In M.P. Fourman, C.J. Mulvey, and D.S. Scott, editors, Applications of Sheaves,volume 753 of Lecture Notes in Mathematics. Springer Verlag, 1979.
D.S. Scott. Relating theories of the -calculus. In R. Hindley and
J. Seldin, editors, To H.B. Curry: essays in Combinarory Logic, lambda
calculus and Formalisms. Academic Press, 1980.
K. Sharma. Syntactic aspects of the non-deterministic lambda calculus. Master's thesis, Washington State University, September 1984.
available as internal report CS-84-127 of the comp. sci. dept.
45

[SS71]

D.S. Scott and C. Strachey. Toward a mathematical semantics for computer languages. Technical Report PRG-6, Oxford Univ. Computing
Lab., 1971.
[Wad76] C. Wadsworth. The relation between computational and denotational
properties for scott's D -models of the lambda calculus. SIAM Journalof Computing, 5, 1976.
1

46

Course exercises
1. Express A, A and T (f : A ! B ) in the metalanguage with base types A
and B and unary operation f : A ! B .
Given two monads S and T over the category C , express that  is a simpli ed
monad morphism from S to T via a set of equations in the metalanguagewith two unary type constructors S and T , one base type for each object of
C and one unary function  : S ! T for each type expression  . Try to
make the equations as simple as possible, no more than two let or [ ] in eachequation. Given two strong monads S and T over the category C , What
additional axioms do you need (if any) to express that  is a strong monadmorphism?
2. Prove that any operation of arity  0  (T )A !: (T ) on T can be lifted along
Tcont: T ! Tcont. Discuss possible improvements to lifting of operations alongcont and seff .
3. Given a category K , and an endofunctor F : K ! K de ne two functors from
Mon(C ) to Mon(C K ). If T is a monad over C , then
 T K (A)(k) = T (A(k)) (hint: de ne a 2-endofunctor on Cat that does
the job for any K ).
 (TallcA)(k) = T (n: N:A(F nk)) (we assume that C has countable coproducts)
complete the de nition of T K and Tallc and de ne a monad morphism fromT K to Tallc.
Investigate whether there are other possibilities for Tallc which take a monadT in C K instead.
Discuss lifting of operations on T for the monad constructors Talloc and T K(hint: is there a monad morphism in the generalized sense from T to these
two monads on C K )4. Reynolds and Oles have been considering functor categories to model a stackdiscipline for memory allocation. this means that we are not allowed dynamic
allocation of memory that once created cannot be deallocated. Consider an47

operation block: U  (TA)L !: TA. Intuitively block(u; (l:e)) is a block,which declares a new variable l initialized with u, computes a value of type
A and at the end deallocate l. Can you de ne block on the monad of storesover the functor category C K by choosing a suitable K and L? What kindof assumptions do you need on U and A for de ning such operation? (hint:consider the restrictions on a programming language, that make possible astack discipline for memory allocation).
5. Complete the de nition of the monad constructor for CCS

TcssA =  :T (A + 1 + + (Port  U ) + (Port  U  ) + (  ))Prove that Tccs can be de ned by adding incrementally the following features
to T -computations (show also that the order in which they are added isirrelevant):
 deadlock Tnil(A) = T (A + 1)
 internal indivisible action Tiia(A) =  :T (A + ) interactive input Tin(A) =  :T (A + (Port  U ))
 interactive output Tout(A) =  :T (A + (Port  U  ))
 non-deterministic choice Tor (A) =  :T (A + (  ))De ne monad morphisms from T to each of the monads for the ve incremental steps and discuss lifting of operations for T along these monadmorphisms.
6. Prove that (Tin )out(A) and (Tout)in(A) (see previous esercise) are isomorphic.
De ne a simpli ed version, TbO = (T (A  O))O , of the monad for batch
output, where O is the set U of nite sequences of elements in U . De ne amonad morphism from Tout to TbO, then consider how the interpretations of
the operation write: U ! T 1 in the two monad are related.
7. Give the interpretation for the following operations on Tcss:
 Nil: 1 !: T ( ) deadlock  : T ( ) !: T ( ) internal indivisible action
 !: Port  U  T ( ) !: T ( ) output
 ?: Port  (T )U !: T ( ) input
 or: T ( )  T ( ) !: T ( ) non-deterministic choice j: T ( 1)  T ( 2) !: T ( 1  2) parallel composition
 n: Port  T ( ) !: T ( ) hidding of ports48

Consider two additional operations on processes seq(p1; p2) and alternate(p1; p2).
Intuitively, seq(p1; p2) is sequential composition, i.e. it executes p1 and then(when p1 has nished) p2, while alternate(p1; p2) alternates one action of p1
with one of p2 (startingfrom p1). Give an interpretation for: the operations:
seq: T ( 1)  T ( 2) ! T ( 2) and alternate: T ( 1)  T ( 2) ! T ( 1  2) on
Tccs (hint: seq is an instance of let. alternate is underspeci ed, i.e. there areseveral possible de nitions, and it already de nable on Tiia).

49