It may well be that interaction is best expressed in a process calculus. In sequential calculi, Cartwright and Felleisen's ``Extensible Denotational Language Specifications'' is the earliest fully worked-out rigorous presentations of effects as interactions.
Revisiting the origins of the field and recovering the insights and forgotten alternatives help make our programs have the intended effect.
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 and Matthias Felleisen are gratefully acknowledged.
edlsng.ml [12K]
The OCaml version: the modern reconstruction of the Cartwright-Felleisen framework. State, dynamic binding, call-by-value and call-by-name lexical binding are the sample effects.
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 the stumbling block for using denotational semantics in studying and defining real-life languages and their effects, as was first noted by John Reynolds back in 1974. 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 tinc:
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 Expr. Recall,
denotational semantics is a compositional mapping from Expr to
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 Expr to
their denotations Dom, is then defined constructively, as the Haskell
function 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)
_ -> DError
Whereas EApp EInc (EInt 8) signifies the phrase (a mere string) inc 8 in our language, DInt 9 is its meaning, a
Haskell integer. The last clause of eval shows off compositionality:
the meaning of EApp e1 e2 depends only on eval e1 and eval e2:
that is, on the meaning of the arguments e1 and 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
re-define Expr to accommodate the extensions:
data Expr = EInt Int | EInc | EApp Expr Expr
| EEq | EIf Expr Expr Expr
A sample conditional
expression if 3 == inc (inc 2) then 10 else inc (inc (inc 2)) looks as tif below. We want to re-use the previously defined tinc
for inc (inc 2) but cannot: the type Expr has changed.
We have to re-define tinc using 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 eval gives 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 eval step. 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-associative
The type class says that our language has two primitives, integer literals
and the increment, and one compound expression, app with two sub-expressions.
The meaning of the compound is determined from the meaning d of 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: ttinc is the term in the EBasic language. Or: given an appropriate
domain -- that is, to which we may map the primitives and compounds
of the language -- ttinc gives the meaning of the phrase inc (inc 2)
in that domain. What remains is to tell that Dom is `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 _ _ = DError
where we write injI succ for the Haskell successor function lifted to Dom, returning DError if the value to increment is not a DInt.
The meaning of the sample expression is thus ttinc :: Dom, that is, ttinc specialized to the domain type Dom.
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 -> d
The 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
ttinc without
re-writing it. Likewise, we re-use, rather
than re-write the interpreters. The inferred type of ttif, (EBasic d, ECond d) => d, tells that to make sense, it needs
the domain mappings for the basic and the conditional primitives. The EBasic Dom mapping 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 -> d
The 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 ttS is much harder
than writing it. Onto which Dom element 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 get and put becomes easy to express: get
stands 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., app:
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 Dom interpretation
of if_.
The problem is not in the complexity of writing the EBasic, ECond,
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 EBasic, 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 EInt
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
Although DomFCF looks like it may work for var
and 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 EBasic, 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
of 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 ReqError, standing
for an error message (we reveal more alternatives later).
data ReqT = ReqError ...
err :: Comp
err = Req ReqError (\_ -> err)
The function err sends such request, which denotes an erroneous
computation. Unlike Dom in Sec. 1, DomC no longer has the DError
element. 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 EBasic instance;
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 Dom instance,
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, inc
always means the successor on integers. New for EBasic Comp is
the effect propagation in the last two app clauses: 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 Comp.
(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
reference.)
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
straightforward:
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 Dom instance, 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 app we wrote just recently. Let's factor out this common
pattern and write a clearer ECond Comp instance: 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 k expresses 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 :: Comp with its old
denotation be used alongside the new effectful operations?
We shall find out.
The operations get and 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 get, put and eventually ttS, Sec. 1 had to
introduce the special denotation domain DomIntState, and the
corresponding instances
of EBasic and other type classes. In the new approach, the
earlier defined Comp suffices. We only need to reveal more of ReqT:
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 get and put hence is essentially the ReqState request:
for example, get sends the request and immediately returns the reply.
Since Comp is unchanged, and the instances EBasic Comp
and ECond Comp have been written earlier, we can see the
meaning of ttS right away:
*EDSLNG> ttS :: Comp
ReqState (Put 4)
The term ttS means 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 ReqError is 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)
The handler 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
the 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 localized: 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
introduce 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
stream of 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 th0:
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 var and lam in terms of Comp. The operation var to access the bound value feels quite like the get operation 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 var as the sender of ReqHO requests (similar to Get, but parameterized by the variable name); the interpretation of lam as the function that receives an argument and handles, through handleVarD, ReqHO requests 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 v. If body has
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 ReqVar requests (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 handleVar ((v,x):env),
which handles ReqVar requests not just for v (the variable bound
by the lambda that created the closure) but for all other variables
within 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 handleVar []
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 languages FX and ATS likewise treat the closure creation as an effect.
ReqT as 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.
We demonstrate that first-class abstractions may be treated uniformly as any other effects, thus completing the Cartwright and Felleisen's program of ``Extensible Denotational Language Specifications'': Variable substitution is indistinguishable from the dereference of a C-like variable; ``lambda'', or creating a closure, is an effect as well. The (lexical) closure acts as a handler of all variable dereference effects arising during the execution of its body. Our approach uniformly handles dynamic and lexical binding and various calling conventions.
Like call-by-push-value and the languages ATS or FX, we regard a lambda-abstraction as an effectful expression. Unlike these calculi and languages, we treat a variable as an effectful expression as well. Bound variables are essentially single-assignment reference cells allocated in first-class storage. This is how they are typically compiled in machine code. Our approach hence promises a faithful description of distributed and heterogeneous systems, where variable dereference is a non-trivial effect.
It is customary to design a language with effects as an extension of lambda-calculus, with the following, familiar typing judgment:
Gamma |- M : T e athat an expression
M has the type T e a. Here, a is the type
of the value produced upon the successful evaluation of M, and e describes the effects that M may perform while at it. (T is the
two-argument type-constructor: think of an (effect-indexed) monad.) Gamma is the familiar typing environment, telling the types of
free variables in M. We modestly propose to simplify the type judgment,
to mere|- M : T e athat is, to remove the typing environment -- as well as the lambda-calculus as the starting point. How to judge then the type of, say,
x + 1, where x is a free variable?
Whence come the type of x? Let's contemplate ask + 1.
To type such effectful expression
we need to suppose that ask is an effectful operation producing
an integer. We thus write: |- (ask+1) : T {ask:int} int
taking the effect annotation {ask:int} as a binding
for the effect operation ask within the expression: as the
typing environment for effects. Dereferencing a variable is also an effect!
Therefore, we may well write |- (x+1) : T {x:int} int
|- (ask+x) : T {x:int, ask:int} int
|- lambda x. (ask+x) : T {ask:int} (int->int)
|- handle (ask+x) with ask => 10 : T {x:int} int
Since the effect annotation serves as the binding environment for
yet to be handled effects, it may as well describe the types for
yet to be bound variables. Gamma indeed becomes redundant.
The whole program P should be closed:
|- P : T {} a
it should have no unbound variables -- nor unhandled effects.All in all, a framework like extensible-effects that supports multiple effects should not hence have any problem with abstraction and substitution effects -- which gives HOPE.
edlsng.ml [12K]
The OCaml version: the modern reconstruction of the Cartwright-Felleisen framework. State, dynamic binding, call-by-value and call-by-name lexical binding are the sample effects.
EDSLNG.hs [11K]
The essentially Haskell98 version of the code
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.
oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML