scoped-effects-notes-2020-11-12.md

With scoped effects, handlers must be a part of the program

It is seductive to imagine that effect handlers in an algebraic effect system are not part of the program itself but metalanguage-level folds over the program tree. And in traditional free-like formulations, this is in fact the case. The Eff monad represents the program tree, which has only two cases:

data Eff effs a where
  Pure :: a -> Eff effs a
  Op :: Op effs a -> (a -> Eff effs b) -> Eff effs b

data Op effs a where
  OHere  :: eff a -> Op (eff ': effs) a
  OThere :: Op effs a -> Op (eff ': effs) a

Program trees of this type are only syntax, not semantics. Effect handlers assign semantics to the syntax, and they are expressed as ordinary Haskell functions that recursively fold over the tree, e.g.:

runReader :: r -> Eff (Reader r ': effs) a -> Eff effs a
runReader _ (Pure x)           = Pure x
runReader r (Op (OHere Ask) k) = runReader r (k r)
runReader r (Op (OThere x) k)  = Op x (runReader r . k)

In practice, libraries provide combinators that abstract away the recursive structure of such handler functions, but handlers could in principle always be written in the directly recursive style.

However, when we introduce scoping operators, things get more complicated. We start by extending the grammar of computations to include scopes:

data Eff effs a where
  Pure :: a -> Eff effs a
  Op :: Op effs a -> (a -> Eff effs b) -> Eff effs b
  Scoped :: Scoped effs (Eff effs) a -> (a -> Eff effs b) -> Eff effs b

data family Scope eff :: (Type -> Type) -> Type -> Type -> Type

data Scoped effs m a where
  SHere  :: Scope eff m r a -> m r -> Scoped (eff ': effs) m a
  SThere :: Scoped effs m a -> Scoped (eff ': effs) m a

Note the difference between the kind of effect types and their corresponding scopes:

type EffectK = Type -> Type
type ScopeK  = (Type -> Type) -> Type -> Type -> Type

The extra type parameters are needed because scopes are more complicated than algebraic operations in two ways:

1. Scopes contain computations, not just values. In Scope eff m a b, the m type parameter is the functor that provides the program structure of the enclosing computation. For example, this is used for in the definition of Scope (Error e):

   data instance Scope (Error e) m a b where
     Catch :: (e -> m a) -> Scope (Error e) m a a

   Here, the field of type e -> m a is the exception handler, which must be able to perform precisely the same set of effects as the enclosing computation can.

2. Scopes wrap subcomputations, and the result type of the scoped computation may differ from the result of its subcomputation. For example, the listen operator extends the result with an additional value. The relationship between the “inner” and “outer” result types is encoded in the final two type parameters, as in Scope (Writer w):

   data instance Scope (Writer w) m a b where
     Listen :: Scope (Writer w) m a (w, a)

The second of the above two points is a minor complication, but it does not present any real difficulty. However, the first quickly becomes a nuisance when writing handler functions. Consider the revised definition of runReader:

runReader :: r -> Eff (Reader r ': effs) a -> Eff effs a
runReader _ (Pure x)           = Pure x
runReader r (Op (OHere Ask) k) = runReader r (k r)
runReader r (Op (OThere x) k)  = Op x (runReader r . k)
runReader r (Scoped (SHere (Local f) m) k)
  = runReader (f r) m >>= runReader r . k
runReader r (Scoped (SThere x) k)
  = Scoped (weave (runReader r) x) (runReader r . k)

The interesting case is the last one, which recurs inside a scoping operator from a different effect. Because scoping operators themselves contain subcomputations, the runReader r handler must be pushed into those subcomputations as well as the unscoped continuation. But how do we know how to recur into the subcomputations in an arbitrary Scope eff value? The structure of such types is specific to each effect.

The usual solution is to require each definition of Scope eff to provide a mapping operator that applies a natural transformation to each subcomputation:

class Effect eff where
  mapS :: (forall r. f r -> g r) -> Scope eff f a b -> Scope eff g a b

mapS is then used in the implementation of weave, which applies a natural transformation to an arbitrary Scoped effs m a value:

weave :: (forall b. f b -> g b) -> Scoped effs f a -> Scoped effs g a

weave, or something like it, appears in several existing Haskell effect libraries, including polysemy and fused-effects. In the mtl ecosystem, it is directly analogous to the operations provided by MonadBaseControl. All implementations based on weave-like constructs suffer two problems:

1. Powerful continuation-manipulation effects such as Coroutine are impossible to express.

2. Scoping operators affect the semantics of other effects in unintuitive ways. For example, State operations become mysteriously “transactional” inside catch scopes, in that state updates made inside the catch are discarded if an exception is thrown. Other effects behave in even less intuitive ways, but that has been discussed elsewhere.

Both of these problems actually stem from the same issue, namely that weave requires handler state be threaded through subcontinuations in such a way that state becomes inextricably linked with control flow: discarding a continuation also discards state changes made up to that point. Furthermore, some effects, such as NonDet and Coroutine, manipulate control in a way that is non-local and can capture continuations that include the scoping operator itself, but the subcontinuations made available to handlers by weave only include the evaluation frames enveloped by the scope.

In other words, scoping operations fundamentally delimit the continuation because they do not commute with >>= (by definition). This makes it impossible for effect handlers that perform continuation manipulation to be fully independent of one another, since capturing a continuation that includes a scoping operator would require cooperation from the scope’s “owner”.

As a final attempt to salvage this approach, we might look for a general-purpose way to encode that sort of inter-handler cooperation. For example, we might imagine that a handler that wishes to capture the continuation could return a “continuation capture request” to the handler in control of the enclosing scope, which would then observe the request by rewrapping the inner continuation in the relevant scoping operator and composing it with the outer continuation before passing the request up the handler chain. But at this point we’ve reimplemented a virtual machine that cooperatively passes control between various handlers via continuation capture and abort, and we’ve completely lost the idea that handlers are simple folds over program syntax.

To elaborate, in order to free individual handlers from the burden of individually reimplementing the calling convention of the virtual machine, we could naturally introduce the notion of a central authority that mediates control flow between the various handlers. But now handlers are no longer independent folds: the central authority performs a single, grand, unified fold over the entire program, imposing a rigid evaluation order and dispatching briefly to handlers only as appropriate. Intermediate program states are inextricably entangled with the state of the handlers currently “in scope,” and continuations are no longer meaningfully described by our simple, handler-independent Eff syntax tree we started from.