The talk will try to tell a bigger story, following the tantalizing lead: all the founding papers on monads, free monads, monad transformers, handlers, algebraic effects, etc. -- all of them, down to the title, are about extensible interpreters. What we eventually find is the interaction -- between a client and a server, an interpreter and the interpreted code, an expression and its context. The distinction between functional and imperative becomes contingent, an artifact of focusing on a small part of the interacting system. Lambda and State are not at all dissimilar, and can be treated uniformly.
Revisiting the origins of the field and recovering the insights and forgotten alternatives not only help with the wiser attitude towards monads. We see how they help make our programs have the intended effect.
The talk gives the modern reconstruction of Cartwright and Felleisen's ``Extensible Denotational Language Specifications''. We make the effect handlers themselves be modular and extensible -- and be part of a program rather than permanently stationed outside. Notably, Cartwright and Felleisen had to bake the variable environment into the basic semantic framework, even though integers, or first-order sub-languages in general, make no use of it. We avoid postulating the variable environment; we do not need this hypotheses. After all, we treat Lambda on par with the State, in the same uniform formalism. We shall see that the expression problem, stable denotations, and extensible interpreters are all different names for the same thing.
This talk was first presented at the Indiana University's School of Informatics and Computing (SoIC) Computer Science Colloquium on August 25, 2016. I am grateful to Martin Berger for many helpful discussions and especially for explaining the origins of process calculi. Helpful comments by Shin-Cheng Mu are gratefully acknowledged.
Recorded presentation at the Seminar at the Institute of Information Science Academia Sinica, Taipei, Taiwan, December 2, 2016
< https://www.youtube.com/watch?v=GhERMBT7u4w >
In this section, we demonstrate the well-known problem of unstable denotations. It is, Peter Mosses argued, the stumbling block for using denotational semantics in studying and defining real-life languages and their effects. Section 3 brings the insight from process calculi to overcome the problem.
For concreteness, we will be using Haskell to program our definitional interpreters, although OCaml, F# or Scala, among others, would have worked as well. Even the readers unfamiliar with Haskell should be able, hopefully, to get the main idea, by looking at the code and drawing analogies with the standard mathematical notation. After all, when visiting a foreign land, we manage to survive and enjoy the trip, language and cultural barriers notwithstanding. Willingness to communicate goes a long way.
We start with the simplest language of
arithmetic expressions: integer literals, the increment function,
and the application operator to let us apply the increment.
In Haskell, we define the language as a data type
Expr. A sample
expression -- twice incremented literal 2 -- looks then as
data Expr = EInt Int | EInc | EApp Expr Expr tinc = EApp EInc (EApp EInc (EInt 2)) -- inc (inc 2)
We now introduce denotational semantics to give meaning to
denotational semantics is a compositional mapping from
something else. We take the somewhat universal domain
Dom below to be
the meaning, or denotation, of expressions in our language. It contains
integers, booleans, functions, and a special element that stands for
the meaning of a meaningless expression.
data Dom = DError | DInt Int | DBool Bool | DFun (Dom -> Dom)
The semantics, the mapping from expressions
Dom, is then defined constructively, as the Haskell
eval. It is an interpreter of our simple language.
eval :: Expr -> Dom eval (EInt x) = DInt x eval EInc = DFun $ \x -> case x of DInt n -> DInt (succ n) _ -> DError eval (EApp e1 e2) = case eval e1 of DFun f -> f (eval e2) _ -> DErrorWhereas
EApp EInc (EInt 8)signifies the phrase (a mere string)
inc 8in our language,
DInt 9is its meaning, a Haskell integer. The last clause of
evalshows off compositionality: the meaning of
EApp e1 e2depends only on
eval e2: that is, on the meaning of the arguments
e2, but not on the arguments themselves, i.e., not on their structure. Thus denotational semantics is defined by a structurally-inductive interpreter, a fold.
The language is in dire need of new features; for example,
booleans, equality checking on integers, and conditional expressions.
Alas, data types in Haskell are not extensible. Therefore, we have to
Expr to accommodate the extensions:
data Expr = EInt Int | EInc | EApp Expr Expr | EEq | EIf Expr Expr ExprA sample conditional expression
if 3 == inc (inc 2) then 10 else inc (inc (inc 2))looks as
tifbelow. We want to re-use the previously defined
inc (inc 2)but cannot: the type
Exprhas changed. We have to re-define
tincusing the new
Expr, although it looks exactly as before.
tinc1 = EApp EInc (EApp EInc (EInt 2)) tif = EIf (EApp (EApp EEq (EInt 3)) tinc1) (EInt 10) (EApp EInc tinc1)The interpreter
evalgives the meaning to the extended language. The first three clauses look exactly as the old interpreter. Alas, we cannot refer to it and have to write anew: functions in Haskell are not extensible either.
eval :: Expr -> Dom eval (EInt x) = DInt x eval EInc = -- ... as before ... eval (EApp e1 e2) = -- ... as before ... eval EEq = -- similar to EInc eval (EIf e et ef) = case eval e of DBool True -> eval et DBool False -> eval ef _ -> DError
Thus we have run into the instability, or the expression problem: our denotational semantics is brittle and not extensible. We cannot reuse the previously written sample terms and previously written interpreters; we have to re-write them. Arguably, this is the problem with the Haskell formalization rather than denotational semantics. It is still telling. Normally denotational semantics is presented mathematically, and mathematics is usually informal, although still rigorous. Many problems come up in formalization. Luckily, there is a way to make our interpreters extensible.
Dom, let us define a language by directly telling the meaning of each language phrase, and how to make sense of a compound phrase from the meaning of its components. We hence introduce denotational semantics right off the bat, without the intermediate
evalstep. After all, defining the semantics includes defining the structure (syntax) of the language. For generality, which will come handy later on, we do not fix the domain of denotations to be
Dom. Rather, we make it variable
d. All in all, we define a language by a set of definitions, one per syntactic form, each defining the domain mapping for that form. The domain is kept abstract. Thus we define a language as a type class in Haskell (or a module type in OCaml, etc.):
class EBasic d where int :: Int -> d inc :: d app :: d -> d -> d infixl 1 `app` -- make the infix `app` left-associativeThe type class says that our language has two primitives, integer literals and the increment, and one compound expression,
appwith two sub-expressions. The meaning of the compound is determined from the meaning
dof the sub-expressions. The semantics is indeed compositional, by its very design The sample term
inc (inc 2)now takes the form:
ttinc = inc `app` (inc `app` int 2)whose inferred type is
ttinc :: EBasic d => d. One may read it as:
ttincis the term in the
EBasiclanguage. Or: given an appropriate domain -- that is, to which we may map the primitives and compounds of the language --
ttincgives the meaning of the phrase
inc (inc 2)in that domain. What remains is to tell that
Domis `appropriate' to give the meaning to the basic language:
instance EBasic Dom where int = DInt inc = injI succ app (DFun f) e2 = f e2 app _ _ = DErrorwhere we write
injI succfor the Haskell successor function lifted to
DErrorif the value to increment is not a
DInt. The meaning of the sample expression is thus
ttinc :: Dom, that is,
ttincspecialized to the domain type
As before, we have mapped an expression to its meaning, the element of
Dom. Earlier, that mapping was implemented as the Haskell function
eval. Now, it is wired-in into
ttinc itself, while the mapping of the
primitives is collected in
EBasic. We have thus learned that a
mathematical mapping does not have to correspond to a Haskell
function. There are other ways to program it.
Math is abstract, which is a blessing -- it
applies to so many circumstances -- and a curse: one has to know how
to apply it.
Extending the language is much easier in the new approach. To add the equality and the conditional form, we merely need to write down the corresponding definitions, collecting them into a new type class:
class ECond d where eq :: d if_ :: d -> d -> d -> dThe new features are usable right away:
ttif = if_ (eq `app` (int 3) `app` ttinc) (int 10) (inc `app` ttinc)Now, we re-use the previously written term
ttincwithout re-writing it. Likewise, we re-use, rather than re-write the interpreters. The inferred type of
(EBasic d, ECond d) => d, tells that to make sense, it needs the domain mappings for the basic and the conditional primitives. The
EBasic Dommapping was defined earlier and can be used as is. What remains is to tell the meaning of the new features:
instance ECond Dom where eq = -- like inc if_ (DBool True) et ef = et if_ (DBool False) et ef = ef if_ _ _ _ = DError
To summarize, the new way of defining languages, though denotational semantics, lets us easily extend the languages -- re-using rather than re-writing, previously written definitions, interpreters and expressions. We thus obtained the convenient framework for semantic analyses. We will now apply it to the real effect, State.
At first, adding the state effect with its two operations goes smoothly. We define the primitives to access the current state and to change it, returning the new value:
class GlobalIntState d where get :: d put :: d -> dThe sample term
ttS :: (EBasic d, ECond d, GlobalIntState d) => d ttS = if_ (eq `app` (int 3) `app` (put ttinc)) (put (int 10)) (put (inc `app` get))shows off the new operations alongside the old ones: the increment in the earlier term
ttinc. Giving the meaning to
ttSis much harder than writing it. Onto which
Domelement we can possibly map
get? The current state is subject to change and has no fixed value. We need a new semantic domain, of state transformers, which map the current to the new state and give the meaning that depends on the current state.
type DomIntState = Int -> (Dom,Int) instance GlobalIntState DomIntState where get = \s -> (DInt s,s) put e = \s -> case e s of (DInt s',_) -> (DInt s',s') (_,s) -> (DError,s)The meaning of
putbecomes easy to express:
getstands for the current state, which is kept unchanged.
Alas, to give the meaning to
ttS we also need
EBasic DomIntState and
ECond DomIntState instances: the interpretation of the old features in the new
domain. Granted, that is straightforward, merely decorating and re-using
earlier definitions, e.g.,
instance EBasic DomIntState where int x = \s -> (DInt x,s) inc = \s -> (injI succ,s) app e1 e2 = \s0 -> let (f,s1) = e1 s0 (x,s2) = e2 s1 in (app f x,s2) instance ECond DomIntState where eq = \s -> (eq,s) if_ e et ef = \s -> case e s of (DBool True,s) -> et s (DBool False,s) -> ef s
Although the meaning of
app is reasonable and enough for many examples,
it is not as general as should be. The reader is invited to
think why. The second quiz is why we could not reuse the
The problem is not in the complexity of writing the
etc. instances for the new domain, but in the fact that we have to do
it. What if we want to add the global state with several components
(mutable variables)? We have to introduce another domain, and once
again write the
ECond instances. This is a significant
practical problem, for languages with many features. It is also deeply
unsatisfactory: the `true' meaning of integer literals such as
1 or of the the increment
EInc has not changed. The meaning of the
increment is the successor on integers, and it remains the same no
matter whether the language has state or not. Integers are integers
forever, and should not have to be re-imagined when the domain of
denotation is extended for the sake of more and more complex features.
type VarName = String class Lam d where var :: VarName -> d lam :: VarName -> d -> d
The trouble is giving the meaning to these operations. None of the earlier domains will suffice: a variable does not have any fixed value associated with it; the bound value is determined only when the function is applied, which can happen many times and to different arguments. We need a new domain, reflecting that the meaning of an expression depends on its context: the environment giving the denotation to bound variables:
type DomFCF = Env -> Dom type Env = VarName -> Dom
DomFCF looks like it may work for
lam, it actually does not. The reader is invited to consider why.
What if we want call-by-name functions? Coroutines?
Non-determinism? We need more and more domains. Each new
domain requires re-writing of
ECond instances, to give the meaning
of integers, increment in these fancier domains. This is the problem: expressions do not have stable denotations. Old expressions suddenly
change meaning when the language is extended.
The theme of interactions can be traced through:
Of special note is Hewitt's influential note ``Viewing Control Structures as Patterns of Passing Messages'': it shows how recursion, iteration and `hairy' control structures can all be represented in terms of interactions between actors. One hears that all further development of process calculi is making Hewitt's ideas more precise and formal. As far as effects are concerned, the logical culmination is the work of Cartwright and Felleisen, which we reconstruct below, in modern language and in practical terms.
Carl Hewitt: Viewing Control Structures as Patterns of Passing Messages
MIT A.I. Memo 410, 1976.
Robert Cartwright, Matthias Felleisen: Extensible Denotational Language Specifications
Symposium on Theoretical Aspects of Computer Software, 1994. LNCS 789, pp. 244-272.
Cartwright and Felleisen's idea can be programmed right away:
data Comp = Done DomC | Req ReqT (DomC -> Comp) data DomC = DCInt Int | DCBool Bool | DCFun (DomC -> Comp)
From now on, an expression will mean
Comp, which is a disjoint union
DomC (similar to the old
Dom) and requests. A request always includes
the `return' address
(DomC -> Comp): the mapping from a reply to the
meaning of the recipient.
A request also includes the `payload'
ReqT, telling what
exactly is being requested. For now, the payload is
for an error message (we reveal more alternatives later).
data ReqT = ReqError ... err :: Comp err = Req ReqError (\_ -> err)The function
errsends such request, which denotes an erroneous computation. Unlike
Domin Sec. 1,
DomCno longer has the
DErrorelement. Error is now treated as an effect: a request to terminate the computation.
It is rather straightforward to give the meaning of the basic language
in terms of
Comp. We write yet another
this is the last time, however, we have to do it.
instance EBasic Comp where -- old int = Done . DCInt inc = Done . DCFun $ \x -> case x of DCInt x -> int (succ x) _ -> err app (Done (DCFun f)) (Done e2) = f e2 app (Done _) (Done e2) = err -- new app (Req r k) e2 = Req r (\x -> app (k x) e2) app e1 (Req r k) = Req r (\x -> app e1 (k x))Most of the code is similar to the
EBasic Dominstance, not surprisingly. Notably, integer literals are mapped to integers of
DomC, no matter what effects (requests) may be in the language: integers are integers forever. Likewise,
incalways means the successor on integers. New for
EBasic Compis the effect propagation in the last two
appclauses: if an argument of an application is a request the whole application means the same request, but with the modified return address: after the reply is delivered, the application is re-attempted. Indeed effects propagate from sub-expressions upwards.
The sample term
ttinc has the following meaning as
(The earlier written term was polymorphic over the domain and hence
its definition can be used as is. We repeat it below for ease of
ttinc :: EBasic d => d ttinc = inc `app` (inc `app` int 2) *EDSLNG> ttinc :: Comp Done (DInt 4)
The meaning of the conditional expression in terms of
Comp is just as
instance ECond Comp where eq = ... like inc if_ (Done (DCBool True)) et ef = et if_ (Done (DCBool False)) et ef = ef if_ (Done _) _ _ = err -- new if_ (Req r k) et ef = Req r (\x -> if_ (k x) et ef)Again, most of it is similar to the old
ECond Dominstance, except for the last line, that describes the effect propagation. It starts to look boring: This line is not much different from the effect-propagation lines for
appwe wrote just recently. Let's factor out this common pattern and write a clearer
instance ECond Comp where eq = ... if_ e et ef = bind e $ \x -> case x of DCBool True -> et DCBool False -> ef _ -> err bind :: Comp -> (DomC -> Comp) -> Comp bind (Done x) k = k x bind (Req r k1) k2 = Req r (\x -> bind (k1 x) k2)Here
bind e kexpresses the common pattern of consuming the value of
e. If that expression is not a value but sends a request, the request is propagated, with the updated return address. Looks familiar? Indeed monads arise naturally in the interaction view. In fact, Mike Spivey, pursuing the error propagation lead not unlike the one we have just shown, came up with the application of category-theoretic monads to programming languages roughly at the same time as Moggi.
Mike Spivey: A functional theory of exceptions
Science of Computer Programming, v14, 1990.
EBasic? Can the old sample term
ttinc :: Compwith its old denotation be used alongside the new effectful operations? We shall find out.
put to retrieve and update the current state were already defined,
in Sec. 1. We repeat the definitions below, along with the sample term
ttS, for ease of reference.
class GlobalIntState d where get :: d put :: d -> d ttS :: (EBasic d, ECond d, GlobalIntState d) => d ttS = if_ (eq `app` (int 3) `app` (put ttinc)) (put (int 10)) (put (inc `app` get))
To give the meaning to
put and eventually
ttS, Sec. 1 had to
introduce the special denotation domain
DomIntState, and the
EBasic and other type classes. In the new approach, the
Comp suffices. We only need to reveal more of
requests to access and update the state.
data ReqT = ReqError | ReqState StateReq ... data StateReq = Get | Put Int instance GlobalIntState Comp where get = Req (ReqState Get) Done put e = bind e $ \x -> case x of DCInt x -> Req (ReqState (Put x)) Done _ -> err
The meaning of
put hence is essentially the
get sends the request and immediately returns the reply.
Comp is unchanged, and the instances
ECond Comp have been written earlier, we can see the
ttS right away:
*EDSLNG> ttS :: Comp ReqState (Put 4)The term
ttSmeans the request to update the state to 4; the rest of the meaning (not printed by GHCi) depends on the reply to the request. This is the best one can do since there are not any request handlers yet. The
ReqErroris not meant to be replied to: an unhandled request always signifies an error. On the other hand, one should reply to
ReqState, and access and update the global state as requested.
handleState :: Int -> Comp -> Comp handleState _ (Done x) = Done x handleState s (Req (ReqState r) k) = case r of Get -> handleState s $ k (DCInt s) Put s -> handleState s $ k (DCInt s) -- everything else handleState s (Req r k) = Req r (handleState s . k)
handleState is the authority that Cartwright and Felleisen
were talking about, in charge of resources -- state in our case -- and
replying to requests. When the computation to handle is
Get request, the handler replies with the current state,
and continues handling the replied-to computation in case it has other
requests. The last line in
handleState deals with requests other than
ReqState; they are propagated up, or, `sent to a higher authority'.
This line is the difference of our approach from Cartwright and Felleisen:
to us, there is no central authority stationed outside the program.
Our handlers are part of the program, forming a bureaucracy. What one cannot
handle gets sent to a superior.
The sample expression
ttS with the state handler in the initial
state 0, that is,
handleState 0 ttS has the meaning of
DInt 5. We
have already pointed out that the handler is recursive: after
receiving a reply, an expression may send further requests, to be
handled in turn. Strictly speaking therefore, the mathematical mapping
established by handlers is a fixpoint -- and we have to implicitly
Done bottom for a non-terminating handling computation. We
saw no bottoms before since we had no divergent
computations. Incidentally, an expression that sends an unending
Get requests is not divergent: its meaning is the productive stream of requests.
Thus the Cartwright and Felleisen's idea really works! We have added a real effect without having to re-write any of the earlier domains and interpreters. One may just as painlessly introduce other sorts of mutable state, or other effects in general. Integer literals always mean integers, and can be used as such within arbitrary effectful expressions. Cartwright and Felleisen's idea works even better than the authors have described: we made the handlers themselves be modular, each responsible for its own requests.
Sec. 1 introduced first-class functions with the following
operations, demonstrated through the sample term
type VarName = String class Lam d where var :: VarName -> d lam :: VarName -> d -> d th0 = lam "x" (inc `app` var "x") -- increment (eta-expanded)We now give the meaning of
lamin terms of
Comp. The operation
varto access the bound value feels quite like the
getoperation earlier to access the current state. Since the bounding is not mutated, it is better thought of as the environment rather that the state. Unlike the global state earlier, the bound environment is local to an application. Here it really helps that in our framework (unlike Cartwright and Felleisen's) handlers may appear in expressions. That is enough hints to write down the semantics: the interpretation of
varas the sender of
ReqHOrequests (similar to
Get, but parameterized by the variable name); the interpretation of
lamas the function that receives an argument and handles, through
ReqHOrequests for its bound variable raised within its body.
data ReqT = ReqError | ReqState StateReq | ReqHO HOReq data HOReq = ReqVar VarName instance Lam Comp where var v = Req (ReqHO (ReqVar v)) Done lam v body = Done . DCFun $ \x -> handleVarD [(v,x)] body type Env = [(VarName,DomC)] handleVarD :: Env -> Comp -> Comp handleVarD _ (Done x) = Done x handleVarD env (Req (ReqHO (ReqVar v)) k) | Just x <- lookup v env = handleVarD env $ k x -- everything else handleVarD env (Req r k) = Req r (handleVarD env . k)
It does seem to work, for example,
th0 `app` ttinc :: Comp has the
expected meaning of integer 5. However,
*EDSLNG> (lam "z" (lam "x" (var "z" `app` var "x"))) `app` inc `app` int 1 :: Comp ReqHO (ReqVar "z")(which is a fancy way of computing
inc 1) unexpectedly has as its meaning the request for the value bound to the variable
z-- that is, the unbound variable error. Can the reader guess what went wrong?
Let us look again at the salient parts of the dynamic-binding code we wrote just before:
lam v body = Done . DCFun $ \x -> handleVarD [(v,x)] body handleVarD env (Req (ReqHO (ReqVar v)) k) | Just x <- lookup v env = handleVarD env $ k x handleVarD env (Req r k) = Req r (handleVarD env . k)Creating a first-class function is straightforward: mere wrapping the body of the function in the handler that responds to requests for the value of the lambda-bound variable
bodyhas variables besides
v, those requests will propagate out of our
handleVarD [(v,x)]and should be handled by other handlers in (dynamic) scope. Creating a first-class function therefore requires no context information and no context interaction. We may call such an operation pure. On the other hand, applying the first-class function to a value may give rise to
ReqVarrequests (for the variables other than
v). The function application hence is not context-invariant: it is effectful.
With lexical scope, it is the other way around. Recall, a lexically-scoped function captures the variable environment (the binding context) at the point of its creation: as Landin would say, closes over the context. Therefore, building a closure does depend on the context and is, by our definition, effectful. When the closure is applied, this captured environment is used to satisfy all variable dereference requests:
data ReqT = ReqError | ReqState StateReq | ReqHO HOReq data HOReq = ReqVar VarName | ReqClosure VarName Comp type Env = [(VarName,DomC)] instance Lam Comp where var v = Req (ReqHO (ReqVar v)) Done lam v body = Req (ReqHO (ReqClosure v body)) Done handleVar :: Env -> Comp -> Comp handleVar _ (Done x) = Done x handleVar env (Req (ReqHO r) k) = case r of ReqVar v | Just x <- lookup v env -> handleVar env $ k x ReqVar _ -> err -- unbound variable ReqClosure v body -> handleVar env $ k (DCFun $ \x -> handleVar ((v,x):env) body) -- everything else handleVar env (Req r k) = Req r (handleVar env . k)
Now the body of the function is enclosed into
ReqVar requests not just for
v (the variable bound
by the lambda that created the closure) but for all other variables
body. Therefore, when the closure is applied, no variable
requests propagate outside the closure and need to be handled by
the context. The closure application therefore is context-invariant: the
closure is pure.
On the other hand, to create a closure we must inquire the context
about all variables bound in it. Capturing the environment thus is an effect. The
lam form initiates the capture, sending the
ReqClosure v request. When it reaches a
handleVar interpreter --
which, recall, contains the complete information about the
variables bound within its scope -- the interpreter creates the closure by
passing down its variable environment to the handler for the function's
body. The top-level
passes the empty environment, since no variables are
supposed to be bound at top-level. Now,
handleVar  $ (lam "z" (lam "x" (var "z" `app` var "x"))) `app` inc `app` int 1 :: Comphas the desired meaning: the integer 2.
We have just demonstrated that
even the addition of lexically-scoped first-class functions preserves the
denotations of the earlier-defined features. The increment
inc still means the
successor and integer literals still mean integers, whether they appear
within function bodies or not. Our denotations evoke embeddings of
lambda-calculus in pi-calculus. The perhaps unexpected feature of
our semantics is that
lam is treated as an effect. One should not be too
surprised: after all, closure creation does have to interact with the context
and does have to allocate space for the environment. It is not an accident
that the language ATS likewise treats closure creation as an effect.
ReqTas if it were extensible. Haskell data types are not extensible; the source code accompanying the article had to define the request types upfront. That is not the practically viable.
Luckily, it does not take too much pain to introduce an extensible request
type, by nesting co-product (
Either type). The
library of Extensible Effects in Haskell and other languages do exactly
that. The end result is truly extensible -- and typed -- framework
that lets our programs have a desired effect.
Whether something is side-effect or not, is thus a matter of perspective. When focusing on a small part of computation, all interactions with the context -- be they accessing an external memory or accessing a bound variable -- are a side-effect. Even lambda may be regarded as an effect, of closure creation.
Should we regard Lambda or State as an effect depends on the task at hand: are we evaluating an expression or compiling it, are we interested only in expression's result or also in the time to compute it. Effects hence emerge as a convenience and an abstraction, letting us focus on one part of the whole system, abstracting the rest as ``the context'' to be interacted through a fixed protocol. Different protocols allow different degrees of equational reasoning. That is why it is so important, when it comes to effects, is to be explicit and to be aware.
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML