Extensible Effects

Monad transformers is a framework to let the programmer assemble monads through a number of transformers, producing a combined effect consisting of layers of monadic effects. The layering is determined statically and cannot easily be altered dynamically in different parts of the program. This framework is fundamentally limited.

Their alternative to a monad transformer stack is a single monad Eff, for the coroutine-like communication of a client with its handler. The ambition is for Eff to be the only monad in Haskell. Rather than defining new monads, programmers will be defining new effects, that is, effect interpreters.

• We denote (algebraic) handlers as authorities that control some resources and interpret some requests.
• We develop an expressive type-and-effect system that keeps track of which effects are currently active in a computation. This system maintains an open union (type-indexed coproduct of functors) containing an unordered collection of current effects.
• The action of each handler is reflected in the type by removing the effects that have been handled.

2. A Tour of Extensible Effects Framework

The two main points of interest are that:

1. All effectful computations are represented by a monad Eff r
2. The type parameter r is an open union of individual effects whose components must be Typeable (the class Typeable allows a concrete representation of a type to be calculated). Effects are represented by requests, hence the name r.

There are two basic ways of indicating that an effect m is part of this open union r.

1. Via a type constraint Member m r which indicates that the effect m is an element of the set r.
2. Via an explicit pattern m ▷ r' that decomposes the union r into the effect m and the remaining effects r'.

The extensible effects library is implemented to look similar to MTL.

-- The effect monad, which can express a monad transformer stack
instance Monad (Eff r) 

We can think of Void as the empty set of effects, i.e. a computation of type Eff Void a is pure.

data Void 
run :: Eff Void w -> w -- Pure computations

Here are some more common monads expressed as effects.

type Reader e
ask       :: (Typeable e, Member (Reader e) r) => Eff r e
runreader :: Typeable e => Eff (Reader e ▷ r) w -> e  -> Eff r w

As an example, the following computation’s type indicates that it returns an Int after potentially manipulating an environment containing an Int. The fact that r includes at least the Reader Int effect is expressed by the constraint (Member (Reader Int) r). The operation ask inquires about the current value in the environment, and t1 returns the incremented value.

t1 :: Member (Reader Int) r => Eff r Int
t1 = do v <- ask
        return (v + 1 :: Int)

We can execute the computation t1 by providing it with an initial value for the environment:

runReader t1 (10 :: Int) :: Eff r Int

The inferred type for this expression is (Eff r Int) without further constraints, because the Reader Int effect has been handled and hence subtracted from the open union. In this particular case, there are no remaining effects, and the pure computation can be run to produce a plain Int.

t1r = (run $ runReader t1 (10 :: Int))  :: Int

At the expression level, the code for running the effectful computation is identical to that of an MTL-based implementation. At the type level, the constraint (Member (Reader Int) r) looks similar to the MonadReader constraint. However Eff r is more general: r may contain an arbitrary number of Reader effects, and does not force us to choose the order of the effects, and hence does not force us to use lift.

t2 :: (Member (Reader Int) r, Member (Reader Float) r) => Eff r Float
t2 = do
  v1 ← ask
  v2 ← ask
  return $ fromIntegral (v1 + (1 :: Int)) + (v2 + (2 :: Float))

Each occurrence of ask obtains the value from its own environment, which it finds by type (here, Int vs Float).

3. The Implementation of the Extensible Effects Framework

3.1 Reader Effect as an Interaction with a Coroutine

We implement the effect of obtaining a Int value from the environment. We view effects as arising from communication between a client and an effect handler. This client-handler communication adheres to a generic client-server communication model, and thus may be easily modeled as a coroutine. A computation sends a request and suspends, waiting for a reply; a handler waits for a request, handles what it can, and resumes the client. We use the continuation monad to implement such coroutines, where the result type .

-- The result type `r` is specialised to `VE w`
newtype Eff a = Eff { runEff :: ∀ w. (a -> VE w) -> VE w }

instance Monad Eff where
  return x = Eff $ \k -> k x
  m >>= f  = Eff $ \k -> runEff m (\v -> runEff (f v) k)

-- The result type `VE w` can either be a value or resumable continuation which reads from the environment
data VE w = Val w | E (Int -> VE w)

The type Eff a is the type of computations that perform control effects instantiated to the coroutine status types (VE w) for polymorphic final result type w, where VE is short for Value-Effect, indicating the two types that make up the signature.

The coroutine status type shows that a computation may:

1. Val - Produce a value (Val w).
2. E - Send a request to read the Int environment (E (Int -> VE w)). This request, when resumed, continues the computation, which then recursively produces another answer of type VE w.

ask :: Eff Int
ask = Eff (\k -> E k)

The function ask sends a request that retrieves the current environment as follows: it obtains the current continuation k :: Int -> VE w and incorporates it into the request E k, constructing a function k that will be invoked when resumed from E k.

admin :: Eff w -> VE w
admin (Eff m) = m Val

The function admin launches a coroutine with an initial continuation expecting a value, which must be the final result. Hence, the Val continuation will be applied to the final result after all requests have been handled.

runReader :: Eff w -> Int -> w
runReader m e = loop (admin m) where
  loop :: VE w -> w
  loop (Val x) = x
  loop (E k)   = loop (k e)

The handler runReader launches the coroutine and checks its status.

1. If the coroutine sends an answer Val x, then the result is returned.
2. If the coroutine sends a request asking for the current value of the environment, then that value e is given in reply.

3.2 Coroutines for an Arbitrary Effect

We now extend the framework to handle other effects.

Example: • We may model boolean exceptions: To do this, we send the exception value Bool as a request without specifying the continuation (since no resumption is expected). The answer type (Value-Effect) for exception-throwing coroutines can be expressed as:

data VEexception = Val w | E Bool

• We can also model non-deterministic effects, one which non-deterministically chooses an element from a given list. To do this, we send the request that includes the list [a] and the continuation a -> VEchoose w expecting one element in reply.

data VEchoose w = Val w | forall a. E [a] (a -> VEchoose w)

Implementing the Groundwork for Generalized Coroutines

By looking at the result type VE for the coroutines servicing Reader, choice, and Exception requests, we make the observation that:

The result type VE for an effect Eff always includes:

1. The Val w alternative for normal termination with a final value.
2. A form of E alternative for carrying requests. The request typically includes the continuation of form t -> VE effect w where:
   • The expected reply type t depends on the request.
   • The result type VE effect w is the status type of the coroutine.

If we abstract this approach the general type for the coroutine status is:

data VE w r = Val w | E (r (VE w r))

The type parameter r :: * -> * describes a particular request.

• For example, the Reader request would instantiate r with (Reader e):

newtype Reader e v = Reader (e -> v)

Hence using the Reader request would look like E (Reader (e -> VE w (Reader e)))

The effect r is therefore actually a type constructor of kind * -> *, constructing the type of the request E from the status type of the coroutine VE w r. This follows directly from the recursive nature of the request type. This type will allow us to compose arbitrary effects.

Using this rich type for coroutine statuses VE w r, we can easily generalize our monad coroutine to arbitrary requests:

newtype Eff r a = Eff { runEff : forall w. (a -> VE w r) -> VE w r }

The coroutine monad Eff is indexed by the type of requests r that the coroutine may send.

send :: (forall w. (a -> VE w r) -> r (VE w r)) -> Eff r a
send f = Eff $ \k -> E (f k)

The function send dispatches a request r and waits for a reply.

• It takes an f :: (a -> VE w r) -> r (VE w r) which is a user-specified request builder. This is typically a type constructor representing an effect, which takes a suspended continuation.
• It obtains the suspension/continuation k :: a -> VE w r
• It applies f to k, to obtain the request body f k :: r (VE w r)
• It incorporates the request body f k into the request E.

admin :: Eff r w -> VE w r
admin (Eff m) = m Val

The function admin takes a coroutine and launches it with the initial continuation being Val which expects a final return value.

Examples

This described coroutine library (along with open unions) provides the entire groundwork for our effect system. We demonstrate two such effects below:

• The type Void is the type of no requests, similar to the Identity monad: it describes pure computations that contain no effects and send no requests.

data Void v -- no constructors

run :: Eff Void w -> w
run m = case admin m of Val

The function run serves as the handler for pure computations. • The effect of reading from an environment is reimplemented with the generalized coroutine library as follows:

newtype Reader e v = Reader (e -> v)

ask :: Eff (Reader e) e
ask = send Reader

runReader :: forall e w. Eff (Reader e) w -> e -> Eff Void w
runReader m e = loop (admin m) where
  loop :: VE w (Reader e)