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.
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.
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.
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
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 >
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.
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.
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.
Tutorial3.hs [10K]
Another example of non-determinism
EffDynCatch.hs [5K]
The accompanying code
EffRegion.hs [11K]
EffRegionTest.hs [10K]
The accompanying code
oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML