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 -- A`Reader`

effect definition with one operation`ask`

of type`()`

to`a`

. 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 ans`handlerLocal`

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`

a`h`

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`

a`h`

only and not visible in the `action`

as
apparent from its effect context (which does *not* contain

). The
`Local`

a`ret`

argument can be used to transform the final result combined with the final state.