lexi-lambda · November 13, 2020 02:25 · Nov 13, 2020
diff --git a/scoped-effects-notes-2020-11-12.md b/scoped-effects-notes-2020-11-12.md
@@ -0,0 +1,106 @@
+# 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:
+
+```haskell
+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.:
+
+```haskell
+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:
+
+```haskell
+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:
+
+```haskell
+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)`:
+
+     ```haskell
+     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)`:
+
+     ```haskell
+     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`:
+
+```haskell
+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:
+
+```haskell
+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:
+
+```haskell
+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.
No results found