Semantic LegoDavid A. Espinosa

Submitted in partial ful llment of therequirements for the degreeof Doctor of Philosophy
in the Graduate School of Arts and Sciences.
COLUMBIA UNIVERSITY
1995

c 1995
David A. Espinosa
ALL RIGHTS RESERVED

ABSTRACT

Semantic LegoDavid A. Espinosa
Denotational semantics Sch86] is a powerful framework for describing programming languages however, its descriptions lack modularity: conceptually independent
language features in uence each others' semantics. We address this problem by presenting a theory of modular denotational semantics.
Following Mosses Mos92], we divide a semantics into two parts, a computation
ADT and a language ADT (abstract data type). The computation ADT represents
the basic semantic structure of the language. The language ADT represents theactual language constructs, as described by a grammar. We de ne the language ADT
using the computation ADT in fact, language constructs are polymorphic over manydierent computation ADTs.
Following Moggi Mog89a], we build the computation ADT from composable parts,
using monads and monad transformers. These techniques allow us to build manydierent computation ADTs, and, since our language constructs are polymorphic,
many dierent language semantics.
We automate these ideas in Semantic Lego (SL), a modular language construction set written in Scheme. SL generates interpreters automatically from composable
parts and is a useful tool for programming language design.

Contents
Table of Contents
List of Figures
List of Tables
1 Introduction

1.1 Denotational Semantics : : : : : : : : : : : : : : : : : : : : : : : : : :1.1.1 Domains / Types : : : : : : : : : : : : : : : : : : : : : : : : :1.1.2 Logics : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :1.1.3 Environments : : : : : : : : : : : : : : : : : : : : : : : : : : :1.1.4 Stores : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :1.1.5 Continuations : : : : : : : : : : : : : : : : : : : : : : : : : : :1.1.6 The importance of types : : : : : : : : : : : : : : : : : : : : :1.2 Languages as ADTs : : : : : : : : : : : : : : : : : : : : : : : : : : : :1.3 Monolithic interpreters : : : : : : : : : : : : : : : : : : : : : : : : : :1.4 Modular interpreters : : : : : : : : : : : : : : : : : : : : : : : : : : :1.4.1 Lifting interpreter : : : : : : : : : : : : : : : : : : : : : : : : :1.4.2 Strati ed interpreter : : : : : : : : : : : : : : : : : : : : : : :1.5 Examples : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :1.5.1 A Scheme-like language : : : : : : : : : : : : : : : : : : : : : :1.5.2 Nondeterminism and continuations : : : : : : : : : : : : : : :1.5.3 Uni ed system of parametrization : : : : : : : : : : : : : : : :1.5.4 Resumptions : : : : : : : : : : : : : : : : : : : : : : : : : : :2 Monads

2.1 Basic category theory : : : : : : : : : : : : : : : : : : : : : : : : : : :2.1.1 Categories : : : : : : : : : : : : : : : : : : : : : : : : : : : : :2.1.2 Functors : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :2.1.3 Natural transformations : : : : : : : : : : : : : : : : : : : : :2.1.4 Initiality : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :2.1.5 Duality : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :2.1.6 Category theory and functional programming : : : : : : : : :2.1.7 References : : : : : : : : : : : : : : : : : : : : : : : : : : : : :
i

i
iv
vi
1

3
3
4
6
6
7
8
9
15
18
20
22
26
27
30
32
32

38
38
39
39
40
41
41
42
42

2.2 Monads : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :2.2.1 First formulation : : : : : : : : : : : : : : : : : : : : : : : : :2.2.2 Second formulation : : : : : : : : : : : : : : : : : : : : : : : :2.2.3 Interpretations : : : : : : : : : : : : : : : : : : : : : : : : : :2.3 Monad morphisms : : : : : : : : : : : : : : : : : : : : : : : : : : : :2.4 Monads don't compose : : : : : : : : : : : : : : : : : : : : : : : : : :2.5 Monads do compose : : : : : : : : : : : : : : : : : : : : : : : : : : :2.6 Monad transformers : : : : : : : : : : : : : : : : : : : : : : : : : : :2.6.1 Motivation : : : : : : : : : : : : : : : : : : : : : : : : : : : : :2.6.2 Formalization : : : : : : : : : : : : : : : : : : : : : : : : : : :2.6.3 Classes of monad transformers : : : : : : : : : : : : : : : : : :2.6.4 Composition of monad transformers : : : : : : : : : : : : : : :

43
43
44
48
52
52
53
56
56
58
60
62

3 Lifting63

4 Stratication

69

5 Conclusion

82

Bibliography
A Miscellanea

9398

3.1 Lifting : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :3.1.1 Formal lifting : : : : : : : : : : : : : : : : : : : : : : : : : : :3.1.2 Monads and lifting : : : : : : : : : : : : : : : : : : : : : : : :3.2 Pragmatics : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :3.2.1 Bottom-up : : : : : : : : : : : : : : : : : : : : : : : : : : : : :3.2.2 Top-down : : : : : : : : : : : : : : : : : : : : : : : : : : : : :4.1 Strati ed monads : : : : : : : : : : : : : : : : : : : : : : : : : : : : :4.2 Strati ed monad transformers : : : : : : : : : : : : : : : : : : : : : :4.2.1 Top transformers : : : : : : : : : : : : : : : : : : : : : : : : :4.2.2 Bottom transformers : : : : : : : : : : : : : : : : : : : : : : :4.2.3 Around transformers : : : : : : : : : : : : : : : : : : : : : : :4.2.4 Continuation transformers : : : : : : : : : : : : : : : : : : : :4.3 Computation ADTs : : : : : : : : : : : : : : : : : : : : : : : : : : : :4.4 Language ADTs : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :
5.1
5.2
5.3
5.4
5.5

Lifting versus strati cation : : : : : : : : : : : : : : : : : : : : : : : :Limitations : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :Related work : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :Future work : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :Conclusion : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :

63
63
66
66
67
68
69
71
73
74
74
75
76
79
82
83
86
90
91

A.1 Why Scheme? : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 98
A.2 Typed versus untyped values : : : : : : : : : : : : : : : : : : : : : : : 100
A.3 Extensible sums and products : : : : : : : : : : : : : : : : : : : : : : 101ii

B Code103

B.1 Monad transformer de nitions : : : : : : : : : : : : : : : : : : : : : : 103
B.2 Language construct de nitions : : : : : : : : : : : : : : : : : : : : : : 111

iii

List of Figures
1.1 Interpreter : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :1.2 Environment ADT : : : : : : : : : : : : : : : : : : : : : : : : : : : :1.3 Expression predicates and selectors : : : : : : : : : : : : : : : : : : :1.4 Expression constructors : : : : : : : : : : : : : : : : : : : : : : : : :1.5 Interpreter interface : : : : : : : : : : : : : : : : : : : : : : : : : : : :1.6 Denotational implementation : : : : : : : : : : : : : : : : : : : : : :1.7 Map from syntax to semantics : : : : : : : : : : : : : : : : : : : : : :1.8 Monolithic interpreter, part 1 : : : : : : : : : : : : : : : : : : : : : :1.9 Monolithic interpreter, part 2 : : : : : : : : : : : : : : : : : : : : : :1.10 Store ADT : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :1.11 Lifting operators : : : : : : : : : : : : : : : : : : : : : : : : : : : : :1.12 Value level : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :1.13 Store level : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :1.14 Environment level : : : : : : : : : : : : : : : : : : : : : : : : : : : : :1.15 Level-negotiating operators : : : : : : : : : : : : : : : : : : : : : : : :1.16 Modular interpreter, part 1 : : : : : : : : : : : : : : : : : : : : : : :1.17 Modular interpreter, part 2 : : : : : : : : : : : : : : : : : : : : : : :1.18 Example speci cation and expressions : : : : : : : : : : : : : : : : : :1.19 %let source de nition : : : : : : : : : : : : : : : : : : : : : : : : : :1.20 %let de nition simpli ed : : : : : : : : : : : : : : : : : : : : : : : : :1.21 %amb source de nition : : : : : : : : : : : : : : : : : : : : : : : : : :1.22 %amb version 1 : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :1.23 %amb version 2 : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :1.24 %amb version 3 : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :1.25 Uni ed system of parametrization : : : : : : : : : : : : : : : : : : : :1.26 Uni ed parametrization examples : : : : : : : : : : : : : : : : : : : :1.27 Parallel language using resumptions : : : : : : : : : : : : : : : : : : :2.1 Example monads, part 1 : : : : : : : : : : : : : : : : : : : : : : : : :2.2 Example monads, part 2 : : : : : : : : : : : : : : : : : : : : : : : : :2.3 Monads don't compose : : : : : : : : : : : : : : : : : : : : : : : : : :2.4 Environment monad transformer : : : : : : : : : : : : : : : : : : : :4.1 First answer transformer : : : : : : : : : : : : : : : : : : : : : : : : :
iv

10
11
12
12
13
13
14
16
17
17
21
22
23
24
26
27
28
29
30
31
31
33
34
35
36
36
37
46
47
53
57
76

4.2 Second answer transformer : : : : : : : : : : : : : : : : : : : : : : : : 76
5.1 Odd de nition of %end-of-input? : : : : : : : : : : : : : : : : : : : 85
B.1 Environment transformer : : : : : : : : : : : : : : : : : : : : : : : : : 104
B.2 Exception transformer : : : : : : : : : : : : : : : : : : : : : : : : : : 105
B.3 Continuation transformer : : : : : : : : : : : : : : : : : : : : : : : : : 105
B.4 Store transformer : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 106
B.5 First lifting transformer : : : : : : : : : : : : : : : : : : : : : : : : : 107
B.6 Second lifting transformer : : : : : : : : : : : : : : : : : : : : : : : : 107
B.7 List transformer : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 108
B.8 Monoid transformer : : : : : : : : : : : : : : : : : : : : : : : : : : : : 109
B.9 Resumption transformer : : : : : : : : : : : : : : : : : : : : : : : : : 110
B.10 Amb : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 111
B.11 Reset : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 111
B.12 Stores : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 112
B.13 Output : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 112
B.14 While : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 113
B.15 Begin : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 113
B.16 Error exceptions : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 114
B.17 Error values : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 114
B.18 Batch I/O : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 115
B.19 Booleans : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 116
B.20 Call with current continuation : : : : : : : : : : : : : : : : : : : : : : 117
B.21 Dynamically scoped procedures : : : : : : : : : : : : : : : : : : : : : 118
B.22 Environments : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 119
B.23 Fixed points : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 120
B.24 Letrec using xed points : : : : : : : : : : : : : : : : : : : : : : : : : 121
B.25 Numbers : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 122
B.26 Statically scoped procedures : : : : : : : : : : : : : : : : : : : : : : : 123
B.27 Resumptions : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 124
B.28 Products : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 125
B.29 Sums : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 126
B.30 Shift : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 127v

List of Tables
2.1
2.2
2.3
2.4
2.5
4.1
4.2
4.3
4.4
5.1

Monad type constructors : : : : : : : : : : : : : : : : : : : : : : : : :Meaning of existence : : : : : : : : : : : : : : : : : : : : : : : : : : :Monad transformers : : : : : : : : : : : : : : : : : : : : : : : : : : :Monad transformer classi cation : : : : : : : : : : : : : : : : : : : : :Classi cation examples : : : : : : : : : : : : : : : : : : : : : : : : : :Names associated with each transformer : : : : : : : : : : : : : : : :Levels and names for a complex language : : : : : : : : : : : : : : : :Procedure types : : : : : : : : : : : : : : : : : : : : : : : : : : : : : :Modules and language constructs : : : : : : : : : : : : : : : : : : : :Non-local language constructs : : : : : : : : : : : : : : : : : : : : : :

vi

44
50
57
61
62
78
79
80
81
83

Acknowledgements
Mary Ng, my ancee, has been waiting patiently for this thesis for several years.
I could have done it without her, but it would have been much worse, and it was
already bad. Mary is easily the happiest result of grad school.
Joanne Espinosa, my mother, has been great for 28 years. Thanks, mom.
Gerald J. Sussman, who I have known for a decade now, has always been an
inspiration. His faith in his students never fails, and talking with him makes you
believe, if only for a moment, that you can do anything. On the more material side,
Jerry let me hang out at his lab for the last year (or more).
Sal Stolfo, my advisor at Columbia, has been an extremely tolerant observer ofmy graduate school career. In part, I picked Sal as an advisor because he was a niceguy remarkably, he still is.
My defense committee, Gail Kaiser, Ken Ross, and Mukesh Dalal, helped me getout of Columbia in one piece.
Albert Greenberg rescued me from unemployment for several summers at AT&T.
He initially hired me because \it takes less paper work to hire Ph.D. scholars". We
had fun hacking parallel Fourier transforms and solving models of communication
networks. The connection between that and monads seems certain, but, for thepresent time, obscure.
An AT&T Ph.D. scholarship supported me for ve years, and they didn't evenmake me beg too hard for a fth year. Unfortunately, all they gave me was money(Albert notwithstanding).
Thanks to Phil Chan, Mauricio Hernandez, Sushil Da Silva, Paul Michelman,
and Bulent Yener for keeping me company at Columbia. Similarly for Michael Blair,
Kleanthes Koniaris, Natalya Cohen, Raj Surati, and all the other fourth- oor peopleat MIT.
Thanks also to my musical friends, Joseph Briggs, Kerstin Kup, Brian and Karen
Neal, Lois Winter, and Johelen Carleton.
vii

Albert Meyer has been great fun on many occasions. It's splendid to talk tosomeone who knows semantics inside and out, along with most of its history. You
just can't get that from papers!
Eugenio Moggi deserves my thanks for his work, sine qua non. Albert objected
to Moggi's inclusion here since our relationship is scienti c rather than personal (especially since I've never met him). Albert, as a logician, splits any hair he can nd.
Jonathan Rees introduced me to monads and category theory. I hope we'll beable to work more together later. Now he's o chasing bugs in England.
Bill Rozas helped me out on many, many occasions and was always happy to
discuss semantics or architecture. Bill is incredibly generous and made me feel that
we were equals, even when we weren't. I envy him this quality.
Carl Gunter has been a great source of advice and assistance. When I rst met him
at LFP in 1992, he was a soft-spoken man who, after a heated semantics argument
died down, would say, \Actually, the real answer is : : : ". His explanations and his
book Gun92] are crystal clear.
Charles Leiserson provided convincing evidence to attend MIT as an undergrad
by being the most interesting person at Brown when I visited there. He did a great
job teaching me algorithms, but I gure that eld's too easy anyway. Charles has an
astounding ability to formalize just about anything.
Franklyn Turbak and I have had enormous fun hacking interpreters and languages
for the last two years. Until meeting Lyn, I was convinced that formal semantics was a
non-sensical hodgepodge of Greek letters intended to confuse the reader into thinking
the eld had actual content. My present views you'll have to ascertain by reading
this thesis.

viiiChapter 1
Introduction
Denotational semantics is a powerful framework for de ning programming languages.
Using it, we can describe languages concisely and unambiguously and build interpreters that execute actual programs. It is not a dicult theory to understand,especially considering its power.
Unfortunately, it is hard to read and write denotational descriptions, primarily
because they lack modularity. Each language construct interacts with all the semantic
building blocks that form the language's foundation. For example, if we model assignment using a store, then every language construct must interact with the store, notjust assignment. The complexity of this interaction makes denotational descriptions
overly intricate.
This thesis presents a modular style of writing denotational descriptions, which we
automate as Semantic Lego1(SL), a Scheme program that builds interpreters fromcomponent parts. In essence, SL is a language for describing languages. This workmakes several important contributions: We reintroduce the idea of programming languages as abstract data types. Interpreters written in this style are shorter and clearer than usual.

 We restate Moggi's theory of lifting in simple terms, making it accessible to a1

Lego is a registered trademark of Interlego AG.

1

2
wider audience.

 We describe a new theory of strati cation that is simpler than lifting yet more
powerful. This theory extends Mosses's work on semantic algebras, adding
structure and modularity.

 We show two styles of writing modular interpreters, based respectively on liftingand strati cation.

 We present Semantic Lego, a modular language construction set based on
strati cation, and give several examples.

This work has several important consequences: We can understand, discuss, and teach languages better by decomposing theminto parts. For example, the resumptions model of parallelism appears complex
until we see it as a combination of several simple features.

 We can experiment with new languages. SL handles the bookkeeping associatedwith denotational descriptions, leaving the designer free to consider higher-levelissues. SL's underlying theory can also help suggest new language constructs.

The following story illustrates SL's power. Three teaching assistants for the MIT
graduate programming languages course needed to describe the semantics of a sophisticated control construct (shift) in the presence of state. Although they understoodcontrol and state independently, they were unable to nd a suitable interaction between these features before distributing the problem set.
Using SL, I generated two solutions in under a minute. In fact, SL formed complete
interpreters, not just the single required construct. It was also easy to add errors
generation and handling, another semantic complication. Since I was con dent inSL's ability to produce correct semantics, I did not even examine the de nitions to
see if they were well-formed.

3
The thesis is organized as follows. Chapter 3 discusses lifting chapter 4 discusses
strati cation. Chapter 5 compares these approaches and reviews previous work. Appendix A covers issues tangentially related to the thesis.
We assume an elementary understanding of denotational semantics and functional
programming for further background, see Wad92]. All examples and code fragments
are in Scheme CR91].
The rest of this chapter presents languages as abstract data types, demonstrates
that the usual style of writing interpreters isn't modular, shows two styles of writing
modular interpreters, and exercises SL with a series of examples.

1.1 Denotational Semantics
In this section, we discuss denotational semantics, the theory on which SL isbased. Excellent references are Gun92, Sch86]. In general, semantics is the study of
meaning. Our goal is to determine, for example, that x = x+1 means \add one to x".
Programming language semantics is actually a branch of mathematical logic themain dierence is that logics are for reasoning, while programming languages arefor computation. Semantics (whether of propositions or programs) is split into twointeracting parts. Proof theory, the more syntactic part, lets us reason and compute.
Model theory, the more semantic part, lets us describe what we are actually reasoning
and computing about.

1.1.1 Domains / Types
Our rst step is to describe the raw material for building models. This elaborate
subject is called domain theory however, most of it is irrelevant to our interest inmodeling language features. I usually call domains types, although the concepts are
not quite the same.
We begin with base types such as Num, Bool, and String. We glue these together
using the type constructors ! (function space),  (cartesian product), and + (disjoint

4union). A ! B is the set of functions from A to B . Since ! associates to the right,
A ! B ! C means A ! (B ! C ). A  B is the set of all pairs (a b). A + B is theset of all (0 a) and (1 b). That is, elements of A + B are either A's or B 's, exceptthat we can always tell which is which by checking the tag. Thus, A + A is dierent
from A.
Two types A and B are isomorphic (set-theoretically) if there exist functions
f : A ! B and g : B ! A such that f  g = g  f = id. Writing = for isomorphism,
we have

A+B 
= B+A
AB 
= BA
(A + B ) + C = A + (B + C )(A  B )  C = A  (B  C )A  (B + C ) = AB +AC
A ! (B ! C ) = AB !C
(A ! C )  (B ! C ) = (A + B ) ! C
Thus, +, , and ! resemble addition, multiplication, and exponentiation. Becauseof this structure, types built using these constructors are called algebraic types. Also,
all one-element sets are isomorphic (and similarly for other cardinalities). If we distinguish a set of each cardinality, we can also write identities such as 0  A = 0 and1+1 = 2.

1.1.2 Logics
A logic is given by a language, a class of models, a set of inference rules, and ameaning or denotation function for each model. The meaning function maps terms

5in the language to elements of the model and interprets the language as being about
the model. The inference rules are used for reasoning or computation. Let's take asimple arithmetic language:= Num
j Exp + Exp
j Exp  Exp(Exp )
Num = Dig j DigNum
Dig = 0 : : : 9
Exp

An example expression is 3  (10 + 1). For a model, we have the usual natural
numbers. For inference rules, we have the usual identity, associative, commutative,and distributive laws. The meaning function sends expressions to actual numbers.
For example, it sends 3  (10 + 1) to 33. The inference rules must be sound thatis, they must preserve meanings. For example, if we apply the distributive law to
3  (10 + 1) to get 3  10 + 3  1, the meaning of this totally dierent expression mustalso be 33. Note that we specify only a single model, while our de nition allows aclass of models see Mes89] for a more thorough treatment of logics.
Interestingly, we have two ways of evaluating expressions: inside the language,
using the inference rules, and outside the language, using the meaning function. If
we use the meaning function, we need a way to compute in the language in which themeaning function is described (the metalanguage). Sometimes this means is available
for example, if we implement an evaluator for the above language in C, we can use
C's arithmetic. Sometimes it is not in performing arithmetic by hand, we use theinference rules to justify the syntactic manipulations of the usual addition and multiplication algorithms. In this thesis, we build interpreters using meaning functions
and focus on models rather than inference rules.
Most meaning function de nitions are compositional: the meaning of an expression
depends only on the meaning of its subexpressions, rather than their exact syntax.
For example, in the arithmetic language, the meaning of a + b is the sum of themeanings of a and b.

6

1.1.3 Environments
The semantics of more complex programming languages is simply an elaborationof the above example. In the rest of this section, we discuss the basic techniques.
For example, suppose we add variables and a binding construct let to the language.
Now we can write (shifting to a Scheme-like notation):(let ((a 1) (b 2))(+ a (* b 3)))The meaning of the overall program could still be a number, but what about themeaning of an expression such as a? We take the meaning of an expression to be afunction from an environment to a number, where the environment assigns values tovariables. We can view the environment as a function from variables to values or as
a list of variable / value pairs it doesn't matter which.
Thus, meanings (or denotations), instead of being numbers, are elements of
Den = Env ! Num

The primary inference rule for variables is substitution. It must be carefully dened, and there are several variations, but, in general, we can infer that(let ((a 1) (b 2))(+ a (* b 3)))has the same meaning as (+ 1 (* 2 3)). Although it seems simple, it is already noteasy to prove the soundness of this inference rule with respect to the environment
model.

1.1.4 Stores
The next complication arises in modeling state. Suppose we have a language withassignment statements and sequencing. We can write programs such as
a = 1
b = 2
a = a + b
return a

7
The meanings of statements are functions from stores to stores, where a store is justanother name for an environment. That is, a statement accepts a set of variablebindings and returns a new set. We write this as
Den = Sto ! Sto

For example, the meaning of a = a + 1 sends a store binding a to 3 to a store binding
a to 4. To be accurate, we need separate meaning functions for programs, statements,and expressions. We have
Den Program = Num
Den Statement = Sto ! Sto
Den Expression = Sto ! Num

We also need to handle unbound variables somehow there are several viable approaches. We could return an observable error value (that we could test), an unobservable error value (that would propagate through all operators unchanged), or we
could abort the computation immediately.

1.1.5 Continuations
One way to model an abort operator is via continuations. The continuation represents the rest of the computation, a map from the current store to the nal store. A
statement accepts both a store and a continuation. Most statements form a new store(as usual) and apply the continuation to the result, thus continuing the computation.
To abort, statements return the store directly, ignoring the continuation. Thus, amodel for statements is
Den = Sto ! Cont ! Sto
Cont = Sto ! Sto

In a language with operators for manipulating continuations, such as catch andthrow, we can build non-local control structures for backtracking or coroutines. This
example shows that semantic concepts can sometimes suggest new and useful language
features.

8

1.1.6 The importance of types
Quite often, once we specify the language and the model, there are few ways to
map terms to denotations. Once we know that
Den = Env ! Num(and that environments map variables to numbers), it is clear how to de ne variablereference. Thus, an experienced semanticist needs only the language, the model,
and some general instructions about how the language should behave in order toreconstruct its exact semantics. The model alone conveys most of the interesting
information, which is why types are good tools for describing semantics.
Why do models determine language construct semantics so completely? With
respect to the values they manipulate, language constructs are general and uniform.
For example, function call works for all types, and in the same way. This notion,formalized by Reynolds, is called parametric polymorphism.
In the above semantics, it is clear that the only sensible meaning for a variable is
to look it up in the environment. How else could we get a number? We would haveto make one up, which would not be general. A good reference for this material isWad89], which describes Reynolds' result that polymorphic functions obey identities
derivable solely from their types. For example, a function f : List (A) ! List (A)must obey(f (map g l)) = (map g (f l))

for any l : List (A) and g : A ! B .
Since models tightly constrain language semantics, we always begin by nding asuitable model. Furthermore, it is not surprising that a modular theory of interpreters
begins with a modular theory of models.

9

1.2 Languages as ADTs
We begin with a simple interpreter in the style of Abelson and Sussman ASS85]
and reduce it to its essence, eliminating issues of syntax as much as possible. Thisapproach shows that \metalinguistic abstraction" is no dierent from ordinary abstraction. In other words, it is not necessary to \go outside" the implementation
language in order to program in the target language. It also provides a streamlined
style of writing interpreters that shortens them and makes the separation of syntax
and semantics more apparent.
A simple interpreter for a purely functional language appears in gures 1.1 { 1.3.
A typical use of it is(compute '((lambda x (* x x)) 9))
81)

This interpreter parses concrete syntax in the form of lists. That is, it recognizes thesubset of lists that are valid programs. Parsing has little to do with semantics, so wepass to an abstract syntax, using the constructors shown in gure 1.4. Now the same
program reads as(compute (%call (%lambda 'x (%* (%var 'x) (%var 'x))) (%num 9)))81)

which is more explicit (but less readable).
These constructors, along with the procedure compute, describe the interpreter as
an abstract data type (ADT), whose signature is shown in gure 1.5. Of course, thesignature only partially speci es the behavior of the interpreter. The easiest way todescribe its behavior more completely is to provide a \model" implementation, suchas the one in gures 1.1 { 1.4.
Now that we have speci ed the interpreter's interface, we can ask whether there
is a simpler implementation. In fact, gure 1.6 shows that there is. In this gure, we
use the Scheme syntax for de ning curried functions, so that(define ((f a) b) ...)

10

(define (eval exp env)
(cond ((number? exp) (eval-number exp env))((variable? exp) (eval-variable exp env))((lambda? exp) (eval-lambda exp env))((if? exp) (eval-if exp env))((+? exp) (eval-+ exp env))((*? exp) (eval-* exp env))(else (eval-call exp env))))(define (compute exp)
(eval exp (empty-env)))(define (eval-number exp env)
exp)
(define (eval-variable exp env)
(env-lookup exp env))(define (eval-lambda exp env)
(lambda (val)(eval (lambda-body exp)
(extend-env env (lambda-variable exp) val))))(define (eval-call exp env)((eval (call-operator exp) env)
(eval (call-operand exp) env)))(define (eval-if exp env)
(if (eval (if-condition exp) env)
(eval (if-consequent exp) env)
(eval (if-alternative exp) env)))(define (eval-+ exp env)(+ (eval (op-arg1 exp) env)
(eval (op-arg2 exp) env)))

Figure 1.1: Interpreter

11(define (empty-env) '())
(define (env-lookup var env)
(let ((entry (assq var env)))(if entry(error "Unbound variable: " var)(right entry))))(define (env-extend var val env)
(pair (pair var val) env))

Figure 1.2: Environment ADT
expands into
(define f (lambda (a) (lambda (b) ...)))

Notice that the syntactic constructors and selectors have entirely disappeared.
The new implementation is shorter, yet it preserves the semantic content of the original. We call gure 1.6 a denotational implementation of the language ADT because
we represent expressions by their denotations rather than their syntax. We call anequation such as
Den = Env ! Val
the basic semantics of the language. We write Den in place of Exp to re ect thechange in point of view, but the ADT semantics remains the same.
Despite these advantages, few authors write interpreters in this style, perhaps
because most languages encourage programmers to use concrete (rather than abstract)
data types. For example, Scheme emphasizes lists, while ML and Haskell emphasize
algebraic data types (sums and products). Programmers in languages with bettersupport for ADTs might arrive more easily at this style, although rst-class functions
are also necessary.
The denotational style shows explicitly that the semantics is compositional, whichis to say that the meaning of an expression is composed from the meanings of its imme-

12(define variable? symbol?)(define (lambda? exp)
(eq? 'lambda (first exp)))(define lambda-variable second)(define lambda-body third)(define call-operator first)(define call-operand second)(define (if? exp)
(eq? 'if (first exp)))(define if-condition second)(define if-consequent third)(define if-alternative fourth)(define (+? exp)
(eq? '+ (first exp)))(define (*? exp)
(eq? '* (first exp)))(define op-arg1 second)(define op-arg2 third)

Figure 1.3: Expression predicates and selectors(define (%num x) x)(define (%var name) name)(define (%lambda name exp) (list 'lambda var exp))(define (%call e1 e2) (list e1 e2))
(define (%if e1 e2 e3) (list 'if e1 e2 e3))
(define (%+ e1 e2) (list '+ e1 e2))
(define (%* e1 e2) (list '* e1 e2))

Figure 1.4: Expression constructors

13

compute%num%var%lambda
%call
%if
%+
%*

: Exp
: Val
: Name: Name  Exp: Exp  Exp: Exp  Exp  Exp: Exp  Exp: Exp  Exp

! Val
! Exp
! Exp
! Exp
! Exp
! Exp
! Exp
! Exp

Figure 1.5: Interpreter interface
 Den Proc= Env ! Val= Val ! Val(define ((%num n) env)n)(define ((%var name) env)
(env-lookup name env))(define ((%lambda name den) env)
(lambda (val)(den (env-extend env var val))))(define ((%call d1 d2) env)((d1 env) (d2 env)))(define ((%if d1 d2 d3) env)
(if (d1 env) (d2 env) (d3 env)))(define ((%+ d1 d2) env)(+ (d1 env) (d2 env)))(define ((%* d1 d2) env)(* (d1 env) (d2 env)))

Figure 1.6: Denotational implementation

14(define (D exp)
(cond ((number? exp) (%num exp))((variable? exp) (%var exp))((lambda? exp)(%lambda (lambda-variable exp)
(D (lambda-body exp))))((if? exp)(%if (D (if-condition exp))(D (if-consequent exp))(D (if-alternative exp))))((+? exp)(%+ (D (op-arg1 exp))(D (op-arg2 exp))))((*? exp)(%* (D (op-arg1 exp))(D (op-arg2 exp))))(else(%call (D (call-operator exp))(D (call-operand exp))))))

Figure 1.7: Map from syntax to semantics
diate subexpressions. The original implementation does not preclude the possibility
that the meaning of an expression could depend on the syntax of its subexpressions.
Figures 1.1 { 1.4 and gure 1.6 implement the same interface ( gure 1.5) using very
dierent base types. The former uses expressions, while the latter uses denotations.
As shown in gure 1.7, we can de ne a map from expressions to denotations, that is,from syntax to semantics. For example, (* 2 3) goes to (%* (%num 2) (%num 3)).
The denotational approach to interpreters originates with GTWW77]. This paper
shows that the expression implementation is initial in the category of implementations of an ADT interface (see section 2.1.4). A consequence is that all syntaxes are
isomorphic, and hence, from a mathematical point of view, syntax doesn't matter.
The presentation of languages as ADTs shows that, contrary to ASS85] or even
Wad92], there is no real dierence between \metalinguistic" abstraction and data
abstraction. New syntax (even abstract syntax) is not necessary for new languages.

15
In essence, every ADT forms a new language, and vice-versa. Of course, we cannot
have language without syntax in fact, we reuse Scheme's syntax. For example, theexpression(%+ (%num 1) (%num 2))

has meaning in Scheme (directly) and in the interpreted language (using compute).
With an extensible parser, we could make the interpreted language more readable.
Finally, observe that the denotational style can be used in languages other than
Scheme. With a little more work, we could implement the language ADT in C, andthe result would be equally usable.

1.3 Monolithic interpreters
In this section, we examine the usual monolithic style of writing interpreters andshow that it is non-modular. Monolithic means that a program is not textuallydivided into modules. Non-modular means that a local conceptual change requires a
global textual change. Hence, monolithic is a syntactic property, while non-modular
is a semantic property.
To see an example of non-modularity, we extend the language presented above toinclude stores. We add three new operations:%begin%fetch%store: Exp  Exp: Loc: Loc  Exp

! Exp
! Exp
! Exp

The intuitive meanings of these operations are that %begin threads a store throughtwo expressions in sequence, %fetch reads a value from the store, and %store writes avalue into the store. We could de ne %begin using %let but, since they are operationsin the same ADT, I prefer to give them equal status.
Figures 1.8 and 1.9 show a monolithic denotational implementation of the extended language. The store ADT, shown in gure 1.10, is almost identical to theenvironment ADT. The intuitive meaning of the base semantics

16
 Den Proc= Env ! Sto ! Val  Sto= Val ! Sto ! Val  Sto(define (((%num n) env) sto)(pair n sto))(define (((%var name) env) sto)(pair (env-lookup name env) sto))(define (((%lambda name den) env) sto)(pair (lambda (val) (den (env-extend env name val)))sto))(define (((%call d1 d2) env) sto)(with-pair ((d1 env) sto)(lambda (v1 s1)(with-pair ((d2 env) s1)(lambda (v2 s2)((v1 v2) s2))))))(define (((%if d1 d2 d3) env) sto)(with-pair ((d1 env) sto)(lambda (v1 s1)(if v1((d2 env) s1)((d3 env) s1)))))

Figure 1.8: Monolithic interpreter, part 1
Den = Env ! Sto ! Val  Sto

is that an expression is interpreted relative to an environment and a store. For
example, to evaluate (%fetch 'a), we need to know what is stored in location a. In
addition to returning a value, a denotation also returns an updated store.
Even though we have added only three new language constructs, the implementations of the other constructs change drastically. For instance, although numbers havenothing to do with stores, we are forced to write

17(define ((((make-op op) d1 d2) env) sto)(with-pair ((d1 env) sto)(lambda (v1 s1)(with-pair ((d2 env) s1)(lambda (v2 s2)(pair (op v1 v2) s2))))))(define %+ (make-op +))(define %* (make-op *))(define (((%begin d1 d2) env) sto)((d2 env) (right ((d1 env) sto))))(define (((%fetch loc) env) sto)(pair (store-fetch loc sto) sto))(define (((%store loc den) env) sto)(with-pair ((den env) sto)(lambda (val sto)(pair 'unit (store-store loc val sto)))))(define (with-pair p k)(k (left p) (right p)))Figure 1.9: Monolithic interpreter, part 2(define (empty-store) '())
(define (store-fetch loc sto)(let ((entry (assq loc sto)))(if entry(error "Empty location: " loc)
(right entry))))(define (store-store loc val sto)(pair (pair loc val) sto))

Figure 1.10: Store ADT

18(define (((%num n) env) sto)(pair n sto))in place of(define ((%num n) env)n)

Thus we have an instance of non-modularity: a conceptually local change requires a
textually global change.

1.4 Modular interpreters
Modular programs have several advantages over monolithic programs:

 They are easier to understand.
 They are easier to reason about.
 They are easier to extend and modify.
In this section, we describe two modular interpreters. We begin by examining theinterpreter constructed in the last section. The basic semantics is
Den = Env ! Sto ! Val  Sto

In this type, we distinguish three distinct \levels":

E = Env ! Sto ! Val  Sto
S = Sto ! Val  Sto
V = ValModularity is possible because most language constructs operate primarily at a single
level. For example, %var operates on environments, %+ operates on values, and %store
operates on stores.

19
There are two methods for building a modular interpreter, which we describe byanalogy with building a house. In both methods, we build a oor at a time, startingfrom the bottom. However, in the rst, we move in our belongings (rugs, furniture,china, paintings, books) after we nish each oor. In the second, we wait until thehouse is complete before moving in. It's not surprising that the second method works
better.
In the rst method, we start with the value level and constructs such as %+. Then
we add the stores level and more constructs such as %fetch. We also lift the value
constructs up to the stores level (the interesting part). Then we add the environments
level and constructs such as %call. We also lift the value and store constructs up to
the environments level.
In the second method, we de ne operators for lifting values and functions between
all pairs of levels. For example, unitVE lifts from values to environments. We cande ne these operators in stages, but it is easier to de ne them all at once. Then we
use them to de ne each language construct in a single step, without lifting it throughseveral levels.
In both interpreters, we use monads to relate pairs of levels. A monad is a triple(T , unit, bind) of a type constructor and two polymorphic operators
unit
bind

: A ! T (A): T (B )  (A ! T (B )) ! T (B )The operators are required to obey several identities, as discussed in section 2.2. Twotypes A and B are related by a monad (T , unit, bind) if B = T (A). Unit lifts values
from A to B , and bind lifts functions of type A ! B to functions of type B ! B .
We can use bind to lift functions of other types also.
Let's examine what lifting means. Suppose that we have a function square: Num ! Num and we want to de ne a function square-list : List (Num ) !
List (Num ) that squares each number in a list. Given the list monad

20


T (A) = List (A)(define (unit a)(list a))(define (bind tb f)(flatten (map f tb)))

we can de ne square-list as(define (square-list l)(bind l (lambda (n) (unit (square n)))))

We can perform this lifting using the standard Scheme map function, but monads canlift functions that map (and its generalizations) cannot, as shown in section 2.2.3. We
present a formal de nition of lifting in section 3.1.

1.4.1 Lifting interpreter
This section presents a modular interpreter built using lifting. Since strati cation
is simpler and more powerful, it may be better to skip to the next section on rst
reading.
The interpreter is shown in gures 1.11 { 1.14. The rst gure shows a set of lifting
operators. These accept a monad relating levels A and B and a function de ned on A.
They return a function de ned on B . Functions may accept parameter types (written
X ), that are untouched by the lifting process. The parameters always come before
the actual arguments. The operator lift-pN-aM lifts a function of N parameters andM arguments. For example, lift-p1-a2 takes functionsf: X AA ! A

f0:X B B ! B

to lifted functions

The lifting operators assume that all functions return values of type A.

21(define ((lift-p1-a0 unit bind op) p1)(unit (op p1)))(define ((lift-p0-a1 unit bind op) d1)(bind d1
(lambda (v1)(unit (op v1)))))(define ((lift-p0-a2 unit bind op) d1 d2)(bind d1
(lambda (v1)(bind d2
(lambda (v2)(unit (op v1 v2)))))))(define ((lift-p1-a1 unit bind op) p1 d1)(bind d1
(lambda (v1)(unit (op p1 v1)))))(define ((lift-if unit bind op) d1 d2 d3)(bind d1
(lambda (v1)
(op v1 d2 d3))))Figure 1.11: Lifting operators
The second gure shows the values level and the constructs de ned on it. The
third gure uses the lifting operators and the stores monad to lift these operators to
the level of stores. It also de nes several new operators. The fourth gure does thesame for environments. Using appropriate laws for reasoning about Scheme programs(essentially call-by-value lambda calculus), we can show that the nal constructs areoperationally equivalent to the monolithic de nitions of gure 1.8.
Although the code for this interpreter is somewhat long, it is fairly modular. For
example, the de nitions of %num, %+, and %* do not involve environments or stores,

22


V = V al(define computeV id)(define %numV id)(define %+V +)(define %*V *)(define (%ifV d1 d2 d3)(if d1 d2 d3))

Figure 1.12: Value level %fetch and %store do not involve environments, and %var, %lambda, and %call do not involve stores.
We obtain modularity by lifting operators in a canonical way using unit andbind. Canonical means that operators with identical types have identical liftings. An
exception is %if, which needs special treatment. Even in this case, the lifting of %if
is uniform for all levels.
A more serious lack of modularity occurs when de ning %var, %lambda, and %call.
Here we use unitS and bindS, which were intended solely for the stores level. Also, we
assume that environments contain values from the values level. Since the environment
constructs interact with multiple levels, we say that they are non-local.

1.4.2 Stratied interpreter
The second interpreter is much simpler than the rst. We de ne all language
constructs using ve operators that relate levels in pairs:

23


S = Sto ! V  Sto

 Store monad(define (unitS v)(lambda (sto)(pair v sto)))(define (bindS s f)(lambda (sto)(let ((v*sto (s sto)))(let ((v (left v*sto))(sto (right v*sto)))((f v) sto)))))
 Lifted operators(define (computeS den)(computeV (left (den (empty-store)))))(define %numS(define %+S(define %*S(lift-p1-a0 unitS bindS %numV))(lift-p0-a2 unitS bindS %+V))(lift-p0-a2 unitS bindS %*V))(define %ifS (lift-if unitS bindS %ifV)) New operators(define ((%fetchS loc) sto)(pair (store-fetch loc sto) sto))(define ((%storeS loc den) sto)(let ((v*s (den sto)))(let ((v (left v*s))(s (right v*s)))(pair 'unit(store-store loc v s)))))(define ((%beginS d1 d2) sto)(d2 (right (d1 sto))))Figure 1.13: Store level

24

E=

!S
=V !S


Env
 Proc

 Environment monad(define (unitE s)(lambda (env) s))(define (bindE e f)(lambda (env)((f (e env)) env)))
 Lifted operators(define (compute den)(computeS (den (empty-env))))(define %num
(lift-p1-a0 unitE bindE %numS))(define %+(lift-p0-a2 unitE bindE %+S))(define %*(lift-p0-a2 unitE bindE %*S))(define %if(lift-if unitE bindE %ifS))(define %fetch (lift-p1-a0 unitE bindE %fetchS))(define %store (lift-p1-a1 unitE bindE %storeS))(define %begin (lift-p0-a2 unitE bindE %beginS))
 New operators(define ((%var name) env)
(unitS (env-lookup name env)))(define ((%lambda name den) env)
(unitS(lambda (val)(den (env-extend name val env)))))(define ((%call d1 d2) env)
(bindS (d1 env)
(lambda (v1)(bindS (d2 env)
(lambda (v2) (v1 v2))))))

Figure 1.14: Environment level

25
:S !E
:V !S
:V !E
: E  (S ! E ) ! E: E  (V ! E ) ! E
We have left out bindVS since we don't need it. These operators form an abstract
data type of computations, from which we can build the usual language ADT. We
could alternatively call it an ADT of denotations, but Moggi's work on monads setsa precedent for \computations", although we have altered his meaning somewhat.
Peter Mosses was the rst author to describe an ADT abstracting the basic semantics of a language Mos92]. What is new here is strati cation, which has several
advantages:
unitSE
unitVS
unitVE
bindSEbindVE We can de ne non-local language constructs more naturally.
 We can understand computations and language constructs via the structurethat strati cation provides.

 We can build strati ed computation ADTs automatically from component modules.

We return to this approach in chapter 4.
Figure 1.15 shows the computation ADT for this semantics, and gures 1.16 and1.17 show the language ADT built from it. Once again, this interpreter is observationally equivalent to the original monolithic interpreter. It is also somewhat nonmodular speci cally, all constructs assume

 There are no levels above E .
 Level S is immediately below E .
 Level V is immediately below S .
Section 4.3 solves these modularity problems in the context of automatically generated
interpreters by giving each level several names.

26




E = Env ! S
S = Sto ! V  Sto
V = V al(define ((unitSE s) env)s)
(define ((unitVS v) sto)(pair v sto))(define (((unitVE v) env) sto)(pair v sto))(define ((bindSE t f) env)((f (t env)) env))(define (((bindVE t f) env) sto)(let ((p ((t env) sto)))(let ((v (left p))(s (right p)))(((f v) env) s))))Figure 1.15: Level-negotiating operators

1.5 Examples
The examples in this section show Semantic Lego's input / output behavior the
next two chapters explain the mechanisms behind it. We consider

 A full-featured, Scheme-like language, Three interactions between nondeterminism and continuations, Lamping's uni ed system of parametrization, and A parallel language modeled using resumptions.

27

E=
S=
V=

!S
! V  Sto
=V !S


Env

Sto

Val
 Proc(define (%num v)(unitVE v))(define ((%var name) env)
(unitVS (env-lookup env name)))(define ((%lambda name den) env)
(unitVS(lambda (val)(den (env-extend env name val)))))(define (%call d1 d2)(bindVE d1(lambda (v1)(bindVE d2(lambda (v2)(unitSE (v1 v2)))))))(define (%if d1 d2 d3)(bindVE d1(lambda (v1)
(if v1 d2 d3))))Figure 1.16: Modular interpreter, part 1

1.5.1 A Scheme-like language
We construct an interpreter for a language with environments, call-by-value procedures, stores, continuations, nondeterminism, and errors. Figure 1.18 shows thecomplete language speci cation, the basic semantics, and two example expressions.
SL automatically generates descriptions of the basic semantics in pre x form.
We build an interpreter in two steps. In essence, SL automates the manual methods used to build the strati ed interpreter just shown. First, we de ne a computation

28(define ((make-op op) d1 d2)(bindVE d1(lambda (v1)(bindVE d2(lambda (v2)(unitVE (op v1 v2)))))))(define %+ (make-op +))(define %* (make-op *))(define (%begin d1 d2)(bindVE d1(lambda (v1)d2)))
(define (%fetch loc)
(unitSE(lambda (sto)(pair (store-fetch loc sto) sto))))(define (%store loc den)(bindVE den(lambda (val)(unitSE(lambda (sto)(pair 'unit (store-store loc val sto)))))))

Figure 1.17: Modular interpreter, part 2
ADT using make-computations, which accepts a list of semantic modules. The resulting ADT is just a collection of appropriately named unit and bind operators.
Second, we load several les of language constructs. These de ne the language
ADT using operators extracted from the computation ADT. These de nitions are
similar to those of the last section. Constructs may be de ned over any computation
ADT that includes the appropriate semantic modules. For example, the %amb construct requires the nondeterminism module. In general, the same construct de nition
yields dierent semantics when de ned over dierent computation ADTs.

29
 Computation ADT(define computations(make-computations
cbv-environments stores continuations nondeterminism errors))
 Language ADT(load "error-exceptions" "numbers" "booleans" "procedures" "amb""environments" "while" "numeric-predicates" "stores" "callcc")
 Basic semantics(show-computations)(-> Env(-> Sto(let A0 (* Val Sto)(let A1 (+ (List A0) Err)(-> (-> A0 A1) A1))))))

 Sample expressions(compute(%call (%lambda 'x (%+ (%var 'x) (%var 'x)))(%amb (%num 1) (%num 2))))(2 4)
 would be (2 3 3 4) in call-by-name)(compute(%begin(%store 'n (%amb (%num 4) (%num 5)))(%store 'r (%num 1))(%call/cc (%lambda 'exit(%while (%true) (%begin(%if (%zero? (%fetch 'n))(%call (%var 'exit) (%fetch 'r))(%unit))(%store 'r (%* (%fetch 'r) (%fetch 'n)))(%store 'n (%- (%fetch 'n) (%num 1)))))))))(24 120))

Figure 1.18: Example speci cation and expressions

30(define %let
(let ((unitE (get-unit 'envs 'top))(bindE (get-bind 'envs 'top))(bindV (get-bind 'env-values 'top)))(lambda (name c1 c2)(bindV c1(lambda (v1)(bindE c2(lambda (e2)(unitE(lambda (env)(e2 (env-extend env name v1)))))))))))

Figure 1.19: %let source de nition
A typical construct is %let, whose source de nition (from the environments le)is shown in gure 1.19. We have not yet described enough of SL to explain thisde nition in detail, but its form should be clear. Appendix B.2 shows the de nitionof each construct presently available in SL.
Although Scheme procedures are usually opaque, MIT Scheme allows us to reify
them as abstract syntax. We then apply a program simpli er that performs inlining and  and  reduction. By inlining the operators of the computation ADT andsimplifying, we automatically generate denotational-style de nitions of language constructs.
The result of simplifying %let in the context of the speci ed computation ADT,
shown in gure 1.20, is exactly what we would have written by hand. The whole pointof SL is that the source de nition of %let did not mention stores or continuations,
yet they were introduced properly and automatically.

1.5.2 Nondeterminism and continuations
In this section, we use SL to explore the interaction between nondeterminism andcontinuations. We use three dierent computation ADTs but leave the de nitions

31(lambda (name c1 c2)(lambda (env)(lambda (sto)(lambda (k)(((c1 env) sto)(lambda (a)
 Val
Sto
(((c2 (env-extend env name (left a)))(right a)) k)))))))



Figure 1.20: %let de nition simpli ed(define %amb
(let ((unit (get-unit 'lists 'top))(bind (get-bind 'lists 'top)))(lambda (x y)(bind x(lambda (lx)(bind y(lambda (ly)(unit (append lx ly)))))))))

Figure 1.21: %amb source de nitionof all language constructs unchanged. For reference, gure 1.21 gives the sourcede nition of %amb. For each semantics, we show the modules forming the computation
ADT, the basic semantics, the simpli ed version of %amb, and the evaluation of an
example program.
In the rst semantics ( gure 1.22), the subexpressions of %amb are evaluated withlist as a continuation. The results are appended and returned. In the example, thelist continuation is replaced by a continuation that adds one, hence the result 51.
In the second semantics ( gure 1.23), we replace continuations with continuations2.
These modules dier only in their treatment of operators on continuation answers.
The continuations transformer passes down an identity continuation, applies theoperator to the results, and then applies the original continuation in the appropriate

32
way. Continuations2 passes the original continuation down directly and applies theoperator to the results. The evaluation of the example in this semantics is clear.
In the third semantics ( gure 1.24), we compose the continuations and nondeterminism
modules in the opposite order. Here, continuations accept lists of values, rather thanjust values. %amb takes two lists, appends them, and continues with the result. In
the example, invoking the captured continuation aborts this process and returns 4
directly. Hence, the expression has only one value in contrast to the other two semantics. Of the semantics presented here, this is the only one that Steele's system
can generate Ste94]. Incidentally, replacing continuations with continuations2
leaves %amb unchanged.

1.5.3 Unied system of parametrization
In this section, we use SL to realize John Lamping's \Uni ed System of Parametrization" Lam88]. Lamping describes a semantics in which expressions areparametrized over variables that (recursively) denote expressions. This recursion
models a substitution in which substituted terms can contain variables. The language
also includes call-by-name static environments hence the basic semantics is
Den = Env ! EEnv ! Val

where both Env and EEnv contain EEnv ! Val . Figure 1.25 shows the SL language speci cation and the semantics of %evar and %elet, which are used to form
expressions. The line marked *** is especially interesting. Figure 1.26 shows several
examples.

1.5.4 Resumptions
Resumptions are a denotational model of interruptable execution sequences. The
basic structure of a resumption semantics is
Den = x (X ) T (Val + X )33 Computation ADT(define computations(make-computations environments continuations nondeterminism))
 Basic semantics(-> Env (let A0 (List Ans) (-> (-> Val A0) A0))) Simpli ed %amb
(lambda (x y)(lambda (env)(lambda (k)(reduce append ()(map k (append ((x env) list) ((y env) list)))))))
 Example(compute(%+ (%num 1)(%call/cc(%lambda 'k(%* (%num 10)(%amb (%num 3) (%call (%var 'k) (%num 4))))))))) (31 51)
Figure 1.22: %amb version 1
where T is a type constructor describing other features present in the language.
This construction means that a computation either terminates, producing a value,or pauses, producing a computation with which to continue. The typical use of resumptions is to interleave several computations by executing one until it pauses, thenexecuting the next, etcetera.
The standard parallel semantics, described in Sch86] has

T (A) = Sto ! List (A  Sto )34
 Computation ADT(define computations(make-computations environments continuations2 nondeterminism))
 Basic semantics(-> Env (let A0 (List Ans) (-> (-> Val A0) A0))) Simpli ed %amb
(lambda (x y)(lambda (env)(lambda (k)(append ((x env) k) ((y env) k)))))
 Example(compute(%+ (%num 1)(%call/cc(%lambda 'k(%* (%num 10)(%amb (%num 3) (%call (%var 'k) (%num 4))))))))) (31 5)Figure 1.23: %amb version 2
so that computations accept and return stores and can fork into multiple computations. Thus the complete type of denotations is
Den = x (X ) Sto ! List ((Val + X )  Sto )Figure 1.27 shows the SL speci cation for this language, along with several examples.
An expression evaluates to a list of values, one for each possible order of execution.
The de nition of %par appears in appendix B.2, gure B.27 we could show its expansion, but it is not especially enlightening.

35

 Computation ADT(define computations(make-computations environments nondeterminism continuations))
 Basic semantics(-> Env (let A0 (List Ans) (-> (-> (List Val) A0) A0))) Simpli ed %amb
(lambda (x y)(lambda (env)(lambda (k)((x env)(lambda (a)((y env)(lambda (a0)(k (append a a0)))))))))
 Example(compute(%+ (%num 1)(%call/cc(%lambda 'k(%* (%num 10)(%amb (%num 3) (%call (%var 'k) (%num 4))))))))) (5)Figure 1.24: %amb version 3

36
 Computation and language ADTs
(define computations(make-computations cbn-environments exp-environments))(load "error-values" "numbers" "booleans" "numeric-predicates""environments" "exp-environments")
 Simpli ed %evar

and %elet(lambda (name)(lambda (env)(lambda (eenv)(if (env-lookup eenv name)((right (env-lookup eenv name)) eenv)(in 'errors (unbound-error name))))))

 ***(lambda (name c1 c2)(lambda (env)(lambda (eenv)((c2 env) (env-extend eenv name (c1 env))))))

Figure 1.25: Uni ed system of parametrization(compute(%let 'f (%* (%evar 'x) (%evar 'x))(%+ (%elet 'x (%num 3) (%var 'f))(%elet 'x (%num 4) (%var 'f)))))
25)(compute(%let 'g (%+ (%evar 'a) (%evar 'a))(%let 'f (%elet 'a (%* (%evar 'x) (%evar 'x))(%var 'g))(%elet 'x (%num 3) (%var 'f)))))
18)

Figure 1.26: Uni ed parametrization examples

37
 Computation and language ADTs
(define computations(make-computations resumptions stores lists))(load "error-values" "numbers" "booleans" "begin" "while""products" "numeric-predicates" "amb" "stores" "resumptions")
 Examples(compute(%par (%num 1) (%num 2) (%num 3)))
(1 2 1 3 2 3))(compute(%seq(%store 'x (%unit))(%par(%store 'x (%pair (%num 3) (%fetch 'x)))(%store 'x (%pair (%num 2) (%fetch 'x)))(%store 'x (%pair (%num 1) (%fetch 'x))))(%fetch 'x)))((pair 3 (pair 2 (pair 1 unit)))(pair 2 (pair 3 (pair 1 unit)))(pair 3 (pair 1 (pair 2 unit)))(pair 1 (pair 3 (pair 2 unit)))(pair 2 (pair 1 (pair 3 unit)))(pair 1 (pair 2 (pair 3 unit)))))(compute(%seq(%store 'x (%num 1))(%store 'go (%true))(%par(%store 'go (%false))(%while (%and (%fetch 'go)(%< (%fetch 'x) (%num 7)))(%pause (%store 'x (%1+ (%fetch 'x))))))(%fetch 'x)))(2 3 4 5 6 7 7 1))

Figure 1.27: Parallel language using resumptions

Chapter 2
MonadsIn this chapter, we rst present some basic category theory, then discuss monads,
maps between monads, monad composition, and monad transformation. This may
sound like \everything you always wanted to know about monads", but in reality itbarely scratches the surface. See BW85, Mog89a] for more information.
Monads may be a \hot topic" in the 1990's functional programming community,
but the real \monad explosion" occurred in the category theory / algebraic topology
community during the 1960's, when they were rst invented. Although I consider
myself a fairly good \monad hacker" by 1990's standards, I have to admit that I'm
not even on the 1960's chart. Even so, I nd hard to hear computer scientists ask,
\Monads { aren't those about state?". That's like asking, \Algebra { isn't that about
1 + 1 = 2?".

2.1 Basic category theory
In this section, we de ne the basic notions of category theory, discuss the relationship between category theory and functional programming, and mention somereferences.

38

39

2.1.1 Categories
Categories abstract the composition of typed functions. A category is a set of objects (these are the types), a set of arrows (these are the functions), and a composition
operator on the arrows. Each arrow points from one object (its domain) to another(its codomain). If f : A ! B and g : B ! C are two arrows then g  f : A ! C istheir composition. There is a distinguished identity arrow from each object to itself.
Composition must be associative with the identity arrows as left and right identities.
The basic category that we use depends on whether we are doing semantics orfunctional programming. In semantics, we use a suitable domain theory (see Gun92]).
In functional programming, we use the types and functions of our language, in thiscase, Scheme CR91]. Scheme has no explicit types, so we have to imagine themourselves.
In a category, composition is primary, rather than application. In functional
programming, it's the reverse, unless we program in a combinator language. Thischange in point of view causes few problems in practice we use whichever is mostconvenient.

2.1.2 Functors
In category theory, whenever we de ne a class of objects, we also de ne the appropriate maps between them, thus making them into a category. For this reason, we
now consider maps between categories.
A function T between categories C and D is a map from C 's objects to D's objects.
An endofunction is a function from a category to itself. In our case, an endofunction
is a type constructor it builds one type from another. For example, T (A) = List (A)builds lists of any type we like. The other type constructors we use are function space(!), products (), and sums (+).
Functions are insucient as maps between categories because they have no action
on arrows. We de ne a functor T : C ! D to be a function, also called T , along with

40
an function mapT from C 's arrows to D's arrows such that mapT: (A ! B ) ! (T (A) ! T (B ))(mapT id)
= id
(mapT (oC g f)) = (oD (mapT g) (mapT f))

An endofunctor is a functor from a category to itself, so that we need only one
composition operator. For example, the ordinary map function on lists makes T (A) =List (A) into an endofunctor. Functors are the appropriate class of maps between
categories, since they respect identities and composition structure. Other functors
are the pairing functor

T (A) = A  A(define ((map f) ta)(pair (f (left ta)) (f (right ta))))and the environment functor, which parametrizes a type by an environment:

T (A) = Env ! A(define (((map f) ta) env)
(f (ta env)))

2.1.3 Natural transformations
A natural transformation from a functor S to a functor T is a polymorphic functionsigma: S (A) ! T (A)such that(o sigma (mapS f)) = (o (mapT f) sigma): S (A) ! T (B )for all f : A ! B . It is easy to remember this law as \sigma commutes with map".
Examples include

41
reverseflatten
list
left
diag

: List (A) ! List (A): List (List (A)) ! List (A): A ! List (A):AA!A:A!AA

where list is natural from Id to List, left is natural from pairing to Id, and diagis natural from Id to pairing.
In categorical terms, a natural transformation is a map from objects to arrows.
Given an object A, we obtain an arrow sigmaA: S (A) ! T (A). In other words, we obtain a family of functions, indexed by type. The naturality condition above structures
our choice of arrows we cannot pick arbitrarily. This yields parametric polymorphism
rather than ad-hoc polymorphism. For further information, see Wad89].

2.1.4 Initiality
An object in a category is initial if there is a unique arrow from it to each objectof the category. A object is terminal is there is a unique arrow to it from each object.
Initial and terminal objects are unique up to isomorphism if they exist. Two objects
A B of a category are isomorphic if there exist arrows f : A ! B and g : B ! A
such that g  f = Id B and f  g = Id A .
For example, in the category of sets and total functions, the empty set is initialand any one-element set is terminal. Notice that there are many one-element sets, allof which are isomorphic. Initiality will not see much use in this thesis, although it isperhaps the fundamental concept of category theory.

2.1.5 Duality

Given a category C, we can form its dual C op by reversing the direction of eacharrow and the order of composition. Needless to say, this operation is quite dicultin ordinary functional programming. If an object is initial in C, it is terminal in
Cop, and vice-versa. Hence we say that initial and terminal are dual concepts. Other

42
well-known dual concepts are products / sums and injective / surjective. In general,
we can form the dual of any concept formulated solely in category-theoretic terms.
In his brilliant master's thesis Fil89], Filinski shows that values and continuations
are dual. Although it is dicult to develop an intuition for his language, his thesis
contains many surprising insights.

2.1.6 Category theory and functional programming
It is important to remember that, at least for the moment, mathematics andprogramming are two dierent activities. The main problem is that current languages
provide no automated support for representing and verifying properties of programs.
In this thesis, we embed category theory within functional programming in aparticular way: objects are types, and arrows are functions. Other embeddings are
possible for example, see RB90], which represents objects as values. Their approachis less straightforward, but more exible.
Our choice of embedding has several problems: Current languages have weak, non-existent, or implicit type systems (see section

A.1). In category theory, we can form categories with any kind of objects atall.

 It may not be easy to represent categorical composition as functional composition. Also, we cannot represent uncomputable compositions.

The clearest and most comprehensive treatment of category theory and functional
programming in this embedding is Spi93] hopefully, Spivey will soon publish thesehandwritten notes in electronic or book form. A much-abbreviated version appears
as Spi89].

2.1.7 References
General references on category theory for computer science are Pie91] and BW90].
The latter contains many examples and applications and is easy despite its length.

43
Category theory is not terribly hard to learn, because its rich descriptive content
encourages the reader to acquire concepts one at a time, relating each to alreadyunderstood notions from other elds.
Category theory may be considered part of abstract algebra. MacLane andBirkho's larger book MB88] is a wonderful introduction to algebra, not only because
it presents category theory near the end, but because it applies category-theoretic insight throughout.

2.2 Monads
In this section, we present two formulations of monads and discuss the intuitions
behind them. Monads are functors with additional structure, in the same way thatfunctors are functions with additional structure.

2.2.1 First formulation
A monad is a triple1 (T , unit, join) of an endofunctor and two natural transformations
unit
join

: A ! T (A): T (T (A)) ! T (A)is natural from the identity to T and maps values into T . For example, unit
for the list monad is list. Unit is not required to be injective, although it actually
is in most applications. Join is natural from T  T to T and attens multiple T 's intoa single T . Join for the list monad is flatten.
Unit and join for the environment monad T (A) = Env ! A are
Unit(define ((unit a) env)a)(define ((join tta) env)((tta env) env))
1

Monads are also called triples.

44
Monad
Action T (A) =IdentityA
Lists
List (A)
Lifting
1!A
Environments Env ! A
StoresSto ! A  Sto
Exceptions
A+X
Monoids
AM
Continuations (A ! Ans ) ! Ans
Resumptions x (X ) (A + X )Table 2.1: Monad type constructors
Unitand join must satisfy the additional properties(o join unit)= id: T (A) ! T (A)(o join (map unit)) = id
: T (A) ! T (A)(o join (map join)) = (o join join) : T (T (T (A))) ! T (A)This formulation presents monads as modi ed monoids Mac71] (whence the name),
where unit is the identity and join is the monoid operator. The above laws are left
and right identity and associativity.
Table 2.1 shows the type constructors for some common monads used in semantics. We describe their unit and join operators in the next section (via the second
formulation).

2.2.2 Second formulation
We can also describe a monad as a triple (T , unit, bind) where T is an endofunction, unit is a family of arrows that is not necessarily required to be natural, andbind is a map between sets of arrows:
unit : A ! T (A)bind : (A ! T (B )) ! (T (A) ! T (B ))Unit functions exactly as before. Just as map takes functions from A ! B into
T (A) ! T (B ), bind takes functions of the more general form A ! T (B ) into T (A) !
T (B ). Unit and bind obey several properties:

45
 f
 g

: A ! T (B ): B ! T (C )(bind unit)= id(o (bind f) unit)= f(o (bind g) (bind f)) = (bind (o (bind g) f)): T (A) ! T (A): A ! T (B ): T (A) ! T (C )To show the equivalence of the two monad formulations (bind versus map and join),
we can write(define ((map f) ta) (bind ta (o unit f)))(define (join tta)

(bind tta id))(define (bind ta f)(join ((map f) ta)))

Proving the two sets of laws equivalent is easy.
The second formulation is easier to understand if we rephrase it in terms of theKleisli composition oT on the space of functions A ! T (B ): oT : (B ! T (C ))  (A ! T (B )) ! (A ! T (C ))(define ((oT g f) a)(bind (f a) g))

Then the laws become(oT unit f)= f(oT f unit)= f(oT h (oT g f)) = (oT (oT h g) f)

In other words, oT is associative and has unit as left and right identity. Thus, we canform a Kleisli category whose objects are types and whose arrows are functions of theform A ! T (B ), with oT as composition. Like all systems of functional combinators,
Kleisli composition is useful for stating and deriving laws but is unwieldy for writing
programs.
Figures 2.1 and 2.2 de ne unit and bind for the type constructors shown in table2.1. These gures use an applicative (rather than compositional) version of bindobtained by uncurrying and reversing arguments:bind: T (A)  (A ! T (B )) ! T (B )46

 Identity:

T (A) = A

(define (unit a)a)(define (bind ta f)(f ta))
 Lists:

T (A) = List (A)(define (unit a)(list a))(define (bind ta f)(reduce append '() (map f ta))) Environments:

T (A) = Env ! A(define (unit a)(lambda (env) a))(define (bind ta f)(lambda (env)((f (ta env)) env)))
 Stores:

T (A) = Sto ! A  Sto(define (unit a)(lambda (sto) (pair a sto)))(define (bind ta f)(lambda (sto)(let ((a*s (ta sto)))(let ((a (left a*s))(s (right a*s)))((f a) s)))))

Figure 2.1: Example monads, part 1

47
 Exceptions:

T (A) = A + X(define (unit a)(in-left a))(define (bind ta f)(sum-case ta(lambda (a) (f a))(lambda (x) (in-right x)))) Monoids:

T (A) = A  M(define (unit a)(pair a monoid-unit))(define (bind ta f)(let ((a1 (left ta))(m1 (right ta)))(let ((a*m (f a1)))(let ((a2 (left a*m))(m2 (right a*m)))(pair a2 (monoid-product m1 m2))))))
 Continuations:

T (A) = (A ! Ans ) ! Ans(define (unit a)(lambda (k) (k a)))(define (bind ta f)(lambda (k) (ta (lambda (a) ((f a) k)))))
 Resumptions:

T (A) = x (X )(A + X )(define (unit a)(in-left a))(define (bind ta f)(sum-case ta(lambda (a) (f a))(lambda (ta) (bind ta f))))Figure 2.2: Example monads, part 2

48

2.2.3 Interpretations
In this section, we give several interpretations of monads. Moggi's model, which
we discuss last, is the one most relevant to this thesis.

Monads resemble monoids
MacLane Mac71] describes monads as a variation on monoids, with unit as theidentity and join as the monoid product. A monoid product (on a type constructor)
has type*:T T !TFor example, consider append on List (A). A monad product has typejoin

:T T !TFor example, consider flatten. That these notions have a common generalization israther odd.

Monads model substitution
Suppose T (A) is a type of arithmetic expressions over a set of variables A:

T (A) = A j T (A) + T (A) j T (A)  T (A)Then unit transforms a variable into an expression, and bind performs substitution.
A substitution is a map A ! T (B ) that gives an expression T (B ) over B for eachvariable of A. Bind takes an expression over A and a substitution and returns an
expression over B .
Join also performs substitution by attening \expressions over expressions". Bind
accomplishes everything that join does, but we never have to see more than one
application of T .

49

Monads model lifting
We can view bind as a generalization of map. The naturality of unit means that
(unit (f a)) = ((map f) (unit a))

In other words, it doesn't matter whether we apply f before unit or (map f) after.
We say that (map f) is a lifting of f through unit. We give a very general de nitionof lifting in chapter 3.
Just as map lifting functions of the form A ! B , we can say that bind lifts
functions of the more general form A ! T (B ), and the rst two monad laws ensure aproperty similar to the above. Bind can also lift functions on products. For example,
we can lift + to act on lists of numbers using the list monad:(define (list+ l1 l2)(bind l1
(lambda (n1)(bind l2
(lambda (n2)(unit (+ n1 n2)))))))

This de nition is not possible using map alone. However, with a map
product: T (A)  T (B ) ! T (A  B )we can write(define (list+ l1 l2)(map (product l1 l2)(lambda (n1*n2)(+ (left n1*n2) (right n1*n2)))))

A purely categorical model of lambda calculus over a monad (see Mog89b]) actuallyrequires a \tensorial strength" similar to product, even when using bind. Thus, someof the power of bind (when compared to map) comes from Scheme, rather than frompure category theory.

50
Monad
A computation exists when it
Lists
Produces a single value
Lifting
Terminates
Environments Is independent of environment
StoresLeaves the store unchanged
Exceptions
Causes no exceptions
Output
Doesn't output anything
Continuations Invokes its continuation exactly once
Resumptions Terminates in one step
Table 2.2: Meaning of existence

Monads model computation
Moggi's insight was that T (A) represents a computation of a value of type A. For
example, a nondeterministic computation produces not just a single value but a set of
possible values. Unit lifts a value to a computation that produces that value (and doesnothing else). Join attens computations of computations into single computations.
Bind composes functions from values to computations.
Moggi also made the following de nition: a computation is a value or exists if it
is in the image of unit, that is, if it equals (unit v) for some value v. Thus, we
can say that a nondeterministic computation exists if it produces only a single value.
Table 2.2 shows the meaning of existence for other monads.
If unit is a way into a monad, we also need a way out. We cannot have a map
from computations to values because we might want to see more than one value orperhaps know what nal store a computation produced. Thus, we augment all ourmonads with a map
compute: T (A)  (A ! Rep) ! Rep

where Rep is a universal representation type designed for users to read. In many
languages, this type would be String, but in Scheme we use lists, numbers, etcetera.
An alternative is

51compute: T (Rep) ! Rep

in which we map a function of type A ! Rep across T (A), then apply compute.
Although this approach is direct, it con icts with the computational analogy, since
T (Rep) is a computation of a representation rather than a computation of a value.
We do not discuss compute in the rest of the thesis, but section B.1 shows its
de nition for each of the monad transformers we use.

Why monads?
Moggi's intuition of \values and computations" does not quite explain why we needjoin in addition to map and unit. In fact, we need it to abstract over computations
using functions.
In a language with a nondeterminism operator amb, modeled by the semantics
Den = Env ! List (Val )consider the program(define (f n)(g (amb n (+ n 1))))(define (g n)(amb n (* n 2)))

The function g, although it accepts values, must return computations, since it uses
amb. The function f must apply g to a computation rather than a value. Thus, weneed a functionapply: (Val ! Comp)  Comp ! Comp

This function is essentially bind.

52

2.3 Monad morphisms
In keeping with the \categorical imperative" that arrows between objects are asimportant as the objects themselves, we de ne arrows between monads. Thus, weform a category of monads and monad morphisms.
Since Kleisli categories were helpful in developing the monad laws, we suppose thatan arrow between monads S and T is a functor K between their Kleisli categories.
K acts as the identity on objects. On arrows, we havemapK

: (A ! S (B )) ! (A ! T (B ))satisfying the functorial properties
 f
 g

: A ! S (B ): B ! S (C )(mapK idS)
= idT
(mapK (oS g f)) = (oT (mapK g) (mapK f))

We can reformulate this de nition in terms of unit, bind, and a natural transformation K : S (A) ! T (A), in which case(K (unitS a))= (unitT a)(K (bindS sa f)) = (bindT (K sa) (o K f))

An example of an arrow between monads is reverse from the list monad to itself:(reverse (list a))= (list a)(reverse (append-map f l)) = (append-map (o reverse f) (reverse l))

An example of a natural transformation from the list monad to itself that is not anarrow between monads is (lambda (l) '()), which fails the rst law.

2.4 Monads don't compose
Given the variety of semantic features that monads oer, it seems that we shouldhave no trouble building all sorts of languages. Unfortunately, monads don't compose.

53




S (A) = EnvS ! A
T (A) = EnvT ! A
ST (A) = EnvS ! EnvT ! A(define ((joinS ssa) envS)((ssa envS) envS))(define ((joinT tta) envT)((tta envT) envT))(define (((joinST ststa) envS) envT)((((ststa envS) envT) envS) envT))

Figure 2.3: Monads don't compose
This may seem odd, since functors do compose. Unit also composes, but join andbind do not.
As an example, let's try to compose two environment monads S and T . Figure
2.3 shows join for the individual monads and for their composition. It is clear byinspection that the latter cannot be de ned from the former, even using unit andmap.
Jones and Duponcheel JD93] give a rigorous proof based on the propositions as
types analogy, showing that the type of joinST is not provable in implicational logic
from the types of the other operators. However, if we think of monads as generalized
monoids, that is, as acting on sequences of S 's and T 's, we realize that unit introduces
an S or T , join attens SS or TT , and map allows us to act anywhere in a sequence.
Is is clear that we cannot reduce STST to ST using these operators, since they neverdecrease the number of S=T boundaries.

2.5 Monads do compose
In the last section, we showed that, given two monads S and T , there is no way toform a monad on ST using only the operators of S and T . There are three equivalent

54
ways around this diculty, via distributive laws, liftings, and compatibility.
A distributive law is a map
swap: TS ! ST

that distributes T over S and obeys several side conditions. Clearly, this map allows
us to reduce arbitrary sequences of S 's and T 's to a single pair.
A lifting of S over T is a monad on the Eilenberg-Moore category of T -algebras,
which we will not discuss. It may also be possible to lift S onto T 's Kleisli category,
although the construction would be less direct. It may also be possible to presentmonad transformers (section 2.6) as liftings of this form.
Finally, we can describe conditions under which ST is compatible with S and T .
There are two formulations of these conditions. The rst, due to Barr BW85] (page315), isST = S  T

map = mapS o mapT(C1) unitST = unitS o unitT = mapS(unitT) o unitS(C2) joinST o mapST(unitS) = mapS(joinT)(C3) joinST o mapS(unitT) = joinS(C4) joinS o mapS(joinS)= joinST o joinS(C5) joinST o mapST(mapS(joinT)) = mapS(joinT) o joinST
Drawn as diagrams, these laws are just triangles and squares, which are suciently
described by their types:(C1) : Id! ST(C2) : STT! ST(C3) : SST! ST(C4) : SSTST ! ST
(C5) : STSTT ! ST
The second formulation, due to Beck Bec69], requires that the two maps
unitS
mapS(unitT): T ! ST
: S ! ST

55
be monad morphisms (see section 2.3) and that the middle unitary law holds:
joinST o mapS(unitT o unitS) = id

: ST ! ST

Distributive laws and liftings were discovered by Beck Bec69]. Both Beck Bec69] andBarr BW85] prove that liftings, distributive laws, and compatibility are equivalent.
Why Barr used a dierent formulation of compatibility is unclear2. Barr studied distributive laws at the same time as Beck (see Beck's paper) perhaps the two sets were
derived independently. It remains to verify that the conditions are indeed equivalent.
Jones and Duponcheel's paper JD93] is entirely about distributive laws but misses
the earlier references. This omission is unsurprising since the relevant section inBW85] occurs late in the book and is titled \distributive laws" rather than \monadcomposition".
Using compatibility, we can develop monad composition as a relation rather thana function. The composition of two monads is thus the set of all monads compatible
with them. The compatibility laws imply that composing a monad T with the identity
yields exactly T and no other monads. I have not been able to show associativity {further conditions may be necessary.
If associativity holds, we can form a relational category whose arrows are monads.
The notion of a relational category is obvious but appears not have been studied before(perhaps it lacks sucient structure to be interesting). A request for references to alarge mailing list of category theorists yielded few replies. One was directly relevant:Martin Wirsing (Munich) mentioned that an (unnamed) student of his is studying
the idea in relation to nondeterminism and that his/her thesis is expected during thesummer of 1995.
Needless to say, the compatibility laws don't yield a method for composing monads. We cannot even verify computationally that three monads are compatible, since
we cannot check equality of functions. For the same reason, we cannot check that
one function is a lifting of another (section 3.1). Nevertheless, the compatibility laws
do constrain possible compositions and allow us to reason about them.
2

Barr graciously replied to my questions but doesn't recall why his conditions are dierent.

56

2.6 Monad transformers
Since monad composition fails to be constructive, we try monad transformation
categorically speaking, if monads aren't arrows, let them be objects. That is, webuild monads from other monads. After motivating the basic concepts, we formalize
our constructions.

2.6.1 Motivation
For example, the environment monad transformer, shown in gure 2.4, adds anenvironment to any monad. We write the environment transformer as

F (T )(A) = Env ! T (A)which indicates that it accepts a monad T and returns a new monad F (T ). The
action of F (T ) on a type A is as shown above.
Applying monad transformers for EnvS and EnvT to the identity monad yields
precisely the monad for both environments, with joinST as shown in gure 2.3. Thus,
we immediately see an example of a construction we could not previously make.
The transformation of join is fairly complex. It accepts an argument
ftfta: Env ! T (Env ! T (A))

and forms a value of type T (T (A)) in order to use joinT. Thus it reduces Env ! T (A)to T (A) inside T (Env ! T (A)) using mapT.
Other monad transformers are listed in table 2.3, one for each monad in tables 2.1
and 2.2. More precisely, applying the X monad transformer to the identity monadyields the X monad, where X is environments, stores, etcetera. Appendix B.1 shows
the de nition of each transformer. As usual, composition of transformers is notcommutative, and we shall make creative use of this fact later.
To illustrate the need for monad transformers further, we model a language with
nondeterminism and state using the type of denotations
Den (A) = Sto ! List (A  Sto )

57



F (T )(A) = Env ! T (A)(define (environment-transformer m)(let ((unitT (monad-unit m))(mapT (monad-map m))(joinT (monad-join m)))(define (unit a)(lambda (env) (unitT a)))(define ((map f) fta)
(lambda (env)((mapT f) (fta env))))(define (join ftfta)(lambda (env)(joinT((mapT (lambda (fta) (fta env)))(ftfta env)))))(make-monad unit map join)))Figure 2.4: Environment monad transformer

Transformer
Action on types F (T )(A) =Identity
T (A)Nondeterminism T (List (A))
Environments Env ! T (A)StoresSto ! T (A  Sto )Exceptions
T (A + X )Monoids
T (A  M )Continuations (A ! T (Ans )) ! T (Ans )Resumptions
x (X ) T (A + X )Table 2.3: Monad transformers

58
Unit

for this type is(define (unit a)(lambda (sto) (list (pair a sto))))but it is clear that it cannot be de ned from(define (unitS a)(lambda (sto) (pair a sto)))(define (unitL a)(list a))In fact, there is no way to build Den (A) by composition. The only monad with type
constructor T (A) = A  Sto has(define (unitT a)(pair a (empty-store)))which is useless. On the other hand, we can easily construct this type by composing
the store and nondeterminism transformers.

2.6.2 Formalization
Since we have already constructed a category of monads, we have several choices
for de ning monad transformers. They could be functions (on objects), functors(with an action map on arrows), premonads (functors with unit), or even monads.
We develop these ideas in sequence and show that monads on the category of monads
are less complex than they sound. Formally, we de ne a monad transformer to bea premonad on the category of monads, since there is at least one case of a usefulmonad transformer (stores) that is not quite a monad in the higher category.
A monad transformer's action on objects is to create a monad F (T ) from a monad
T . Its action on arrows is to send an arrow K : S ! T between monads to an arrow(mapF K) : F (S ) ! F (T ) such that the functorial properties are satis ed. For
example, the action of the list monad transformer on arrows is59F (T )(A) = List (T (A))(define ((mapF K) fta)
(map K fta))

Its action on objects (monads) is more complex and is given in appendix B.1. For
each monad transformer F , we require a natural transformationunitF: T (A) ! F (T )(A)from the identity to F . UnitF allows us to lift values from T (A) in F (T )A.
To lift functions from T to F (T ) we can either use mapF, or, if possible, de ne a
map
bindF

: F (T )(A)  (T (A) ! F (T )(B )) ! F (T )(B )obeying the usual laws. BindF makes F into a monad on the category of monads.
Before we faint from lack of air at these dizzying heights of abstraction, let's takethe environment monad transformer as an example. First we consider its action on
objects (monads):F (T )(A) = Env ! T (A) unitFT bindFT: A ! F (T )(A)
: F (T )(A)  (A ! F (T )(B )) ! F (T )(B )(define (unitFT a)(lambda (env) (unitT a)))(define (bindFT fta f)(lambda (env)(bindT (fta env)
(lambda (a)((f a) env)))))

Next we consider its action on arrows (between monads):

60F (T )(A) = Env ! T (A) mapF: (S (A) ! T (A)) ! (F (S )(A) ! F (T )(A))(define (((mapF K) fsa) env)
(K (fsa env)))

And nally, we consider unitF and bindF:
 F (T )(A) = Env ! T (A) unitF
 bindF: T (A) ! F (T )(A)
: F (T )(A)  (T (A) ! F (T )(B )) ! F (T )(B )(define (unitF ta)(lambda (env) ta))(define (bindF fta f)(lambda (env)((f (fta env)) env)))

This last de nition is in fact identical to that of the usual environment monad (seegure 2.1). UnitF and bindF are thus much simpler than unitFT and bindFT. As wepass to higher levels of abstraction, the de nitions become simpler but their types
become more complex. Essentially, the more polymorphic a function is, the less it
knows about its arguments, so the less it can do (see section 1.1.6). As before, mapF
is unnecessary if we have unitF and bindF.

2.6.3 Classes of monad transformers
Suppose F transforms type constructors. It may not be possible to extend F 's
action to monads. For example, we can extend

F (T )(A) = Env ! T (A)but not

F (T )(A) = T (Env ! A)

We do not give a rigorous proof, but let's try it and see what happens:

61Type Form
Bottom F (T ) = T  U
Top
F (T ) = S  T
Around F (T ) = S  T  U
Table 2.4: Monad transformer classi cation(define (bindFT fta f)(bindT fta(lambda (env->a)...)))(define (bindFT fta f)(unitT(lambda (env)(bindT fta
 ***(lambda (env->a)(env->a env))))))The rst attempt falls at. The second appears more promising, but is badly typed
at the starred line. Similar arguments indicate that we can de ne

F (T )(A) = T (List (A))
but not

F (T )(A) = List (T (A))

These observations naturally lead to a classi cation of monad transformers as top,bottom, or around, as shown in table 2.4. Continuations and resumptions do nott into this classi cation, but table 2.5 classi es the other transformers we havediscussed. Lifting appears twice since there are two dierent lifting transformers.
Note that S and T in bottom and top transformers have monadic structure, since
we can apply the transformer to an identity monad. In around transformers, S  T
has monadic structure. Although we have only one good example each of top andaround transformers, the classi cation will prove useful later, in section 4.2.
The nondeterminism monad transformer should actually use sets, rather thanlists. In fact, \monads" created by list transformer don't obey the associative law

62
Name
Type F (T )(A) = Classi cation
Nondeterminism T (List A)
BottomExceptions
T (A + X )BottomMonoids
T (A  M )BottomLifting1
T (1 ! A)
BottomLifting2
1 ! T (A)Top
Environments Env ! T (A)TopStoresSto ! T (A  Sto) Around
Table 2.5: Classi cation examples
unless the original monad is commutative (see JD93]) however, in our interpreters,
we represent sets as lists and ask the reader to collapse distinctions of order andmultiplicity.

2.6.4 Composition of monad transformers
We can use transformers to build quite complex types. For example, consider alanguage with environments, stores, continuations, nondeterminism, and exceptions.
We compose the transformers as(composeenvironments
storescontinuations
nondeterminism
exceptions))

obtaining

F (T )(A) = Env !

Sto !
(A Sto ! List (Ans + Err )) !
List (Ans + Err ))Chapter 3
Lifting
This chapter shows how to use monad transformers to build interpreters via theimportant notion of lifting. The rst section presents a general de nition of lifting,and the second describes several methods of building interpreters.

3.1 Lifting
In this section, we formalize lifting and show how monads can lift operations withsimple signatures.

3.1.1 Formal lifting
We de ne a language of types t(S ) parametrized by a functor S :t(S ) = A (constants)
j V (variables)
j t  t (pairs)
j t ! t (functions)j S(t) (functors)
The form of this de nition is from LHJ95] a slightly more complex version appearsin Mog89a]. It is also nearly identical to the fundamental de nition in Reynolds'
work on parametricity Wad89].
63

64
For any particular S , t(S ) is still polymorphic, since we allow type variables.
Given two functors S , S and a natural transformation sigma : S ! S , a lifting oftype t through sigma is a map
00L: t(S ) ! t(S )0such that
(L a)
= a
(L v)
= v
(L (pair x y)) = (pair (L x) (L y))((L f) (L x)) = (L (f x))(L s)= (sigma (mapS L s))(constants)(variables)(pairs)(functions)(functors)

Notice that(sigma (mapS L s)) = (mapS' L (sigma s))since sigma is natural. This de nition speci es li ng as a relation, not a function.
In fact, given t and sigma there may be many liftings, one, or none. For example,
suppose we x the following signature, functor, and function:

t(S )
S (A)

=
=
(mapS f a) =id:

S (A) ! A
A
(f a)
t(S )

Then if we specify a functor S and a natural transformation sigma from S to S , wecan enumerate the liftings of id along sigma. First, we try
0



0

S (A) = A  A
0(define ((mapS' f) p)(pair (f (left p)) (f (right p))))(define (sigma a) (pair a a))

Then there are two liftings of id: left and right. The constraint on liftings f is
(f (pair a a)) = a

65which both left and right satisfy. Another choice of S and sigma is0

S (A) = List (A)0(define (mapS' f l) (map f l))(define (sigma a) (list a))

Liftings in this case have type List (A) ! A. But there are no functions of this type,since we wouldn't know where to send the empty list. Vacuously, all of them meetthe lifting constraint(f (list a)) = a

Given a monad T , we lift functions from Id to T through unit. Both cases above
are examples of this form. Given a monad transformer F , we lift functions from T to
F (T ) through unitF. For example, consider append de ned on the list monad:

T (A) = List (A)append : T (A)  T (A) ! T (A)If we lift append through the environment monad transformer
F (T )(A) = Env ! T (A)(define (unitF ta)(lambda (env) ta))

we obtain
 lifted-append: F (T )(A)  F (T )(A) ! F (T )(A)(define (lifted-append fta1 fta2)(lambda (env)(append (fta1 env) (fta2 env))))There are additional naturality conditions on these liftings that we do not discuss(see Mog89a]).

66

3.1.2 Monads and lifting
By now, it should be obvious that monads can de ne liftings. For example, let's
lift a binary operator f : A  B ! C up to F along unit for a monad T . We write(define (F ta tb)(bind ta(lambda (a)(bind tb
(lambda (b)(unit (f a b)))))))

Using the monad laws, we can show that F is a lifting of f according to the previous
section. We need(F (unit a) (unit b)) = (unit (f a b))

Using substitution and the rst monad law twice, we have(F (unit a) (unit b))= (bind (unit a)(lambda (a)(bind (unit b)(lambda (b)(unit (f a b))))))= (bind (unit b)(lambda (b)(unit (f a b))))= (unit (f a b))

It would be interesting to determine the set of signatures liftable using monads. Someuseful operators, such as %callcc, are not apparently liftable.

3.2 Pragmatics
Consider a composition of monad transformers applied to a monad:

67(F1    Fn)(T )From the bottom up, we form a sequence of monads Fn(T ) Fn 1(Fn(T )) : : :. From
the top down, we form a sequence of monad transformers F1 F1  F2 : : :. Naturally,
we can combine these approaches by splitting the sequence of transformers at somepoint, forming the left half top-down and the right half bottom-up, then combining
the two halves by application.
;

3.2.1 Bottom-up
In the bottom-up approach, we begin with a basic monad, usually the identity,
and apply monad transformers to it. As we apply a transformer we Lift existing operators through the the transformer, and Add new operators to the resulting transformed monad.
Thus, we obtain a new monad with not only the existing operators, but several newones as well. In this case, we lift along the unitF operator of the monad transformer. Although we are technically working with monads on the category of monads, Scheme's implicit polymorphism allows us to use ordinary monads for lifting.
For example, we can lift an operator from T (A) to Env ! T (A) using the ordinary
environment monad. Even easier, an operator on T (A) is already an operator on
T (List (A)), with no lifting needed. These short cuts would not be possible in thepolymorphic lambda calculus, where we would have to keep track of types explicitly.
It appears that we always lift operators through monad transformers, rather thanmonads, but this is not quite the case. To de ne operators on monad transformers,
we must often lift values and functions through the monads they transform. For
example, in order to de ne call-by-value variable reference on Env ! T (A), we must
lift values using unitT:

68
 %var Env: Name ! Env ! T (A)= Name ! A(define (%var name)(lambda (env) (unitT (env-lookup env name))))Similarly, to de ne %amb on T (List(A)), we lift append through T . Modulo these
considerations, building a system based on lifting is straightforward.

3.2.2 Top-down
The top-down approach yields a system of extensible interpreters generalizing
Wadler Wad92]. In a sequence F1 F1F2 : : :, we view F1 as an interpreter parametrized
by a monad for example, Wadler's basic interpreter is F (T )(A) = Env ! T (A).
However, instead of supplying a monad, we supply a monad transformer to obtain
another interpreter. In other words, given a parametrized interpreter I and a monadtransformer F , we form another parametrized interpreter I  F . Of course, we mustalso take care to lift operators properly. Steele searched for this approach in Ste94]
but missed passing to higher-order types.

Chapter 4
Stratication
In this chapter, we formally de ne strati ed monads and their transformers anddescribe how SL actually works.

4.1 Stratied monads
Using compatible monads (section 2.5), we can formalize the notion of \levels
related by monads" discussed in chapters 1 and 3.
A level is simply a type constructor (an endofunction on the category). A monadT relates L1 to L2 if L2 = T  L1. We can form categories whose objects are levels
and whose arrows are monads by de ning composition any way we like, subject tothe category laws and the compatibility of composites.
For example, let's form a category of levels and monads for the semantics Den (A) =Env ! Sto ! A  Sto . We have levels

L4(A) = Env ! Sto ! A  Sto
L3(A) = Sto ! A  Sto
L2(A) = A  Sto
L1(A) = A69

70
These are related by monads

T34(A) = Env ! A
T23(A) = Sto ! A
T24(A) = Env ! Sto ! A
T13(A) = Sto ! A  Sto
T14(A) = Env ! Sto ! A  Sto
where T34 and T23 are environment monads, T13 is the store monad, T24 is a \double
environment" monad, and T14 is an \environment / store" monad. We also have an
identity monad from each level to itself (not shown). Notice that there is no monadfrom L1 to L2. Composition is given by

T34  T13 = T14
T34  T23 = T24
both of which satisfy the compatibility laws.
A strati ed monad is a category of levels and monads satisfying several additional
properties that do not follow solely from the category structure. We require All diagrams commute.
 There are distinguished levels Bot and Top.
 Bot is the identity type constructor.
 Bot and Top are related by a monad T . We also call the entire strati ed monadT.

 Bot must be minimal, and Top must be maximal, meaning that no monad canrelate any L to Bot or Top to any L.

71
The requirement that all diagrams commute means there is at most monad relating
any two levels (there may be none), since two parallel arrows form a diagram. Also,
by forgetting the structure of the arrows, we obtain a partial order in which L1 v L2
if and only if there is a monad relating L1 to L2.
In necessary, we can drop the \all diagrams commute" condition however, mostsemantics obey it, since there aren't usually multiple ways to relate levels. Indeed,
we could call a language \non-uniform" if it requires multiple monads between levels
to de ne its constructs. This restriction makes the implementation of SL easier since
we don't have to specify which monad we want.
We do not require Bot and Top to be initial and terminal (stronger conditions
that minimal and maximal), since some semantics include levels unrelated to Bot andTop for instance, in the previous example, Bot fails to be initial since there is nomonad T12. In many semantics, however, they are actually initial and terminal.
A level L is a monad (rather than just an endofunction) if there is a monadrelating Bot to it hence, Bot is initial if and only if all levels are monads. Thus, inthe previous example, L2 isn't a monad. I haven't found any real examples where
Top fails to be terminal, but we weaken this condition for symmetry.

4.2 Stratied monad transformers
According to the \categorical imperative", we should now form a category ofstrati ed monads however, in this application, we do not need this structure.
Thus, a strati ed monad transformer is an endofunction on the set of strati ed
monads. We can verify these directly for each transformer that it respects the strati ed monad structure.
In practice, we build strati ed monad transformers by \lifting" ordinary monadtransformers to act on strati ed monads. Here the lifting is along the map thatextracts the monad T relating Bot to Top from the strati ed monad T (recall our
naming convention). The action of a strati ed monad transformer is not hard to

72
guess from its action on levels. Let's do an example. By applying strati ed monadtransformers, we build the semantics
Den (A) = Env ! Sto ! List (A  Sto )We begin with an identity strati ed monad, which has a single level and a single
monad:

L1(A) = A
T11(A) = A
We apply the nondeterminism strati ed monad transformer F (T )(A) = T (List (A)).
Omitting the identity monads at each level, we obtain

L2(A) = List (A)L1(A) = A
T12(A) = List (A)Remember that each Tij is an entire monad, not just a type constructor. Now weapply the store strati ed monad transformer F (T )(A) = Sto ! T (A  Sto ), obtaining

L4(A) = Sto ! List (Sto  A)
L3(A) = List (Sto  A)
L2(A) = Sto  A
L1(A) = A
T34(A) = Sto ! A

73

T23(A) = List (A)
T24(A) = Sto ! List (A)T14(A) = Sto ! List (Sto  A)

Finally, we apply the environment strati ed monad transformer F (T )(A) = Env !
T (A):

L5(A) = Env ! Sto ! List (Sto  A)
L4(A) = Sto ! List (Sto  A)
L3(A) = List (Sto  A)
L2(A) = Sto  A
L1(A) = A
T45(A) = Env ! A
T34(A) = Sto ! A
T23(A) = List (A)
T35(A) = Env ! Sto ! A
T24(A) = Sto ! List (A)
T25(A) = Env ! Sto ! List (A)T14(A) = Sto ! List (Sto  A)
T15(A) = Env ! Sto ! List (Sto  A)
In the next few sections, we elaborate the action of the strati ed monad transformers
built from the classes of monad transformers discussed in section 2.6.3.

4.2.1 Top transformers

Top transformers have the form F (T ) = S  T . F acts on the levels of a strati ed
monad by adding a new top level S  Top . F acts on the monads by applying F to

74
all monads relating to Top. We add the new monads without deleting the originals.
We can verify this action in the example above for the environment transformer,
which has S (A) = Env ! A. We formed each of the monads involving environmentsby transforming a monad relating some level to Top. Conversely, all such monads
were transformed.

4.2.2 Bottom transformers

Bottom transformers have the form F (T ) = T  U . F acts on levels by composing
each level with U and adding a new identity at the bottom. F acts on monads byapplying F to all monads relating to Bot. As before, we add the new monads without
deleting the originals.
We can verify this action in the example above for the nondeterminism transformer, which has U (A) = List (A). We formed each of the monads involving lists bytransforming a monad relating some level to Bot. Conversely, all such monads weretransformed.

4.2.3 Around transformers
Around transformers are somewhat more complex than bottom and top transformers. In order to construct all the possible monads relating dierent levels, we
require three ordinary monad transformers, not just one. If the around transformer isFA(T ) = S  T  U
we also require

FB(T ) = S  T
FT (T ) = T  U

The action on levels is to add a new top level S Top , compose each level with U below,
and add a new identity as Bot. The action on monads is to transform the monad75

T using FA, to transform all monads relating to Bot using FB , and to transform all
monads relating to Top using FT . Note that we also transform T using FB and FT .
As before, we add the new monads to the result, leaving the old ones in place.
We obtain the store monad transformer by taking
Ar (T )A = Sto ! T (A  Sto )Top (T )A = Sto ! T (A)We do not use a Bot transformer, since it would have to be
Bot (T )A = T (A  Sto )and we have seen that this choice does not make sense.

4.2.4 Continuation transformers
The continuation transformer is

F (T )(A) = (A ! T (Ans )) ! T (Ans )where Ans is a xed domain of answers. F acts on levels as F (L)(A) = L(Ans ). Thatis, once T is applied to answers, it ignores whatever else we apply it to. We add asingle new level L(A) = (A ! T (Ans )) ! T (Ans ), where T is the old top level.
F acts on monads as follows. It transforms T using the continuation transformer,
yielding a monad relating Bot to the new Top. It also transforms monads M relating
to Top via a special \answer transformer" FAns , yielding monads relating M to the
new Top. These monads allow us to access the levels of the answer type T (Ans ).
There are two choices for FAns , shown in gures 4.1 and 4.2. If we de ne amb inthe semantics

Den(A) = (A ! List (Ans )) ! List (Ans )using each of these choices, we obtain

76(define ((unit1 a) k)(bindT (unitM a) k))(define ((bind1 c f) k)(bindM (c unitT)(lambda (a)((f a) k))))Figure 4.1: First answer transformer(define ((unit2 a) k)(unitM a))(define ((bind2 c f) k)(bindM (c k)(lambda (a)((f a) k))))Figure 4.2: Second answer transformer(define ((amb1 d1 d2) k)(reduce append ()(map k (append (d1 list) (d2 list)))))(define ((amb2 d1 d2) k)(append (d1 k) (d2 k)))as discussed in section 1.5.2. Both de nitions are reasonable.

4.3 Computation ADTs
A computation ADT is a strati ed monad, except that we associate a set ofnames with each level. Since there is at most a single monad relating any pair oflevels, monads are uniquely identi ed by the levels they relate.
We use sets of names because a single level can play multiple roles in a semantics.
For example, in77
Den (A) = Env ! List (A)the level List (A) is called both Lists and Env-Results.
Each strati ed monad transformer adds several new names. For example, theenvironment transformer adds the following pairs of names and levels:
Envs
Env-Results
Env-Values) Env ! T (A)) T (A)) A

Table 4.1 shows the names added by each transformer. In some cases, we reuse thesame strati ed monad transformer, changing only the names that it adds. For example, we build both the Stores and Batch I/O modules using the store transformer. We
can build a semantics using multiple instances of the same transformer (environments,for example) by assigning dierent names to the instances.
Table 4.2 shows the names and levels associated with the following language definition:(define computations(make-computations
cbv-environments
storescontinuations
nondeterminism
errors))Using the information contained in table 4.1, we can de ne language constructs
over strati ed monads. Construct de nitions assume the existence of various levels
and monads. For example, %amb assumes the existence of the level Lists and a monadrelating Lists to Top. The de nition of %amb is

78
ModuleEnvironments

Names
Levels
Envs
Env ! T (A)Env-Results
T (A)Env-Values
A
StoresStoresSto ! T (A  Sto )Store-Results T (A  Sto )Store-Pairs
A  StoStore-Values
A
Batch I/O
IO
IO ! T (A  IO )IO-Results
T (A  IO )IO-Pairs
A  IOIO-ValuesA
Lifting 1
Lifts
1 ! T (A)
Lifting 2
Lifts
1!A
ErrorsErrors
A + Err
OutputOutputA  Out
Nondeterminism Lists
List (A)Continuations Conts(A ! T (Ans )) ! T (Ans )Cont-ValuesA
Cont-Answers T (Ans )Answers
Ans
Resumptions
Res-Topx (X ) T (A + X )Res-Bottom
A + x (X ) T (A + X )Table 4.1: Names associated with each transformer(define %amb
(let ((unit (get-unit 'Lists 'Top))(bind (get-bind 'Lists 'Top)))(lambda (x y)(bind x(lambda (x)(bind y(lambda (y)(unit (append x y)))))))))The strati ed monad operators are not quite sucient to form a truly abstract data
type of computations. We need to know precisely the additional information containedin table 4.1. For example, Lists are lists of some type, Envs are functions fromenvironments to Env-Results, etcetera. Thus, if we desire to build true abstract data

79
Names
Envs, Top
Env-Results, Stores

Level L(A) =
Env !
Sto !
let A1 = List (Ans  Sto ) + Err in(A  Sto ! A1) ! A1
Sto !
let A1 = List (Ans  Sto ) + Err in(A  Sto ! A1) ! A1
let A1 = List (Ans  Sto ) + Err in(A  Sto ! A1) ! A1
List (Ans  Sto ) + Err
List (Ans  Sto )Ans  StoA  StoStore-Results, Conts
Cont-Answers, Errors
Lists
Answers
Store-Pairs, Cont-Values
Env-Values, Store-Values, Bottom A
Table 4.2: Levels and names for a complex language

types, we have to represent all this information as part of the interface.
The types Sto and Env are parameters to the semantics that can be speci ed quite
late. That is, after forming a computation ADT, we can decide what type variables
should denote. Of course, the language constructs must implement this choice, andnot all choices make sense.

4.4 Language ADTs
In general, operators that act primarily at a single level, such as %amb ( gure 1.21)
and %let ( gure 1.19), are easy to write using standard idioms. More complex operators, such as %call/cc, are best written by abstracting from their de nitions in an
example semantics. Using a suciently complex semantics ensures that conceptually
distinct levels are not confused. Table 4.4 lists the available modules and the values
and language constructs they de ne. We omit leading percent signs from the names.
SL includes four types of procedures. Table 4.3 shows the levels of their domains
and codomains. We de ne all four types of procedures over the same environments

80
Procedure type Domain
Codomain
CBV-static
Env-Values Env-Results
CBN-static
Env-Results Env-Results
CBV-dynamic Env-Values Envs
CBN-dynamic Env-Results Envs
Table 4.3: Procedure types
monad transformer by writing dierent versions of %lambda and %call. Clearly, we
can de ne other types of procedures as well.

81

ModuleValuesConstructs
Amb
amb
Batch I/O
read, write, end-of-input?
Begin
unit
begin, unit
Booleans
booleans true, false, not, if, boolean?
CallCC
callccDynamic procedures procedures lambda, call, procedure?
Environments
var, letError exceptions
error
Error values
errorserror
Exp environments
evar, eletFixfix, rec, letrec
Numbers
numbers num, +, -, *, /Numeric predicates=?, zero?, number?
Outputwrite
Procedures
procedures lambda, call, procedure?
Products
pairs
pair, left, right, pair?
Resumptions
pause, seq, par
Shift
shift, reset
Storesfetch, store
Sums
sums
case, in-left, in-right, sum?
While
while
Table 4.4: Modules and language constructs

Chapter 5
Conclusion
This chapter compares lifting and strati cation, describes the limitations of theseideas, relates this work to previous research, and suggests directions for further exploration.

5.1 Lifting versus stratication
The main problem with lifting is that it ties language constructs too tightly tothe monad transformers on which they are de ned. For example, if we de ne variablereference on Env ! T (A), there is no easy way to raise an unbound variable error.
We could de ne an ad-hoc set of lower-level operators to circumvent this problem (see
LHJ95]) however, strati cation shows how to de ne a principled set of lower-level
operators.
Phrased dierently, constructs cannot interact with multiple semantic levels. For
example, + interacts with values and errors, raising an error for non-numeric arguments, and callcc interacts with continuations, environments, and values. Table 5.1
shows the levels referenced by the more complex language constructs.
Lifting also interleaves the creation of new operators with the lifting of old ones.
Not only are these actions conceptually separate, but when we use a transformer, wemight not want all of the operators that come with it. Again, strati cation provides
82

83
Construct

Modules referenced%end-of-input?
IO, booleans%read, %write
IO, numbers%call/cc, %shift continuations, environments, procedures%lambda, %call
environments, procedures%var
environments, errors%fix, %reclifting, environments, procedures%letrec
lifting, environments%/
numbers, errors%casesums, environments, procedures
Table 5.1: Non-local language constructs
a solution by separating the language constructs from the base semantics. Still, thelifting approach remains viable for building abstract data types whose operators are
more local.

5.2 Limitations
SL has several intended limitations: Since it was designed to build denotational models, SL does not address issuesof type and syntax, which occupy large parts of most language speci cations.

 We could extend SL to perform almost any compositional program analysis

however, it provides no help in de ning \extra semantic" mechanisms suchas uni cation or constraint set solution. That is, although an SL-constructedanalysis could derive a set of type constraints from a typed program, it would
not solve them.

 Although SL can build the basic semantics for a real-world language like C, by
the time we add all the speci c details of C's language constructs, we would
hardly claim to have built C from reusable parts.

84
SL also has several unintended limitations, but their descriptions are rather technical. First, store transformers do not compose modularly with each other. For
example, suppose we de ne a language that includes both stores and batch I/O (twodierent parametrizations of the store transformer). By composition, we obtain
Sto ! (IO ! (Val  Sto )  IO )Consider the following construct (%read would do as well):(define (((%end-of-input?) sto) io)(pair (pair (in 'booleans (null? io)) sto) io))

To de ne it directly (see appendix B.2, gure B.18), we need a monad relating Val
to Val  Sto , an impossibility.
There are two unsatisfactory solutions to this problem. The rst is to compose
the transformers in the opposite order and hope that the store operators don't requirea monad from Val to Val  IO (indeed, they don't).
The second solution is, instead of lifting Val to Val  Sto , to return Val in placeof Val  Sto , as though we could put any type at all there. Then we adjust theresult appropriately at the end (see gure 5.1). Hudak et al. adopt this solution
ubiquitously LHJ95], as described in section 5.3. The real problem is that monads
are not exible enough to handle store transformers. We require a more sophisticatedlifting operator, although its form is not yet clear.
The second unintended problem is similar to the rst. When de ning %callcc in
the usual Scheme semantics, we need to uncurry a function fromf : Val ! Sto ! Val  Sto
tof : Val  Sto ! Val  Sto0

Surprisingly enough, the strati ed monad operators on stores cannot perform thistransformation. To be clear, we should say that our goal is not explicitly to uncurry
f but to change its type from85
(define %end-of-input?
(let ((unitT (get-unit 'io-pairs 'io-results))(unitS (get-unit 'io 'top))(unitB (get-value-unit 'booleans 'top))(bindV (get-bind 'io-values 'top)))(lambda ()(bindV(unitS(lambda (io)(unitT (pair (null? (batch-input io))io))))(lambda (b)(unitB b))))))

Figure 5.1: Odd de nition of %end-of-input?

f : Store-Values ! Storestof : Store-Pairs ! Store-Results0(see section 4.3).
To circumvent this problem, we add a left inverse to unit to each monad, called
iunit. Then the required lifting can be de ned (see the tilt function in the de nitionof %callcc, appendix B.2). Since we require unit to be injective, a left inverse always
exists however, it is less apparent that the argument to iunit in the %callcc isalways in its domain. In this case, if we could prove using the monad laws that its
argument is always unit of something, we could probably eliminate iunit.
iunit is clearly a hack once again, the monad operators are simply not powerfulenough to perform all manipulations of the store transformer that occur in standard
construct de nitions.

86

5.3 Related work
Spivey Spi90] used monads to abstract over exception handling but did not connect
these ideas with extensibility.

Moggi Mog89b, Mog91] split an \applied" lambda calculus into a core (variables

and environments) and an extension (other features), expressed as a monad.
He presented many extensions and derived a \computational lambda calculus"
for reasoning about programs.

Moggi also showed that monad transformers can build complex monads fromparts Mog89a]. This crucial facility was hitherto missing however, his presentation is dicult, and few researchers realized that he had made substantial
progress.
Rewriting Moggi's methods Esp94], I saw that they did not easily handle constructs involving multiple semantic levels, such as %call/cc or even %+ (because
it raises errors on non-numbers). Strati ed monads solve this problem, increasing modularity by inserting an abstraction barrier between computation ADT
and language ADT.

Wadler Wad92] popularized Moggi's ideas by presenting monadic interpreters writ-ten in Haskell. The interpreters' limitation to extension by a single monadmotivated this thesis. Also, Wadler and King showed how to combine continuations and lists with other monads KW92]. Despite Moggi's earlier formulationof monad transformers, they discussed \combining M and L" rather than \constructing ML from M ". SL treats monad constructors in general and exhibits acomplete system for building interpreters from multiple modules, not just two.

Steele Ste94] showed how to compose pseudomonads, a new construction. Although
they compose, pseudomonads are both more complex and less general thanmonad transformers. In fact, pseudomonads are essentially bottom monad transformers. That is, they can realize

87

F (T )(A) = T (List A)
F (T )(A) = T (A + X )F (T )(A) = T (A  M )but not

F (T )(A) = Env ! T (A)F (T )(A) = Sto ! T (A  Sto )Steele's claim that pseudomonads improve on monad transformers by providing
a xed composition operator fails to hold since they are not equally powerful however, Steele's complete implementation of a modular semantics was
inspiring, and the strati ed approach described here is based on his tower ofpseudomonads.

Jones and Duponcheel JD93] addressed the problem of composing monads. They

showed rigorously that monads do not compose, but that if one of several auxiliary maps is de ned relating the structures of two monads, they can be composed. They found that some monads compose naturally to the left and someto the right (corresponding to our bottom and top). Although composition isstrictly weaker than transformation, they came as close as one could to discovering monad transformers, and their work provides useful information about
the structure of semantic models however, they did not attempt to build interpreters.

Mosses Mos92] showed how an abstract semantic algebra, which we call a com-putation ADT, could modularize a semantics. By choosing algebra operators
low-level enough to be exible, yet high-level enough to hide irrelevant details,
we can make a semantics much easier to understand.

88
Mosses gave a single ADT with operators for environments, stores, and continuations. Using this ADT, we can de ne other semantic features, but only in an
unnatural and non-modular way. With SL, we can build ADTs custom tailoredto the languages we de ne. In essence, SL is the nal step in Mosses's program,the ability to combine algebras.

Filinski Fil94] showed how to compute over an arbitrary monad in a language withcomposable continuations. His construction is a direct use of the continuationmonad transformer

F (T )(A) = (A ! T (Ans )) ! T (Ans )Most of his paper presents a rather technical proof that computing over F (T )yields the same results as computing over T , as long as our constructs don't use
F . It is possible that his proof could be simpli ed using the general propertiesof monad transformers.
Although composable continuations yield extensibility, we could alternatively
add re ection operators to a language directly. Thus, we would need nothing
but lambda calculus and primitives to be \monadically complete" however,this point is irrelevant, since we probably want to stores and continuations tobe primitive for eciency. Extensibility through continuations costs nothing(beyond the continuations) if we don't use it. This point is not obvious see
Filinski's paper.

Cartwright and Felleisen CF94] postulate that a computation is either a value
or an eect and include a resource administrator to manage eects. Theirsemantics already includes environments, stores, and continuations, the latter
two of which are hidden using a monad (bind is called handle).

Their semantics employs object-oriented techniques such as extensible products (for stores), extensible sums (for values), and \self" arguments (for interpreter composition). These techniques recall my earlier thesis proposals

89Esp93a, Esp93b], although there was no direct connection.
In general, it not surprising that Felleisen and Cartwright's system can be extended with stores and continuations, since they are already included, in theguise of a resource administrator. The intuitive value of this abstraction remains
to be seen. We can extend the store however, stores are already extensible inmost languages, since we can create new locations on demand.

Liang, Hudak, and Jones LHJ95] recently published a paper improving on myearlier work Esp94] and on Moggi's work as well.

Their rst improvement was to lift callcc using operators designed speci callyfor it. Both Moggi and I lifted all operators of a given type in a similar way(parametrically, rather than ad-hoc). Ad-hoc liftings are non-modular, since
they require a new lifting method for each operator and monad transformer.
Using strati ed monads, we can de ne a single reusable callcc (see gure B.20).
Although its de nition is complex, it is independent of new transformers.
Their second improvement was to express monad transformers in a typed language (Gofer, an extension of Haskell). This work shows the power of Jones's
constructor classes, since monad transformers cannot be expressed in pure
Haskell.
The main problem with Liang, Hudak, and Jones's approach is the treatmentof non-local language constructs (those involving multiple levels). They shift
all interaction to the top or bottom of the single monad that de nes the basesemantics. That is, in a semantics
Den = Env ! List (Val )procedures have types

CBV Proc = Val ! Den
CBN Proc = Den ! Den

90
Although these appear reasonable at rst glance, procedure arguments andresults unnecessarily include environments. That is, without access to intermediate levels in the semantics, their types lose precision.
Similarly, to de ne variable reference, they form Den (Env ), denotations that
return environments. In eect, this approach desugars a reference to x into
(env-lookup 'x (the-environment))

Explaining variable reference using rst-class environments is inappropriate,
since environments would not normally appear in a language's value domain.
Of course, after simpli cation, the actual constructs reduce to the de nitions
we would expect, so perhaps the ends justify the means. In general, since theirapproach is based on lifting, it is much weaker than strati cation, as discussed
in section 5.1.

5.4 Future work
Implementation As mentioned in section A.1, we could rewrite SL in Quest Car89]
to verify proper use of higher-order types.

By forming domains from expressions instead of functions, we could build abstract interpretations, translations (such as CPS), and simple compilers.
We could apply the methods developed here to other semantically complex domains, such as communication protocols. If we don't need functional abstraction, simpler lifting operators than monads should suce (see section 2.2.3).

Extensibility We could generalize call-by-value and call-by-name to abstract overother semantic levels. For instance, abstracting over the top level of denotations
yields most of the functionality due to macros. Also, we could de ne a language
capable of abstracting over each semantic level.

91
We could de ne a uniform family of rei cation and re ection operators (seeFil94]), one for each semantic level. These would generalize constructs such as
the-environment, call/cc, and exception handling.

Models Are strati ed monads derivable from more categorical considerations? Since

the monad laws follow nicely from the Kleisli formulation, can we de ne a Kleisli
category for several monads at once? This construction would presumably be
a product of the individual Kleisli categories, indexed by monad. The key idea
is that compositions associate.

Having presented two approaches to building interpreters, lifting and stratication, can we show their equivalence, at least in the cases that lifting canhandle?

Logics Can we develop modular calculi for reasoning about the languages we con-struct? Moggi's computational lambda calculus Mog91] captures precisely theinferences valid for lambda calculus over an arbitrary monad. Moggi's syntactic
approach MC93] is relevant but does not seem to address the problem directly.

Calculi can probably be derived via both lifting and strati cation. Given a setof laws on T , can we lift them to F (T )? Or, can we use the strati ed monadlaws to derive laws for a completed semantics? Abramsky's work Abr91] on
deriving program logics from domain equations is applicable to domains built
using type constructors however, his methods seem to derive calculi that are
still very low-level.

5.5 Conclusion
Four simple imperatives summarize this thesis: Think with types, both abstract and concrete.
 Compute with denotations, not expressions.

92

 Split a complex interpreter into a computation ADT and a language ADT.
 Structure the computation ADT using monads and monad transformers.
The rst two of these are most important, since types let us think in a simple
yet structured way, and denotations let us implement interpreters easily and directly.
These two ideas make an otherwise dicult eld accessible to anyone who understands
functional programming.

BibliographyAbr91]

Samson Abramsky. Domain theory in logical form. Annals of Pure andApplied Logic, 51:1{77, 1991.

ASS85]Harold Abelson, Gerald J. Sussman, and Julie Sussman. Structure andInterpretation of Computer Programs. MIT Press, Cambridge, MA,1985.

Bec69]Jon Beck. Distributive laws. In Seminar on Triples and Categorical
Homology Theory, volume 80 of Lecture Notes in Mathematics, pages
119{140. Springer Verlag, 1969.

BW85]

Michael Barr and Charles Wells. Toposes, Triples, and Theories.
Springer Verlag, New York, 1985.

BW90]

Michael Barr and Charles Wells. Category Theory for Computing Science. Prentice-Hall, 1990.

Car89]Luca Cardelli. Typeful programming. Technical Report 45, DEC Systems Research Center, Palo Alto, CA, May 1989.

CF94]

Robert Cartwright and Matthias Felleisen. Extensible denotational
language speci cations. In Theoretical Aspects of Computer Software,
Sendai, Japan, April 1994.

CR91]

Will Clinger and Jonathan Rees. Revised4 Report on Scheme. Lisp
Pointers, 4(3), 1991.
93

94
Esp93a]David Espinosa. Language extensibility via rst-class interpreters andconstructive modules. See http://www.cs.columbia.edu, April 1993.

Esp93b]David Espinosa. Language features for extensible programs. See
http://www.cs.columbia.edu, October 1993.

Esp94]David Espinosa. Semantic Lego. See http://www.cs.columbia.edu, January 1994.

Fil89]Andrzej Filinski. Declarative continuations and categorical duality.
Master's thesis, University of Copenhagen, August 1989. See http://www.cs.cmu.edu:8001.

Fil94]Andrzej Filinski. Representing monads. In Proceedings of the 21st Annual ACM Symposium on Principles of Programming Languages, Portland, OR, January 1994.

GM94]

Carl Gunter and John Mitchell, editors. Theoretical Aspects of ObjectOriented Programming. MIT Press, Cambridge, MA, 1994.

GTWW77] J. A. Goguen, J. W. Thatcher, E. G. Wagner, and J. B. Wright. Initial
algebra semantics and continuous algebras. Journal of the ACM, 24:68{
95, 1977.
Gun92]

Carl Gunter. Semantics of Programming Languages. MIT Press, Cambridge, MA, 1992.

JD93]Mark P. Jones and Luc Duponcheel. Composing monads. Technical
Report YALEU / DCS / RR-1004, Yale University, December 1993.

KBdR91] Gregor Kiczales, Daniel G. Bobrow, and Jim des Rivieres. The Art of
the Metaobject Protocol. MIT Press, Cambridge, MA, 1991.

95
KW92]David King and Philip Wadler. Combining monads. In Proceedings ofthe Fifth Annual Glasgow Workshop on Functional Programming, Ayr,
Scotland, 1992. Springer Verlag.

Lam88]John Lamping. A uni ed system of parametrization for programming
languages. In Conference Record of the 1988 ACM Symposium on Lispand Functional Programming, pages 316{326, Snowbird, Utah, July
1988.

LHJ95]

Sheng Liang, Paul Hudak, and Mark Jones. Monad transformers andmodular interpreters. In Proceedings of the 22nd Annual ACM Symposium on Principles of Programming Languages, San Francisco, CA,
January 1995.

Mac71]

Saunders MacLane. Category theory for the Working Mathematician.
Springer Verlag, New York, 1971.

MB88]

Saunders MacLane and Garrett Birkho. Algebra. Chelsea, New York,
3rd edition, 1988.

MC93]

Eugenio Moggi and Pietro Cenciarelli. A syntactic approach to modularity in denotational semantics. In Category Theory and Computer
Science, Lecture Notes in Computer Science. Springer Verlag, 1993.

Mes89]Jose Meseguer. General logics. In H. D. Ebbinghaus, editor, Logic Colloquium 87, pages 275{329. North Holland, 1989.

Mog89a]

Eugenio Moggi. An abstract view of programming languages. Technical Report ECS-LFCS-90-113, Laboratory for Foundations of Computer
Science, University of Edinburgh, Edinburgh, Scotland, June 1989. FTP
from theory.doc.ic.ac.uk.

96
Mog89b]

Eugenio Moggi. Computational lambda calculus and monads. In IEEE
Symposium on Logic in Computer Science, pages 14{23, Asilomar, CA,
June 1989.

Mog91]

Eugenio Moggi. Notions of computation and monads. Information andComputation, 93:55{92, 1991.

Mos92]

Peter D. Mosses. Action Semantics, volume 26 of Tracts in TheoreticalComputer Science. Cambridge University Press, 1992.

Pie91]

Benjamin C. Pierce. Basic Category Theory for Computer Scientists.
MIT Press, Cambridge, MA, 1991.

RB90]David Rydeheard and Rod Burstall. Computational Category Theory.
Prentice-Hall, New York, 1990.

Sch86]David A. Schmidt. Denotational Semantics. Allyn and Bacon, New
York, 1986.

Spi89]Michael Spivey. A categorical approach to the theory of lists. In Mathematics of Program Construction, volume 375 of Lecture Notes in Computer Science, pages 399{408. Springer Verlag, 1989.

Spi90]Michael Spivey. A functional theory of exceptions. Science of Computer
Programming, 14(1):25{42, June 1990.

Spi93]

Michael Spivey. Category theory and functional programming. Technical
Report PRG TR 7-93, Oxford University, June 1993.

Ste94]

Guy L. Steele, Jr. Building interpreters by composing monads. In Proceedings of the 21st Annual ACM Symposium on Principles of Programming Languages, Portland, OR, January 1994.

Wad89]

Philip Wadler. Theorems for free. In Functional Programming Languages
and Computer Architecture, London, England, September 1989.

97
Wad92]

Philip Wadler. The essence of functional programming. In Proceedings of the 19th Annual ACM Symposium on Principles of Programming
Languages, pages 1{14, Albuquerque, NM, January 1992.

Appendix A
Miscellanea
This appendix discusses issues tangent to the thesis proper at various points.

A.1 Why Scheme?
The real reason for writing this thesis in Scheme1 is that I'm used to it. Although
Scheme has many problems (notably the lack of modules and abstract data types), it
is still pretty fun to program in. But, for this thesis, Scheme has several disadvantages:

 It fails to express the typed structure of the mathematics.
 Implicit polymorphism does not distinguish between a polymorphic function
and its instantiations at various types hence, a whole level of structure is lost.

 Since types are not mechanically veri ed, our understanding of them could beincorrect.

On the other hand, Scheme's advantage is that it does not limit what we can
express. For example, in the usual Hindley-Milner type system, polymorphic values
When I failed to explain an example suciently in an earlier thesis proposal, one reader exclaimed, \You can't write your thesis in Scheme!"
1

98

99
are not rst-class, since we cannot instantiate them at dierent types. F2 has rstclass polymorphism but cannot treat type constructors as types, so that monads
cannot be rst-class.
We can probably type SL in F3, which includes type constructors however, it is
not clear how to type the levels of a strati ed monad. For instance, we would needtypes Envs and Env-Results such thatEnvs = Env ! Env-Results(see section 4.3). It would be a good exercise to rewrite SL in Cardelli's Quest
language, which includes higher-order polymorphism as well as several other advanced
typing ideas Car89]. Also, Liang, Hudak, and Jones LHJ95] have implemented
monad transformers in Gofer, a version of Haskell with an enhanced type system(essentially Hindley-Milner extended to higher types).
In general, the programming languages community is realizing that current typesystems are inadequate however, we should go further and question the entire basis
for typed languages. In general, types are a form of speci cation. When we say thatan expression has a type, we really mean that its evaluation meets a speci cation.
This point of view leads naturally to more expressive types. Although inference
and veri cation are intractable for these systems, we should recall that for years,
proof veri ers have automated a well-de ned class of simple inferences within complex
logics.
To strengthen the case for more expressive types, we cite two examples from themonad literature of problems with limited type systems. In Ste94], Steele writes,\: : : the principal practical motivation for a program simpli er] was to transform thecode into a form acceptable to the Haskell type-checker". In other words, he had totreat programs at the syntactic level in order to bypass the type system. In Fil94],
Filinski circumvents ML's type system using a universal type. He also states in adierent context, \Peyton-Jones and Wadler probe the relationship between monads
and CPS further, and Wadler analyzes composable continuations from a monadic

100
perspective, but in both cases the restriction to Hindley-Milner typeability obscuresthe deeper connections."

A.2 Typed versus untyped values
Typed languages have multiple value domains, one for each type, and determine
expression types statically. Untyped languages have a single value domain that isa sum of several others, and determine types dynamically. Untyped languages also
make fewer type distinctions than typed languages, particularly with respect to procedures. For instance, Scheme does not distinguish procedures returning numbers
from procedures returning pairs.
Monads are typed, as are all category-theoretic concepts, and denotations arepolymorphic over values. For example, we can type the language construct %zero?
as%zero?

: Den (Num ) ! Den (Bool )However, in SL, we compute over a single untyped value domain, represented as anextensible sum. Thus %zero? has type%zero?

: Den ! Den

where we write Den instead of Den (Val ). Tagging values with their types exposes thetreatment of types in the semantic equations and abstracts from the existing Scheme
types.
Most type systems are not powerful enough to type typed interpreters. For example, the interpreters in Wad92] are untyped even though they are written in Haskell,which is typed. The problem is that we would like to write(%var 'x)

: Numwhen x is a number however, the type of (%var 'x) depends on the context inwhich the expression occurs. In general, the type of an expression needs to include

101
the names and types of its free variables, just as in the usual sequent-based typing
rules.
On a slightly dierent subject, Steele Ste94] tries to extend the domain of values
using monads, and I follow him in Esp94] however, as he points out, using theexceptions monad to build extensible sums yields behavior such as(compute (%+ (%num 3) (%true)))true)which shows that monads are not the right tool for building extensible sums.

A.3 Extensible sums and products
Although extensible sums and products play little part in this thesis, they areuseful for building extensible systems (see Esp93b]), and I believe they capture theessential aspects of object-oriented programming. They also demonstrate how category theory can aid language design. We consider types

S = S1 + S2 + 
P = P1  P2  that can be extended either statically or dynamically. It doesn't matter which these
considerations are orthogonal to the basic idea. To S and P there correspond extensible functions

s:S !B
p:A!P
Note that s and p have opposite types. As we extend S or P , we also extend s or p.
As an example, suppose that s computes various vehicles' maximum speeds. Thens : Vehicle ! Number

102
where Vehicle is an extensible sum. Extensible sums are simply generic functionsin the sense of CLOS KBdR91], while extensible products are not commonly used.
The types of s and p come directly from the category-theoretic de nitions of sum
and product. For other theoretical treatments of object-oriented programming, seeGM94].

Appendix B
CodeThis appendix lists the Scheme code for the monad transformers and language constructs presently supported by SL.

B.1 Monad transformer denitions
The code for transforming types and inverse unit operators is omitted for clarity.

103

104

 Environments: F(T)(A) = Env -> T(A)(define (env-trans t)(with-monad t(lambda (unit bind compute)(make-monad(lambda (a)(lambda (env) (unit a)))(lambda (c f)(lambda (env)(bind (c env)
(lambda (a)((f a) env)))))(lambda (c f)(compute (c empty-env) f))))))

Figure B.1: Environment transformer

105
 Exceptions: F(T)(A) = T(A + X)
(define (exception-trans t)(with-monad t(lambda (unit bind compute)(make-monad(lambda (a) (unit (in-left a)))(lambda (c f)(bind c (sum-function
f (lambda (x) (unit (in-right x))))))(lambda (c f)(compute c (sum-function f compute-x)))))))

Figure B.2: Exception transformer Continuations: F(T)(A) = (A -> T(Ans)) -> T(Ans)(define (continuation-trans t)(with-monad t(lambda (unit bind compute)(make-monad(lambda (a)(lambda (k) (k a)))(lambda (c f)(lambda (k)(c (lambda (a) ((f a) k)))))(lambda (c f)(compute (c (compose1 unit value->answer)) f))))))

Figure B.3: Continuation transformer

106

 Stores: F(T)(A) = Sto -> T(A * Sto)(define (store-trans t)(with-monad t(lambda (unit bind compute)(make-monad(lambda (a)(lambda (sto)(unit (pair a sto))))(lambda (c f)(lambda (sto)(bind (c sto)(lambda (as)((f (left as)) (right as))))))(lambda (c f)(compute (c (initial-store))(lambda (a*s)(compute-store (f (left a*s)) (right a*s)))))))))

Figure B.4: Store transformer

107
 Lifting 1: F(T)(A) = 1 -> T(A)(define (lift1-trans t)(with-monad t(lambda (unit bind compute)(make-monad(lambda (a)(lambda () (unit a)))(lambda (c f)(lambda ()(bind (c) (lambda (a) ((f a))))))(lambda (c f)(compute (c) f))))))

Figure B.5: First lifting transformer
 Lifting 2: F(T)(A) = T(1 -> A)(define (lift2-trans t)(with-monad t(lambda (unit bind compute)(make-monad(lambda (a)(unit (lambda () a)))(lambda (c f)(bind c (lambda (l) (f (l)))))(lambda (c f)(compute c (lambda (l) (f (l)))))))))

Figure B.6: Second lifting transformer

108

 Lists: F(T)(A) = T(List(A))(define (list-trans t)(with-monad t(lambda (unit bind compute)(define (amb x y)(bind x(lambda (x)(bind y(lambda (y)(unit (append x y)))))))(make-monad(lambda (a)(unit (list a)))(lambda (c f)(bind c(lambda (l)(reduce amb (unit '()) (map f l)))))(lambda (c f)(compute c (lambda (l) (map f l))))))))Figure B.7: List transformer

109

 Monoids: F(T)(A) = T(A * M)
(define (monoid-trans t)(with-monad t(lambda (unit bind compute)(make-monad(lambda (a) (unit (pair a (monoid-unit))))(lambda (c f)(bind c(lambda (a*m)(let ((c2 (f (left a*m))))(bind c2
(lambda (a*m2)(unit(pair (left a*m2)(monoid-product(right a*m) (right a*m2))))))))))(lambda (c f)(computec (lambda (a*m)(compute-m (f (left a*m)) (right a*m)))))))))

Figure B.8: Monoid transformer

110

 Resumptions: F(T)(A) = fix(X) T(A + X)
(define (resumption-trans t)(with-monad t(lambda (unit bind compute)(make-monad(lambda (a) (unit (in-left a)))(lambda (c f)(let loop ((c c))(bind c(sum-function
f (lambda (c)(unit (in-right (loop c))))))))(lambda (c f)(compute(let loop ((c c))(bind c(sum-function(compose1 unit f)loop)))
id))))))

Figure B.9: Resumption transformer

111

B.2 Language construct denitions
 Amb(define %amb
(let ((unit (get-unit 'lists 'top))(bind (get-bind 'lists 'top)))(lambda (x y)(bind x(lambda (x)(bind y(lambda (y)(unit (append x y)))))))))

Figure B.10: Amb
 Reset  (reset E) ]] k = k (E \i.i)(define %reset(let ((mapC (get-map 'conts 'top))(unitC (get-unit 'cont-values 'cont-answers))(bindC (get-bind 'cont-values 'cont-answers)))(lambda (exp)(mapC exp
(lambda (cont)(lambda (k)(bindC (cont unitC) k)))))))

Figure B.11: Reset

112

 Stores(define %fetch(let ((unitT (get-unit 'store-pairs 'store-results))(unitS (get-unit 'stores 'top)))(lambda (loc)(unitS(lambda (sto)(unitT (pair (store-fetch sto loc) sto)))))))(define %store(let ((unitS (get-unit 'stores 'top))(unitT (get-unit 'store-pairs 'store-results))(bindV (get-bind 'store-values 'top)))(lambda (loc val)(bindV val(lambda (val)(unitS(lambda (sto)(unitT (pair val (store-store sto loc val))))))))))

Figure B.12: Stores Output(define %write(let ((unitV (get-value-unit 'unit 'top))(mapO (get-map 'output 'top)))(lambda (message)(mapO (unitV 'unit)(lambda (a*m)(let ((a (left a*m))(m (right a*m)))(pair a (cons message m))))))))

Figure B.13: Output

113 While(define %while(let ((bindB (get-value-bind 'booleans 'top)))(lambda (c1 c2)(letrec((loop(bindB c1(lambda (b)(if b(%begin2 c2 loop)(%unit))))))
loop))))

Figure B.14: While Begin(define-show 'unit (lambda (b) 'unit))(define %unit (make-op0 'unit 'unit))(define %unit? (make-type-predicate 'unit))(define %begin2(let ((bindV (get-bind 'bottom 'top)))(lambda (c1 c2)(bindV c1(lambda (v1) c2)))))(define (%begin . s)
(reduce %begin2 (%unit) s))

Figure B.15: Begin114 Error exceptions(define (raise-error top)(let ((unit (get-unit 'errors top)))(lambda (msg) (unit (in-right msg)))))(define %error (raise-error 'top))

Figure B.16: Error exceptions Error values(define-show 'errors
identity-procedure)(define-predicate 'errors(lambda (x)(and (pair? x)(eq? (car x) 'error))))(define (raise-error top)(get-value-unit 'errors top))(define %error (raise-error 'top))(define %error? (make-type-predicate 'errors))

Figure B.17: Error values

115
 Batch I/O
 IO= Input * Output
 Input = List Number Output = List Number(define %end-of-input?
(let ((unitT (get-unit 'io-pairs 'io-results))(unitS (get-unit 'io 'top))(unitB (get-value-unit 'booleans 'io-values)))(lambda ()(unitS(lambda (io)(unitT (pair (unitB (null? (batch-input io)))io)))))))(define %read(let ((unitT (get-unit 'io-pairs 'io-results))(unitS (get-unit 'io 'top))(unitN (get-value-unit 'numbers 'io-values)))(lambda ()(unitS(lambda (io)(unitT (pair (unitN (car (batch-input io)))(make-batch (cdr (batch-input io))(batch-output io)))))))))(define %write(let ((unitS (get-unit 'io 'top))(unitT (get-unit 'io-pairs 'io-results))(bindN (get-value-bind 'numbers 'top))(unitU (get-value-unit 'unit 'io-values)))(lambda (val)(bindN val(lambda (val)(unitS(lambda (io)(unitT(pair (unitU 'unit)(make-batch(batch-input io)(cons val (batch-output io))))))))))))

Figure B.18: Batch I/O

116 Booleans(define-show 'booleans(lambda (b) (if b 'true 'false)))(define-predicate 'booleansboolean?)(define %boolean? (make-type-predicate 'booleans))(define %true (make-op0 'booleans #t))(define %false (make-op0 'booleans #f))
(define (b-or x y) (or x y))(define (b-and x y) (and x y))(define %not (make-op1 'booleans 'booleans not))(define %or (make-op2 'booleans 'booleans b-or))(define %and (make-op2 'booleans 'booleans b-and))(define %if(let ((bind (get-value-bind 'booleans 'top)))(lambda (p c a)(bind p(lambda (p)(if p c a))))))

Figure B.19: Booleans

117 Call/CC
 Proc : env-values -> env-results
 Cont : cont-values -> cont-answers(define %call/cc(let ((mapC (get-map 'conts 'top))(mapK (get-map 'conts 'env-results))(iunitK (get-iunit 'conts 'env-results))(unitE (get-unit 'env-values 'env-results))(unitP (get-value-unit 'procedures 'env-values))(unitR (get-unit 'cont-values 'env-results))(bindS (get-value-bind 'procedures 'env-results)))
 tilt : cont-value * (procedures -> env-results) -> conts(define (tilt cv f)(iunitK (bindS (unitR cv) f)))(lambda (exp)(mapC exp
(lambda (cont)(lambda (k)(define (callcc-proc v)(mapK (unitE v)(lambda (cont)(lambda (k1) (cont k)))))(cont(lambda (cv)((tilt cv(lambda (p)(p (unitP callcc-proc))))k)))))))))

Figure B.20: Call with current continuation

118

 Dynamically scoped procedures(define-show 'procedures(lambda (p) '<procedure>))(define-predicate 'procedures
procedure?) Proc : env-values -> envs
(define %lambda(let ((bindE (get-bind 'envs 'top))(unitP (get-value-unit 'procedures 'top)))(lambda (var body)(bindE body(lambda (body)(unitP(lambda (arg)(lambda (env)(body (env-extend env var arg))))))))))(define %call(let ((bindP (get-value-bind 'procedures 'top))(bindV (get-bind 'env-values 'top))(unitE (get-unit 'envs 'top)))(lambda (proc arg)
(bindP proc
(lambda (proc)(bindV arg(lambda (arg)(unitE (proc arg)))))))))

Figure B.21: Dynamically scoped procedures

119

 Environments
 Env = Id -> env-values(define %var(let ((unitT (get-unit 'env-values 'env-results))(unitE (get-unit 'envs 'top))(error (raise-error 'env-results)))(lambda (id)(unitE(lambda (env)(let ((binding (env-lookup env id)))(if binding(unitT (right binding))(error (unbound-error id)))))))))(define %let
(let ((unitE (get-unit 'envs 'top))(bindE (get-bind 'envs 'top))(bindV (get-bind 'env-values 'top)))(lambda (id c1 c2)(bindV c1(lambda (v1)(bindE c2(lambda (c2)(unitE(lambda (env)(c2 (env-extend env id v1)))))))))))

Figure B.22: Environments

120

 Fixed points(define %fix
(let ((bindP (get-value-bind 'procedures 'top))(unitL (get-unit 'lifts 'top))(bindV (get-bind 'env-values 'lifts))(unitR (get-unit 'env-results 'lifts)))(lambda (p)(bindP p(lambda (p)(unitL(fix (lambda (l)(bindV l(lambda (v)(unitR (p v))))))))))))(define %rec(let ((unitE (get-unit 'envs 'top))(bindE (get-bind 'envs 'top))(bindV (get-bind 'env-values 'lifts))(unitL (get-unit 'lifts 'env-results))(unitR (get-unit 'env-results 'lifts)))(lambda (name c)(bindE c(lambda (c)(unitE(lambda (env)(unitL(fix (lambda (l)(bindV l(lambda (v)(unitR (c (env-extend env name v)))))))))))))))

Figure B.23: Fixed points

121

 Letrec(define %letrec(let ((unitE (get-unit 'envs 'top))(bindE (get-bind 'envs 'top))(bindV (get-bind 'env-values 'lifts))(unitL (get-unit 'lifts 'env-results))(unitR (get-unit 'env-results 'lifts)))(lambda (name c1 c2)(bindE c1(lambda (c1)(bindE c2(lambda (c2)(unitE(lambda (env)(unitL(bindV(fix(lambda (l)(bindV l(lambda (v)(unitR (c1 (env-extend env name v)))))))(lambda (v)(unitR (c2 (env-extend env name v)))))))))))))))

Figure B.24: Letrec using xed points

122 Numbers(define-show 'numbers identity-procedure)(define-predicate 'numbers number?)(define %num (get-value-unit 'numbers 'top))(define %+ (make-op2 'numbers 'numbers +))(define %- (make-op2 'numbers 'numbers -))(define %* (make-op2 'numbers 'numbers *))(define %1+ (make-op1 'numbers 'numbers 1+))
(define %-1+ (make-op1 'numbers 'numbers -1+))(define %/(let ((unit (get-value-unit 'numbers 'top))(bind (get-value-bind 'numbers 'top))(error (raise-error 'top)))(lambda (a1 a2)(bind a1
(lambda (a1)(bind a2
(lambda (a2)(if (zero? a2)(error (divide-by-zero-error))(unit (/ a1 a2))))))))))
 Numeric predicates(define %zero? (make-op1 'numbers 'booleans zero?))(define %= (make-op2 'numbers 'booleans =))(define %< (make-op2 'numbers 'booleans <))(define %> (make-op2 'numbers 'booleans >))(define %<= (make-op2 'numbers 'booleans <=))
(define %>= (make-op2 'numbers 'booleans >=))
(define %number? (make-type-predicate 'numbers))

Figure B.25: Numbers

123

 Statically scoped procedures(define-show 'procedures(lambda (p) '<procedure>))(define-predicate 'procedures
procedure?) Proc : env-values -> env-results(define %lambda(let ((unitE (get-unit 'envs 'top))(bindE (get-bind 'envs 'top))(unitP (get-value-unit 'procedures 'env-results)))(lambda (var body)(bindE body(lambda (body)(unitE(lambda (env)(unitP(lambda (arg)(body (env-extend env var arg)))))))))))(define %call(let ((bindP (get-value-bind 'procedures 'top))(bindV (get-bind 'env-values 'top))(unitR (get-unit 'env-results 'top)))(lambda (proc arg)
(bindP proc
(lambda (proc)(bindV arg(lambda (arg)(unitR (proc arg)))))))))(define %procedure? (make-type-predicate 'procedures))

Figure B.26: Statically scoped procedures

124
 Resumptions
 F(T)(A) = rec(X) T(A + X)
 res-top = T(A + X), res-bottom = A + X(define %pause(let ((bindR (get-bind 'res-top 'top))(unitT (get-unit 'res-bottom 'top)))(lambda (c)(bindR c(lambda (t)(unitT (in-right t)))))))(define (%seq2 c1 c2)(%begin2 c1 (%pause c2)))(define (%seq . s)
(reduce %seq2 (%pause (%unit)) s))(define (%par2 c1 c2)(%amb (%then c2 c1)(%then c1 c2)))(define (%par . s)
(reduce %par2 (%pause (%unit)) s))(define %then(let ((bindR (get-bind 'res-bottom 'top))(unitT (get-unit 'res-top 'top)))(lambda (c1 c2)(bindR c1(sum-function(lambda (a) (%pause c2))
(lambda (t) (%pause (%par2 (unitT t) c2))))))))

Figure B.27: Resumptions

125

 Products(define-show 'pairs(lambda (p)`(pair ,(show-value (left p)),(show-value (right p)))))(define-predicate 'pairs pair?)(define %pair? (make-type-predicate 'pairs))(define (make-pair-op op)(let ((unit (get-unit 'bottom 'top))(bind (get-value-bind 'pairs 'top)))(lambda (a)(bind a(lambda (a)(unit (op a)))))))(define %left (make-pair-op left))(define %right (make-pair-op right))(define %pair(let ((unit (get-value-unit 'pairs 'top))(bind (get-bind 'bottom 'top)))(lambda (c1 c2)(bind c1
(lambda (v1)(bind c2
(lambda (v2)(unit (pair v1 v2)))))))))

Figure B.28: Products

126

 Sums(define-show 'sums(lambda (p)(sum-case p(lambda (x) `(in-left ,(show-value x)))(lambda (x) `(in-right ,(show-value x))))))(define-predicate 'sums sum?)(define %sum? (make-type-predicate 'sums))(define (make-sum-op op)(let ((unit (get-value-unit 'sums 'top))(bind (get-bind 'bottom 'top)))(lambda (a)(bind a(lambda (a)(unit (op a)))))))(define %in-left (make-sum-op in-left))(define %in-right (make-sum-op in-right))(define %case(let ((bindS (get-value-bind 'sums 'top))(bindP (get-value-bind 'procedures 'top))(unitV (get-unit 'bottom 'env-values))(unitR (get-unit 'env-results 'top)))(lambda (x f g)(bindS x(sum-function(lambda (x)(bindP f (lambda (f) (unitR (f (unitV x))))))(lambda (x)(bindP g (lambda (g) (unitR (g (unitV x)))))))))))

Figure B.29: Sums

127
 Shift  (shift p) ]] k = (p (\v. \k1. (k1 (k v))) \i.i)(define %shift(let ((mapC (get-map 'conts 'top))(mapK (get-map 'conts 'env-results))(iunitK (get-iunit 'conts 'env-results))(unitC (get-unit 'cont-values 'cont-answers))(bindC (get-bind 'cont-values 'cont-answers))(unitE (get-unit 'env-values 'env-results))(unitP (get-value-unit 'procedures 'env-values))(unitR (get-unit 'cont-values 'env-results))(bindS (get-value-bind 'procedures 'env-results)))
 tilt : cont-value * (procedures -> env-results) -> conts(define (tilt cv f)(iunitK (bindS (unitR cv) f)))(define (cont-compose k1 k2)(lambda (cv)(bindC (k2 cv) k1)))(lambda (exp)(mapC exp
(lambda (cont)(lambda (k)(define (shift-proc v)(mapK (unitE v)(lambda (cont)(lambda (k1)(cont (cont-compose k k1))))))(cont(lambda (cv)((tilt cv(lambda (p)(p (unitP shift-proc))))unitC)))))))))

Figure B.30: Shift