previous   next   up   top

Extensible Effects: understanding them, implementing them, using them. A Tutorial

 

Effects is a model of side-effects as an interaction between a program and a handler: an authority in charge of resources that receives and acts on program requests. Effects let us represent side-effects in pure computations. The explicitness about possible and not possible side-effects, the localized handling, controlled interactions and encapsulation, the ease of reasoning make effects useful even in impure languages, which can do side-effects natively.

There are several implementations of effects in Haskell and Scala. Effects are natively supported in Idris and soon to be in OCaml. They are the defining feature of PureScript. Finally, the language Eff is built on algebraic effects and local effect handling. By nature effects are extensible, letting us easily combine in the same program independently developed components, each with their own effects. In the narrow sense, extensible-effects refer to a specific implementation method, often used in Haskell, Scala, and even in Coq.

This tutorial aims first to explain the ideas behind the extensible effects, on simple to understand toy implementations. Then, using one real, optimized implementation, we will experience defining and handling various effects, on progressively more complex examples.

This tutorial has been presented at the Commercial Users of Functional Programming (CUFP) conferences (affiliated with ICFP): on September 22, 2016 in Nara, Japan and on September 7, 2017 in Oxford, UK.

Overview
Re-discovering extensible-effects for themselves
Applications
Further Pointers

 

Goals

This tutorial will remind what you already knew: effects come from interactions. We will develop this intuition into a practical approach, a library for effective effectful programming. We get to define effects (interaction protocols), handle them, and control their scope and interplay.

Hopefully, you would come to think of effects not as 'Lifting a State through an Error', not even as monads -- but as protocols of interaction with the context. (To be sure, we will encounter monads -- just as we will encounter addition, which is rather more interesting.)

For concreteness, the tutorial uses Haskell. The tutorial part strives for a simple subset of Haskell that could be easily mapped to other functional languages such as Scala or OCaml. At the end, you should be able to write your own library of effects in your preferred language.

The tutorial is meant to be interactive, working through problems with active audience participation. It will be very helpful for the participants to have a laptop with GHC installed. No libraries and packages beyond the standard library is needed.

Re-discovering extensible-effects for themselves

 

What it means to treat effects as interactions and how to program with that

The key idea of effects as interactions is already familiar. Whenever a program is to read from a file, write on a terminal, obtain the current time -- to have any notable effect at all -- it asks the OS kernel. By a system call it sends a request to the kernel, describing the desired effect and its parameters. Having received a request, the kernel checks and acts on it, suspending the program in the meanwhile. When the requested action is completed, the result is passed to the resumed program. (The resumption is not guaranteed -- think of exit -- or may occur twice -- think of fork.) The insight of algebraic-, extensible-, etc. effects is that operations within the program may also be understood as request-response interchanges -- between an expression and a the request handler in its context. Let us see what exactly it means.

We start with a simple language that has integer literals, addition, and the operation to obtain an integer from the context (think of reading a configuration parameter). The language specification can be written in Haskell as

     class ReaderLang d where
       int :: Int -> d
       add :: d -> d -> d
       ask :: d
       
which can be read in two ways. First, one may take the class ReaderLang as a notation for the context-free grammar of the language, reading d as the non-terminal for expressions and int, add, ask as the grammar terminals. The following is a sample expression of ReaderLang (with the name rlExp attached for ease of reference.)
     rlExp = add ask (add ask (int 1))

One may also view the class ReaderLang as the blueprint for determining the meaning of language expressions: int is to tell the meaning of integer literals and add is to tell how to combine the meanings of two argument expressions to obtain the denotation for the addition. The type variable d is a yet-to-be-specified semantic domain.

To interpret rlExp we have to pick the semantic domain. There are many choices, for example, Int->Int functions. We advocate a powerful domain construction described in the unfortunately obscure 1994 paper ``Extensible Denotational Language Specifications'' (hereafter, EDLS) by Robert (Corky) Cartwright and Matthias Felleisen. The paper lays out the construction clearly and insightfully. Here are a few memorable quotes:

``The schema critically relies on the distinction between a complete program and a nested program phrase. 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. We refer to this component of an effect package as the handle since it provides access to the place of origin for the package.

``The central authority is implemented via the function admin. It performs the actions specified by effects. Actions can modify resources, can examine them without changing them, or may simply abort the program execution. Once the action is performed, the administrator extracts the handle portion of the effect and invokes it, if necessary. The handle then performs whatever computation remains following the action of the effect. Thus, at top-level a handle is roughly a conventional continuation.

``An effect is most easily understood as an interaction between a sub-expression and a central authority that administers the global resources of a program. Examples of such resources are stores, heaps, file systems, the place for the final result of a program, and other input/output channels. Given an administrator, an effect can be viewed as a message to the central authority plus enough information to resume the suspended calculation.''

At times the paper reads like a course in Operating Systems for denotational semanticists. The paper then goes on to set up the rigorous denotational semantics along the quoted lines (see p7 of EDLS). Let us rewrite them in Haskell.

Once again, ``The meaning of a program phrase is a computation, which may be a value or an effect.... an effect can be viewed as a message to the central authority plus enough information to resume the suspended calculation.'' In Haskell words:

     data CRead = CRVal Int | Get0 (Int -> CRead)

A (non-effectful) program phrase means a value, to be represented by the variant CRVal (all values are integers, in our simple language). Get0 is the effect: the meaning of a phrase that asks the context (`the authority') for the implicit integer. The request contains the `return address', describing the computation after receiving the central authority's response (as the function of the response value). The entire CRead data type is hence meant to express the meaning of our language phrases. In other words, CRead is meant to be an instance of ReaderLang:

     instance ReaderLang CRead where
       int x = CRVal x
       ask   = Get0 CRVal       -- or, expanded: Get0 (\x -> CRVal x)
     
       add (CRVal x) (CRVal y)  = CRVal (x+y)
       add (Get0 k)   y         = Get0 (\x -> add (k x) y)
       add x         (Get0 k)   = Get0 (\y -> add x (k y))

Integer literals int n literally mean n. Likewise, ask is the request whose resumption immediately returns the requested value. The binary operation add combines the meanings of its operands: if both mean values, the addition means their sum. When the first argument is the request Get0 k -- a computation that may yield an integer after interactions with the context -- we have to wait until the interactions are finished. We relay the request, pass the reply to the remainder k of the argument expression, and add that. Effectively, the request from a sub-expression `bubbles-up', just as EDLS on p.8 says.

It is not too difficult to work out that the sample expression rlExp means a Get0 effect. That is not helpful: we cannot even print the denotation. (Why?) That rlExp does not have a `useful' result should not be surprising: it is not the whole program. We have not yet written the `authority', which receives and satisfies Get0 requests. EDLS on p.11 outlines the authority, which they call admin. To put those ideas into Haskell:
     runReader0 :: Int -> CRead -> Int
     runReader0 e (CRVal x)  = x
     runReader0 e (Get0 k)   = runReader0 e $ k e
The runReader0 authority takes an integer e (`the managed resource', the implicit integer to serve) and the computation to administer. If the computation means (an integer) value, there are no requests to fulfill. On the other hand, if the computation asks for an integer, we pass it e and handle the remainder (which may send more requests).

We can now determine what rlExp means in the context (under authority) of runReader0 given the particular value e. Just like the meaning of an OS process depends on the context (the contents of the file system, etc) so does the meaning of effectful expressions. The result is shown in the comments.

     runReader0 2 rlExp
     -- 5
Version
The current version is September 2016.
References
Tutorial1.hs [3K]
The complete source code

Robert Cartwright, Matthias Felleisen: Extensible Denotational Language Specifications
Symposium on Theoretical Aspects of Computer Software, 1994. LNCS 789, pp. 244-272.
< http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.5941 >

 

Generalizing: arbitrary effects, arbitrary interpreters

We have seen how to model one effect as a request-reply interaction of an expression and a request handler (interpreter). Let us generalize, from a Get0 request for an integer to arbitrary effects with arbitrary return types.

The EDLS paper by Cartwright and Felleisen has, in fact, shown the general solution (on p.7). The idea is still the same: ``The meaning of a program phrase is a computation, which may be a value or an effect.... an effect can be viewed as a message to the central authority plus enough information to resume the suspended calculation.'' We now stress that different computations may have values of different types; different effects carry different messages, each with their own response type. We generalize the CRead data type of the previous section correspondingly:

     data Comp req a where
       Val :: a   -> Comp req a
       E   :: req x -> (x -> Comp req a) -> Comp req a

(This data type declaration is in the new-style GADT syntax although it is not a GADT. It is an existential, however, which looks cleaner in the new syntax: see below.) Like CRead earlier, the data type Comp expresses the meaning of a computation as either a value Val x or an effect E req k. Comp is first parameterized by the type of the value a and then by the type of the request message req. A request message type is a collection of, generally, several request messages, each with its own response type. For example, a hypothetical request type ReqIO may contain the message GetChar with the response type Char and the message PutChar with the response type (); the latter has a payload: the character to print. Such ReqIO type is written in Haskell as a GADT (GADTs are designed to express API interfaces):

     data ReqIO x where
       GetChar :: ReqIO Char
       PutChar :: Char -> ReqIO ()
The request message type like ReqIO hence is not, strictly speaking, a type: rather, it is a type constructor (in Haskell terms, of the kind * -> *). The computation type Comp is parameterized by this constructor. In the effect denotation E r k :: Comp req a, the request r of the type req x, and the resumption k:: x -> Comp req a naturally have to agree on the response type x, which varies with r. It is a matter of a private agreement, so to speak: x need not be mentioned in the type of the computation (a Comp ReqIO Int expression may hence perform both GetChar and PutChar requests). Therefore, x is an private, existential type. (The denotational construction in EDLS is untyped; making it typed, in Haskell, is our elaboration.)

The general Comp data type describes the meaning of ReaderLang expressions just as well as the made-to-order CRead. First, we define the type of ReaderLang's requests, with a single message GetI, for an implicit integer:

     data GetI x where
       GetI :: GetI Int
(as common in Haskell, the name of the message GetI and the request type GetI are spelled the same, although they are different things. One can tell from the context -- term or type -- which is which.) The meaning of ReaderLang expressions can now be stated in terms of Comp GetI Int:
     instance ReaderLang (Comp GetI Int) where
       int x = Val x
       ask   = E GetI Val
     
       add (Val x) (Val y)  = Val (x+y)
       add (E r k)   y      = E r (\x -> add (k x) y)
       add x       (E r k)  = E r (\y -> add x (k y))
which should not be too surprising since Comp GetI Int is isomorphic to the CRead data type of the previous section.

We want further generalizations: We want a language with more types than just integers, and more operations than just the addition. Before extending ReaderLang with, say, subtraction, booleans and comparison, let us take a closer look at the meaning of add, repeated below:

     add (Val x) (Val y)  = Val (x+y)
     add (E r k)   y      = E r (\x -> add (k x) y)
     add x       (E r k)  = E r (\y -> add x (k y))

Of the three cases in the definition, only the first deals with the summation. The other two are the boilerplate of the effect propagation -- the boilerplate that begs to be factored out. In fact, it is factored out in EDLS (p.7), under the name of `handler'. We give that function a more conventional name:

     bind :: Comp req a -> (a -> Comp req b) -> Comp req b
     bind (Val x) f = f x
     bind (E r k) f = E r (\x -> bind (k x) f)
(To see the correspondence with EDLS even closer, keep in mind that we write Val for what EDLS calls inV: the inclusion/retraction of values into the Comp domain.) With the effect-propagation factored out, add takes the form
     add e1 e2 = bind e1 $ \x ->
                 bind e2 $ \y ->
                 Val (x+y)
At this point one may wonder why we need add if we can use bind directly, to implement not just the addition but any other operation on effectful expressions. (Actually, there is still a good reason to use an algebraic specification like ReaderLang: there are interesting and useful ways to define the semantics of add that cannot be expressed in terms of bind. But this is a talk for another time.) In the following, we shall use bind directly.

While in the generalization spirit, let's make GetI ask not just for integers but for values of an arbitrary type. The new request type Get is parameterized by the type e of asked values:

     data Get e x where
       Get :: Get e e
which lets us re-define ask more generally:
     ask :: Comp (Get e) e
     ask = E Get Val

It is still a request for an implicit value from the context, which is no longer restricted to be an integer. The operation bind has been defined already in the general form, for any request req. The old rlExp example -- which asks for two integers and computes their sum incremented by one -- may no be re-written, under the name rlExp2, as:

     rlExp2 :: Comp (Get Int) Int
     rlExp2 =
       bind ask $ \x ->
       bind ask $ \y ->
       Val (x + y + 1)
Having introduced bind, we may as well drop the other shoe and rename bind into >>=, as it is commonly known in Haskell (also renaming Val into return). We then get to use the convenient do-notation:
     rlExp2 :: Comp (Get Int) Int
     rlExp2 = do
       x <- ask
       y <- ask
       return (x + y + 1)

The renaming pre-supposes that Comp req is a monad:

     instance Monad (Comp req) where
       return = Val
       (>>=)  = bind
(The needed Functor and Applicative instances are left as an exercise.) Comp req is indeed a monad -- a Free(r) monad. We now can conveniently program with effectful expressions, using any needed operation and re-using already written expressions:
     rlExp3 :: Comp (Get Int) Int
     rlExp3 = do
       x <- rlExp2
       y <- ask
       return (x * y - 1)
     
     rlExp4 :: Comp (Get Int) Bool
     rlExp4 = do
       x <- rlExp3
       y <- ask
       return (x > y)

The other side of interactions -- request handlers -- also have room for generalization. The runReader0 handler of Get0 requests from the previous section now reads

     runReader :: e -> Comp (Get e) a -> a
     runReader e (Val x)   = x
     runReader e (E Get k) = runReader e $ k e
     
     _ = runReader 2 rlExp2 :: Int
     -- 5

The code is the same (modulo the replacement of Get0 with Get). The type signature is more general: the asked value, and the return value of the computation are not restricted to integers. The new runReader can handle rlExp2, and also rlExp3 and rlExp4 (the latter produced a boolean):

     _ = runReader 2 rlExp3 :: Int
     -- 9
     
     _ = runReader 2 rlExp4
     -- True

The further generalization is perhaps less expected -- especially if we are too used to the monadic view, where there is usually only one way to `run' a monad. From the standpoint of EDLS (and its followers like extensible-effects), an effectful expression does not `do' anything -- rather, it asks for it. It is a request handler that does the doing. There is generally more than one way to interpret a request. The runReader e interpreter gives the same reply e on each Get request -- realizing the so-called `environment', or `reader' effect. Get requests may also be handled differently, for example:

     feedAll :: [e] -> Comp (Get e) a -> Maybe a
     feedAll _ (Val a) = Just a
     feedAll []   _    = Nothing
     feedAll (h : t) (E Get k)   = feedAll t (k h)
The `managed resource' is now a list of values. Each time the administered computation asks for a value, we give the next one from the list. Chances are, the list is exhausted before the program stops asking. Therefore, feedAll is partial, returning Nothing is the latter case. The earlier expression rlExp3 interpreted with feedAll has a different meaning:
     _ = feedAll [2,3,4] rlExp3 :: Maybe Int
     -- Just 23
Under this interpretation, the Get effect is like getchar in C; ask may hence be regarded as a primitive parser. Later on, we will indeed write real parsers with ask.

To strengthen what we have learned and to demonstrate the generality of the approach, let's define another effect. Whereas Get was asking the context for a value, we will now be telling the context a value (e.g., to log it), which becomes the payload of the effect message. Formally, the request message and its type are defined as:

     data Put o x where
       Put :: o -> Put o ()
The helper function:
     tell :: o -> Comp (Put o) ()
     tell x = send (Put x)
makes Put easier to use, where send below makes writing helpers easier:
     send :: req x -> Comp req x
     send req = E req return

Declaring the request type (and, optionally, defining the helper like tell) is all we need to do to introduce a new effect. It can be used right away, for example, for simple logging:

     wrExp :: Show a => Comp (Put String) a -> Comp (Put String) ()
     wrExp m = do
       tell "about to do m"
       x <- m
       tell (show x)
       tell "end"

One may interpret Put by recording all told values, returning them as a list at the end, when the handled expression has nothing more to tell:

     runWriter :: Comp (Put o) x -> ([o],x)
     runWriter (Val x) = ([],x)
     runWriter (E (Put x) k) =
       let (l,v) = runWriter (k ()) in
       (x:l,v)
Under this interpretation the logging example produces the result as shown in the comments underneath:
     _ = runWriter (wrExp (return 1))
     -- (["about to do m","1","end"],())

QUIZ: What other Put interpreters can you write?

In conclusion, we have put the intuition of effects as interactions into practice, as a framework to define, use and handle arbitrary effects. We have seen the connection to the free(r) monads. We will now learn how to combine effects.

Version
The current version is September 2016.
References
Tutorial2.hs [6K]
The tutorial source code

Free and Freer monads

 

Extensibility

The ideal of extensibility is to easily combine in the same program independently developed components, each with their own effects. This is not at all easy: for example, since monads do not compose, they leave the extensibility unsolved (as was made clear when monads were introduced into functional programming). We shall see how extensible-effects make the composition possible. Concretely, we will learn to combine the earlier defined Get and Put effects and handle them separately and together.

(To be written up. See the source code in the meanwhile.)

Version
The current version is September 2016.
References
Tutorial2.hs [6K]
The tutorial source code

Free and Freer monads

OpenUnion52.hs [5K]
One of the implementations of open unions. There are others, with the same interface but different implementation: whether OverlappingInstances are used or not, whether unsafe shortcuts are used for the sake of performance, etc.

Detailed explanation of open unions

Using extensible-effects: notable applications

 

Non-determinism with committed choice

A realistic example using an `industrial-strength' extensible-effects library. That is not the only efficient library for programming with effects. You can find several more on Hackage -- or even write your own.
References
Tutorial3.hs [10K]
The tutorial source code

OpenUnion52.hs [5K]
One of the implementations of open unions. There are others, with the same interface but different implementation: whether OverlappingInstances are used or not, whether unsafe shortcuts are used for the sake of performance, etc.

 

IO errors and the current state

Catching of dynamic and asynchronous exceptions in the presence of other effects -- the solution of the MonadCatchIO problem.
References
EffDynCatch.hs [5K]

 

Monadic Regions

Monadic regions through extensible effects. The test code is essentially the same as that of the original Monadic Regions implementation.
Version
The current version is May 2015.
References
EffRegion.hs [11K]
EffRegionTest.hs [10K]


Last updated October 10, 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