eveff-1.0.0.0: Efficient effect handlers based on evidence translation.
Copyright(c) 2020 Microsoft Research; Daan Leijen; Ningning Xie
LicenseMIT
Maintainerxnning@hku.hk; daan@microsoft.com
StabilityExperimental
Safe HaskellNone
LanguageHaskell2010

Control.Ev.Eff

Description

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 :: Eff (Reader String :* ()) Int
          return (length s)

Enjoy,

Daan Leijen and Ningning Xie, May 2020.

Synopsis

Effect monad

data Eff e a Source #

The effect monad in an effect context e with result a

Instances

Instances details
Monad (Eff e) Source # 
Instance details

Defined in Control.Ev.Eff

Methods

(>>=) :: Eff e a -> (a -> Eff e b) -> Eff e b #

(>>) :: Eff e a -> Eff e b -> Eff e b #

return :: a -> Eff e a #

Functor (Eff e) Source # 
Instance details

Defined in Control.Ev.Eff

Methods

fmap :: (a -> b) -> Eff e a -> Eff e b #

(<$) :: a -> Eff e b -> Eff e a #

Applicative (Eff e) Source # 
Instance details

Defined in Control.Ev.Eff

Methods

pure :: a -> Eff e a #

(<*>) :: Eff e (a -> b) -> Eff e a -> Eff e b #

liftA2 :: (a -> b -> c) -> Eff e a -> Eff e b -> Eff e c #

(*>) :: Eff e a -> Eff e b -> Eff e b #

(<*) :: Eff e a -> Eff e b -> Eff e a #

Choose :? e => Alternative (Eff e) Source # 
Instance details

Defined in Control.Ev.Util

Methods

empty :: Eff e a #

(<|>) :: Eff e a -> Eff e a -> Eff e a #

some :: Eff e a -> Eff e [a] #

many :: Eff e a -> Eff e [a] #

Choose :? e => MonadPlus (Eff e) Source # 
Instance details

Defined in Control.Ev.Util

Methods

mzero :: Eff e a #

mplus :: Eff e a -> Eff e a -> Eff e a #

runEff :: Eff () a -> a Source #

Run an effect monad in an empty context (as all effects need to be handled)

Effect context

type (:?) h e = In h e Source #

An effect membership constraint: h :? e ensures that the effect handler h is in the effect context e. For example:

inc :: (State Int :? e) => Eff e ()
inc = do i <- perform get ()
         perform put (i+1) }

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 (handler hnd action) that the 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

handler :: h e ans -> Eff (h :* e) ans -> Eff e ans Source #

Use handler hnd action to handle effect h with handler hnd in action (which has h in its effect context now as h :* e). For example:

data Reader a e ans = Reader { ask :: Op () a e ans }

reader :: a -> Eff (Reader a :* e) ans -> Eff e ans
reader x = handler (Reader{ ask = value x })

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

data Op a b e ans Source #

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 -> Eff e ans that can be called to resume from the original call site. For example:

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

data Local a e ans Source #

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 Local a. This is fully local to the handler 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 Local a. This is fully local to the handler h only and not visible in the action as apparent from its effect context (which does not contain Local a). The ret argument can be used to transform the final result combined with the final state.

lget :: Local a e ans -> Op () a e ans Source #

Get the value of the local state.

lput :: Local a e ans -> Op a () e ans Source #

Set the value of the local state.

lmodify :: Local a e ans -> Op (a -> a) () e ans Source #

Update the value of the local state.

localGet :: Eff (Local a :* e) a Source #

Get the value of the local state if it is the top handler.

localPut :: a -> Eff (Local a :* e) () Source #

Set the value of the local state if it is the top handler.

localModify :: (a -> a) -> Eff (Local a :* e) () Source #

Update the value of the local state if it is the top handler.