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, which is 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 the 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 certain -- 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 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 n = CRVal n
       ask   = Get0 CRVal       -- or, eta-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, 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 defines 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 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 a 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 the earlier 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 n = Val n
       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 have specifically defined 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 to the context for an implicit value, 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 now 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 out 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, monads -- often talked about in connection with effects -- do not help since they do not compose (which was made clear at the very beginning). We shall see how extensible-effects make the composition possible. Concretely, we will learn to combine the previously defined Get and Put effects and handle them separately -- and together, thus realizing mutable State.

Earlier we wrote the program rlExp3 with the Get effect to ask the context for a (dynamically bound there) integer and compute with it. Later on we wrote the tell function that takes a string and tells it to the context, e.g., to log it. Let's try using both rlExp3 and tell in the same program, to log the beginning and the end of rlExp3:

     rwExp' = do
       tell "begin"
       x <- rlExp3
       tell "end"
       return x
It does not work, does it? The type checker flags the line x <- rlExp3 with the error:
     Couldn't match type `Get b' with `Put [Char]'
       Expected type: Comp (Put [Char]) b
         Actual type: Comp (Get b) b
The error message explains the problem well. The type Comp req a represents computations with one effect req, and here we have two, Get and Put.

The following variation

     rxExp' x = if x then rlExp3 else (do {tell "1"; return (0::Int)})
has exactly the same error, but makes the problem easier to understand. Here we also mean to do two effects: if x is true, the Get request is sent to the context; otherwise, a Put request. In process calculi, such an IO behavior that depends on the process' own decision is called `internal choice'. If process p1 sends a message m1 and process p2 sends m2, a process that somehow decides to continue either as p1 or as p2 may send either m1 or m2. That is exactly what we have been looking for: a program that may do effect r1 or effect r2 has the effect that is a `union', or sum of r1 and r2. Thus we can, after all, represent rxExp' and rwExp' as Comp req Int computations, where req is Sum (Get Int) (Put String). Here, Sum is defined as
     data Sum r1 r2 x where
       L :: r1 x -> Sum r1 r2 x
       R :: r2 x -> Sum r1 r2 x

It is like Either but applied to * -> * constructors. (Incidentally, the EDLS paper also said that an effect message carries a union of possible actions.) For convenience we introduce the following helpers, which re-brand an effectful computation as having a union effect:

     injL :: Comp r1 x -> Comp (Sum r1 r2) x
     injL (Val x)  = Val x
     injL (E r k)  = E (L r) (injL . k)
     
     injR :: Comp r2 x -> Comp (Sum r1 r2) x
     injR (Val x)  = Val x
     injR (E r k)  = E (R r) (injR . k)

We now can combine rlExp3 and tell in the same program, with the shown types.

     rxExp :: Bool -> Comp (Sum (Get Int) (Put [Char])) Int
     rxExp x = if x then injL rlExp3 else (injR (do {tell "1"; return (0::Int)}))
     
     rwExp :: Comp (Sum (Get Int) (Put [Char])) Int
     rwExp = do
       injR $ tell "begin"
       x <- injL $ rlExp3
       injR $ tell "end"
       return x

The notation is too heavy though. Before we get to improving it, let us see how to handle these `union' effects. With the ordinary union Either t1 t2, its value is either the value of the type t1 or the value of the type t2 (appropriately tagged) -- but not both. The same holds for the Sum r1 r2 effect. With this in mind, we re-write the runReader handler from an earlier section as:

     runReaderL :: e -> Comp (Sum (Get e) r2) a -> Comp r2 a
     runReaderL e (Val x)   = return x
     runReaderL e (E (L Get) k) = runReaderL e $ k e
     runReaderL e (E (R r) k)   = E r (\x -> runReaderL e (k x))

If a computation has an effect and that effect is really a Get request, runReaderL replies to it. The other requests are let propagate (like they did in bind). Every handler will now have a line like the last line of runReaderL, to propagate the requests it does not handle. To see runReaderL in action:

     :type runReaderL 2 rwExp
     runReaderL 2 rwExp :: Comp (Put [Char]) Int
Recall, rwExp is an expression that has the union effect. After runReaderL, the Get part of the union is handled: no longer appears in runReaderL 2 rwExp's type. The Put effect still remains -- and can be handled by runWriter from the previous section. Applying it as well lets us see the result of the mixed-effect expression rwExp:
     _ = (runWriter . runReaderL 2) $ rwExp
     -- (["begin","end"],9)
Applying one handler after another is composing them, literally. We have thus seen how to combine expressions of different effects in the same program, and how to compose handlers to deal with such mixed-effect expressions.

There is one problem, however: explicitly using injR and injL when combining effectful expressions is impractical. We have to find a less cumbersome way of building effect unions. Any suggestions?

Let us imagine the most convenient interface that is still implementable in Haskell without too much voodoo.

     type Union (r :: [* -> *]) a
     class Member (t :: k) (r :: [k])
     
     inj    :: Member t r => t v -> Union r v
     prj    :: Member t r => Union r v -> Maybe (t v)
     
     decomp :: Union (t:r) v -> Either (Union r v) (t v)
The type Union is like Sum with several summands: the old Sum r1 r2 a is now written as Union '[t1,t2] a where '[t1,t2] is a type-level list. The type-level list notation makes type sequences easier to write and read. The predicate Member req reqs (a type-class constraint) asserts that a request type req must appear somewhere in the sequence reqs (the exact location is irrelevant). The injection and projection functions inj and prj are written in terms of Member and hence treat the set of possible effects of an expression as truly a set. The function inj tells that a possible effect t is the one being actually performed. The dual prj checks if t, being one of the possible effects according to r, is the request that is actually being sent. For the sake of handlers, whose result type should say that the handled effect type no longer appears among the possible effects, we introduce decomp: an orthogonal decomposition of the union. Either the request that possibly may be t is indeed t -- or it is not. In the latter case, it is clearly no longer a member of the union r. Alas, unlike inj and prj, decomp does treat union components as an ordered type sequence rather than an unordered set. Had something like local instances with the closure semantics were available, we would not have to impose the unneeded order on effect types.

The general open union interface generalizes the earlier injL and injL to the uniform

     injC :: Member req r => Comp req x -> Comp (Union r) x
     injC (Val x)  = Val x
     injC (E r k)  = E (inj r) (injC . k)
saving us trouble figuring out how and in which order a given effect req should appear as part of a wider union. We re-write rwExp simply as
     rwExpC = do
       injC $ tell "begin"
       x <- injC $ rlExp3
       injC $ tell "end"
       return (x::Int)
The inferred type
     :type rwExpC
     rwExpC :: (OpenUnion52.FindElem (Get Int) r,
                OpenUnion52.FindElem (Put [Char]) r) =>
          Comp (Union r) Int
says that rwExpC is an expression that may have a Get Int effect and a Put String effect. Combining effectful expressions has become mechanical: just add injC. We may as well add injC right to the primitive effect expressions ask and tell, so to make them composable without further ado. The real-life extensible-effect library does exactly that.

As we have intimated, handlers use decomp to check if the handled computation asks for something that the handler could deal with:

     runReaderC :: e -> Comp (Union (Get e ': r)) a -> Comp (Union r) a
     runReaderC e (Val x)   = return x
     runReaderC e (E u k)   = case decomp u of
       Right Get -> runReaderC e $ k e
       Left  u   -> E u (\x -> runReaderC e (k x))
For our runReaderC, if the request is really Get, it is answered; otherwise, it is propagated up. The result of runReaderC is an effectful expression that certainly does not include the Get effect any more: it has been handled. Applying runReaderC to the running example rwExpC indeed shows that Get is dealt with and Put still left to handle:
     wExpC = runReaderC (2::Int) rwExpC
     -- wExpC :: OpenUnion52.FindElem (Put [Char]) r => Comp (Union r) Int

The Put handler is similar, relying on decomp and with the clause to propagate all other effects, if any:

     runWriterC :: Comp (Union (Put o ': r)) a -> Comp (Union r) ([o],a)
     runWriterC (Val x)   = return ([],x)
     runWriterC (E u k)   = case decomp u of
       Right (Put x) -> do
         (l,v) <- runWriterC (k ())
         return (x:l,v)
       Left  u       -> E u (\x -> runWriterC (k x))
It lets us handle wExpC's remaining effect:
     expC = runWriterC wExpC :: Comp _ ([String],Int)
     -- expC :: Comp (Union r) ([String], Int)
QUIZ: Why do we need the signature? What to do with expC now?

There is still a task of extracting the result of expC. Its inferred type shows no further constraints on the union of possible effects r -- meaning that the type variable r may be instantiated to any type-list type, including the empty list '[]. If we do that, Comp (Union '[]) a may have only the Val alternative, with the computation result:

     run :: Comp (Union '[]) a -> a
     run (Val x) = x
     -- there are no more choices: effects are not possible
Hence applying run at the end gives us the result:
     _ = run expC
     -- (["begin","end"],9)

We have just seen how to handle the Get effect and then the Put effect, separately. They can be dealt with together, in the same handler:

     runState :: e -> Comp (Union (Get e ': Put e ': r)) a -> Comp (Union r) a
     runState e (Val x)   = return x
     runState e (E u k)   = case decomp u of
       Right Get -> runState e $ k e
       Left  u   -> case decomp u of
         Right (Put e) -> runState e $ k ()
         Left u        -> E u (\x -> runState e (k x))
The handler's type is quite telling: mentioning both Get e and Put e. Put e is treated as an update to the value the next Get will get. In other words, we have realized the mutable state. Here is the example:
     ts21 = do 
       injC $ tell (10::Int)
       x <- injC ask
       injC $ tell (20::Int)
       y <- injC ask
       return ((x+y)::Int)
to be run as
     _ = (run . runState (0::Int)) ts21
     -- 30
The result matches the mutable state intuition: ask now retrieves the current value of the state and tell updates it.

We have learned how to use expressions of different effects in the same program. The resulting code has a union effect, enumerating which effects are possible during the program run (the left out effects are hence positively not going to happen). A handler has to be prepared to receive a request it does not recognize -- which it should propagate up. The handled effect is no longer possible, in type and in effect. A handler can deal with one effect, or several at once. Composing individual effect handlers lets us eventually deal with all effects a program may have. The final run will make sure all the effects are handled.

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 less-toy demo of an `industrial-strength' extensible-effects library -- non-determinism with committed choice (aka LogicT) -- is described in Section 5 of the `more effects' paper.
References
more.pdf [291K]
doi:10.1145/2804302.2804319
Freer Monads, More Extensible Effects
The paper published in the Proceedings of the 2015 ACM SIGPLAN symposium on Haskell, pp. 94-105. Vancouver, BC, Canada. September 3-4, 2015.

Tutorial3.hs [10K]
Another example of non-determinism

 

IO errors and the current state

Catching of dynamic and asynchronous exceptions in the presence of other effects -- the solution of the MonadCatchIO problem. It is described in Section 6 of the `more effects' paper.
References
more.pdf [291K]
doi:10.1145/2804302.2804319
Freer Monads, More Extensible Effects
The paper published in the Proceedings of the 2015 ACM SIGPLAN symposium on Haskell, pp. 94-105. Vancouver, BC, Canada. September 3-4, 2015.

EffDynCatch.hs [5K]
The accompanying code

 

Monadic Regions

Monadic regions through extensible effects. The test code is essentially the same as that of the original Monadic Regions implementation. This is the content of Section 7 of the `more effects' paper.
Version
The current version is May 2015.
References

EffRegion.hs [11K]
EffRegionTest.hs [10K]
The accompanying code



Last updated December 11, 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