Copyright | (c) 2020 Microsoft Research; Daan Leijen; Ningning Xie |
---|---|
License | MIT |
Maintainer | xnning@hku.hk; daan@microsoft.com |
Stability | Experimental |
Safe Haskell | None |
Language | Haskell2010 |
Efficient effect handlers based on Evidence translation. The implementation is based on "Effect Handlers, Evidently", Ningning Xie et al., ICFP 2020 (pdf), and the interface and design is described in detail in "Effect Handlers in Haskell, Evidently", Ningning Xie and Daan Leijen, Haskell 2020 (pdf).
An example of defining and using a Reader
effect:
{-# LANGUAGE TypeOperators, FlexibleContexts, Rank2Types #-} import Control.Ev.Eff -- AReader
effect definition with one operationask
of type()
toa
. data Reader a e ans = Reader{ ask ::Op
() a e ans } greet :: (Reader String:?
e) =>Eff
e String greet = do s <-perform
ask () return ("hello " ++ s) test :: String test =runEff
$handler
(Reader{ ask =value
"world" }) $ --:: Reader String () Int
do s <- greet -- executes in context::
return (length s)Eff
(Reader String:*
()) Int
Enjoy,
Daan Leijen and Ningning Xie, May 2020.
Synopsis
- data Eff e a
- runEff :: Eff () a -> a
- type (:?) h e = In h e
- data (h :: * -> * -> *) :* e
- perform :: h :? e => (forall e' ans. h e' ans -> Op a b e' ans) -> a -> Eff e b
- handler :: h e ans -> Eff (h :* e) ans -> Eff e ans
- handlerRet :: (ans -> a) -> h e a -> Eff (h :* e) ans -> Eff e a
- handlerHide :: h (h' :* e) ans -> Eff (h :* e) ans -> Eff (h' :* e) ans
- mask :: Eff e ans -> Eff (h :* e) ans
- data Op a b e ans
- value :: a -> Op () a e ans
- function :: (a -> Eff e b) -> Op a b e ans
- except :: (a -> Eff e ans) -> Op a b e ans
- operation :: (a -> (b -> Eff e ans) -> Eff e ans) -> Op a b e ans
- data Local a e ans
- local :: a -> Eff (Local a :* e) ans -> Eff e ans
- localRet :: a -> (ans -> a -> b) -> Eff (Local a :* e) ans -> Eff e b
- handlerLocal :: a -> h (Local a :* e) ans -> Eff (h :* e) ans -> Eff e ans
- handlerLocalRet :: a -> (ans -> a -> b) -> h (Local a :* e) b -> Eff (h :* e) ans -> Eff e b
- lget :: Local a e ans -> Op () a e ans
- lput :: Local a e ans -> Op a () e ans
- lmodify :: Local a e ans -> Op (a -> a) () e ans
- localGet :: Eff (Local a :* e) a
- localPut :: a -> Eff (Local a :* e) ()
- localModify :: (a -> a) -> Eff (Local a :* e) ()
Effect monad
The effect monad in an effect context e
with result a
runEff :: Eff () a -> a Source #
Run an effect monad in an empty context (as all effects need to be handled)
Effect context
data (h :: * -> * -> *) :* e infixr 5 Source #
An effect context is a type-level list of effects.
A concrete effect context has the form (h1 :* h2 :* ... :* hn :* ())
.
An effect context can also be polymorpic, as (h :* e)
, denoting a top handler
h
with a tail e
. For example the type of handler
reflects that in
an expression (
that
the handler
hnd action)action
can perform operations in h
as that is now the top handler in the
effect context for action
:
handler
:: h e ans ->Eff
(h:*
e) ans ->Eff
e ans
(Note: The effects in a context are partially applied types -- an effect h e ans
denotes a full effect handler (as a value) defined in an effect context e
and
with answer type ans
. In the effect context type though, these types are abstract
and we use the partial type h
do denote the effect)
Perform and Handlers
perform :: h :? e => (forall e' ans. h e' ans -> Op a b e' ans) -> a -> Eff e b Source #
Given an operation selector, perform the operation. The type of the selector
function is a bit intimidating, but it just selects the right operation Op
from the
handler h
regardless of the effect context e'
and answer type ans
where the
handler is defined.
Usually the operation selector is a field in the data type for the effect handler. For example:
data Reader a e ans = Reader{ ask ::Op
() a e ans } greet :: (Reader String:?
e) =>Eff
e String greet = do s <-perform
ask ()return
("hello " ++ s) test =runEff
$handler
(Reader{ ask =value
"world" }) $ greet
handlerRet :: (ans -> a) -> h e a -> Eff (h :* e) ans -> Eff e a Source #
Handle an effect h
over action
and tranform the final result with
the return function ret
. For example:
data Except a e ans = Except { throwError :: forall b.Op
a b e ans } exceptMaybe ::Eff
(Except a:*
e) ans ->Eff
e (Maybe ans) exceptMaybe =handlerRet
Just (Except{ throwError = except (\_ -> return Nothing) })
handlerHide :: h (h' :* e) ans -> Eff (h :* e) ans -> Eff (h' :* e) ans Source #
Define a handler h
that hides the top handler h'
from its action
,
while keeping h'
is still visible in the operation definitions of h
.
This is used to implement locally isolated state for handlerLocal
using
the regular local
state. In particular, handlerLocal
is implemented as:
handlerLocal
:: a -> (h (Local
a:*
e) ans) ->Eff
(h:*
e) ans ->Eff
e anshandlerLocal
init h action =local
init (handlerHide
h action)
mask :: Eff e ans -> Eff (h :* e) ans Source #
Mask the top effect handler in the give action (i.e. if a operation is performed
on an h
effect inside e
the top handler is ignored).
Defining operations
The abstract type of operations of type a
to b
, for a handler
defined in an effect context e
and answer type ans
.
value :: a -> Op () a e ans Source #
Create an operation that always resumes with a constant value (of type a
).
(see also the perform
example).
function :: (a -> Eff e b) -> Op a b e ans Source #
Create an operation that takes an argument of type a
and always resumes with a result of type b
.
These are called tail-resumptive operations and are implemented more efficient than
general operations as they can execute in-place (instead of yielding to the handler).
Most operations are tail-resumptive. (See also the handlerLocal
example).
except :: (a -> Eff e ans) -> Op a b e ans Source #
Create an operation that never resumes (an exception).
(See handlerRet
for an example).
operation :: (a -> (b -> Eff e ans) -> Eff e ans) -> Op a b e ans Source #
Create an fully general operation from type a
to b
.
the function f
takes the argument, and a resumption function of type b ->
that can be called to resume from the original call site. For example:Eff
e ans
data Amb e ans = Amb { flip :: forall b.Op
() Bool e ans } xor :: (Amb:?
e) =>Eff
e Bool xor = do x <-perform
flip () y <-perform
flip () return ((x && not y) || (not x && y)) solutions ::Eff
(Amb:*
e) a ->Eff
e [a] solutions =handlerRet
(\x -> [x]) $ Amb{ flip =operation
(\() k -> do{ xs <- k True; ys <- k False; return (xs ++ ys)) }) }
Local state
The type of the built-in state effect.
(This state is generally more efficient than rolling your own and usually
used in combination with handlerLocal
to provide local isolated state)
local :: a -> Eff (Local a :* e) ans -> Eff e ans Source #
Create a local state handler with an initial state of type a
.
localRet :: a -> (ans -> a -> b) -> Eff (Local a :* e) ans -> Eff e b Source #
Create a local state handler with an initial state of type a
,
with a return function to combine the final result with the final state to a value of type b
.
handlerLocal :: a -> h (Local a :* e) ans -> Eff (h :* e) ans -> Eff e ans Source #
Create a new handler for h
which can access the locally isolated state
.
This is fully local to the handler Local
ah
only and not visible in the action
as
apparent from its effect context (which does not contain
).Local
a
data State a e ans = State { get ::Op
() a e ans, put ::Op
a () e ans } state :: a ->Eff
(State a:*
e) ans ->Eff
e ans state init =handlerLocal
init (State{ get =function
(\_ ->perform
lget
()), put =function
(\x ->perform
lput
x) }) test =runEff
$ state (41::Int) $ inc -- see:?
handlerLocalRet :: a -> (ans -> a -> b) -> h (Local a :* e) b -> Eff (h :* e) ans -> Eff e b Source #
Create a new handler for h
which can access the locally isolated state
.
This is fully local to the handler Local
ah
only and not visible in the action
as
apparent from its effect context (which does not contain
). The
Local
aret
argument can be used to transform the final result combined with the final state.