previous   next   up   top

Having an Effect

 

Introduction
 
1. Unstable Denotations
2. Effects and Interactions
 
3. Stable Denotations, Extensible Effects
4. Higher-order Programming is an Effect
5. Conclusions

 

Introduction

This research has been a journey following the tantalizing lead: the founding papers on monads, monad transformers, free monads and extensible-effects were all about extensible interpreters. Along the way we have realized that the expression problem, stable denotations, and extensible interpreters are all different names for the same thing. We have eventually found the organizing principle: interaction -- between a client and a server, an interpreter and the interpreted code, an expression and its context.

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.

Version
The current version is September 2017.
References
EDSLNG.hs [11K]
Complete, essentially Haskell98 code underlying the talk

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 >


1. Unstable Denotations, Brittle Interpreters, Hard-to-apply Theory

 

Denotational Semantics, from a `practical' perspective

Since (side-) effects are ubiquitous and controversial, they ought to be studied. And they have been, notably, by the Vienna School of Denotational Semantics in the 1970s -- with the goal to make sense of PL\1. We too will be using the denotational semantics -- but with the practical bent, towards (definitional) interpreters. It eventually leads us to `extensible effects' -- a practical way of managing effects in real-life programs.

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.

 

Definitional interpreters

We explain the definitional interpreter approach to denotational semantics on the embarrassingly simple example. Trivial as it is, the example already makes the case for extensible interpreters.

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.

 

Extensible interpreters

Let us go back to the simplest language of integers and increments, and define it differently. Instead of a data type, which then has to be interpreted as 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.

 

Defining State

This subsection adds the first real effect to the language of increments and conditionals: global mutable integer state. It also brings us face-to-face with the real problem of denotational semantics.

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.

 

First-class functions?

First-class functions are just as easy to add as the state, at least at the outset. We just write down the signature of the basic operations: accessing a value bound to a (named) variable, and creating a function.
     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.


2. Interactions

 

Effects and Interactions

Unstable denotations reflect the interactions of an expression with its context. The traditional approach to the semantics of programming languages, from Landin and Strachey onwards, had little to say about interactions. Robin Milner put it well in his interview: ``But meanwhile [around 1971] I got somehow interested, and I don't know how, in concurrency. I remember that, without linking it to verification particularly, I wondered about interacting automata. I had an idea that automata theory was inadequate, because it hadn't said what it was for two automata to interact with each other. Except for the Krohn-Rhodes Representation Theorem, which said something about feeding the output of one automata into another. But there wasn't interaction between the automata.''

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.

References
Robin Milner interview
< http://users.sussex.ac.uk/~mfb21/interviews/milner/ >

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.

3. Stable Denotations, Extensible Effects

 

Towards Stable Denotations

We now define the meaning of expressions in the way that explicitly accounts for their interactions with the context. We follow the lead of Cartwright and Felleisen: ``A complete program is thought of as an agent that interacts with the outside world, e.g., a file system, and that affects global resources, e.g., the store. A central authority administers these resources. The meaning of a program phrase is a computation, which may be a value or an effect. If the meaning of a program phrase is an effect, it is propagated to the central authority. The propagation process adds a function to the effect package such that the central authority can resume the suspended calculation.''

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.
References
Eugenio Moggi: Computational lambda-calculus and monads
LICS 1989.

Mike Spivey: A functional theory of exceptions
Science of Computer Programming, v14, 1990.

 

State, painlessly

So far, the only effect has been error propagation. The moment of truth for the new approach comes when we add a real effect: global mutable integer state. Do we need to write yet another instance of 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.

 

First-class functions, first attempt

Earlier in Sec. 1 we tried to extend the language with first-class functions, which turned out to require so deep and numerous modifications that we gave up. Let us try again, in the framework of stable denotations. What we are about to do has not been done before in the effect-as-interactions framework.

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?

 

First-class functions, with lexical scope

The first attempt to give meaning to first-class functions within the stable denotations framework ran into the predictable problem: we have unwittingly implemented dynamic rather than lexical scope for bound variables. It is uncanny how `natural' dynamic binding is: it is the first that comes to mind when implementing lambda-calculus. No wonder that both John McCarty and Alan Turing made this mistake. Lexical bindings take quite a bit more effort to recognize and implement. After all, the term closure was introduced by Landin only in 1964, some 20+ years after lambda-calculus was published.

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 :: Comp
has 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.

 

Extensible Effects

An attentive reader must have noticed that we have implicitly treated the data type of requests 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.

References
Extensible Effects: an alternative to Monad Transformers
See specifically Sec. 2.5 of the paper ``Freer Monads, More Extensible Effects''

 

Higher-order Programming is an Effect

We argue that the central problem of the interaction of higher-order programming with various kinds of effects can be tackled by eliminating the distinction: higher-order facility is itself an effect, not too different from state 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 a
that 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 a
that 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.

Version
The current version is September 2017.
References
HOPE-talk.pdf [164K]
The slides of the talk presented at the HOPE workshop affiliated with ICFP 2017. September 3, 2017. Oxford, UK

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

 

Conclusions

What is an effect then? It is an interaction with the context. An expression is effectful if it sends messages to the context. A lexically-scoped lambda has to ask the context for the binding environment, and is hence effectful. The body of a closure, when evaluated, sends requests for the values of its free variables. The entire closure, however, satisfies all such variable requests and (absent state, IO, etc) requires no further context interactions. The closure is therefore ineffectful, pure.

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.



Last updated September 13, 2017

This site's top page is http://okmij.org/ftp/

oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!

Converted from HSXML by HSXML->HTML