Interposing is ignorant of other effect handlers

[robrix]

This came up most recently in the context of #46, but we’ve seen it in a few different contexts overall. I’m aware of three useful lenses on the problem, so I’ll try to detail each of them.

1. interpose applies only to the effects inside it, not whatever effects they’re handled with.

   If you use resumable exceptions, Yield, or some effect-as-abstraction which hides the implementation details behind its requests & handlers, you have to be aware of the interactions with e.g. Exc and Reader. catchError and local both use interpose to intercept requests, but only within the action passed to them at the time at which they were called.

   Thus, local (+ (1 :: Int)) (send Foo) will increment the context value for any asks or further local inside the action it receives, send Foo, and not whatever action handles send Foo. Since there are no Reader actions within send Foo itself (only Foo, whatever that is), it’s as if we hadn’t bothered using local at all.

2. Effects inserted by handlers (relay, etc) are run in the context at which the handler is called, not in the context of the effects they’re handling; or, handlers can inject values, but not effects, into effectful actions.

   This is easiest to demonstrate by zooming out a bit from the local handler described above to encompass the Foo and Reader handlers as well:

   data Foo result where
     Foo :: Foo Int
   
   testFoo :: Eff '[] Int
   testFoo = runReader (0 :: Int) (relay pure (\ Foo yield -> ask >>= yield) (local (+ (1 :: Int)) (send Foo)))

   The relay handling Foo is free to send Reader requests, since Reader is handled above it. However, these requests are made in the context relay is called at, which only has the top-level runReader handler present, and not where the Foo effect is sent. Thus, the result of testFoo will be 0, despite the local increment—sending the Foo effect escapes from the local context and there’s no way to un-escape.

   This is the case even tho we’re calling yield to provide the Int back to the sending context—so we can inject values back in, but not effects. That takes us to the third angle on this.

3. Higher-order effects are inflexible.

   The one exception I’m aware of to the rule that handlers can inject values but not effects is if we have what I’m terming a higher-order effect, i.e. an effect whose result is an effectful action. We can define Foo thus by changing its result type:

   data Foo result where
     Foo :: Foo (Eff '[Foo, Reader Int] Int)

   Rather than encoding a request for an Int, Foo is now a request for an Eff producing an Int. Since we’ve changed the result type of Foo, we must also change its handler and requests:

   testFoo :: Eff '[] Int
   testFoo = runReader (0 :: Int) (relay pure (\ Foo yield -> yield ask) (local (+ (1 :: Int)) (join (send Foo))))

   Note that we’re yielding the ask action (rather than its result), and joining the result of the send. Now, the result of run testFoo is (correctly) 1, which is exactly the behaviour we want. Furthermore, it’s clear that the change to the semantics of the request are the only sensible way of injecting effects into an action; the effect has to specify that they’ll occur, the code making the request has to request and join them, and the handler has to satisfy that request with an effectful action.

   Unfortunately, this comes at a significant cost to flexibility. Foo’s result type enumerates all of the effects it’s able to perform. This same problem exists with Embedded, which makes it easier to encode a smaller list of effects, but in no way addresses the need to enumerate them. (Furthermore, as Embedded requests hold an Eff and return an a, they’re only able to express the passing of an action to a handler, rather than the handling of an effect by passing an action back.)

   This can pose a serious barrier to implementation, since we have to be careful not to mention the effects list itself, i.e. the naïve Member (Reader (Eff effects Int)) effects constraint we would wish to be able to employ is unsolvable due its request for the occurrence of effects within effects—and so we can’t actually handle the effect.

   The reason becomes obvious when you try to give a type for the handler: we start with Eff (Reader _ ': effects) a -> Eff effects a, and then try to fill in the hole. But since it’s self-referential, we have to fill it in with Eff (Reader _ ': effects) Int, and then again, ad infinitum. Attempts to resolve this with a type equality constraint on effects also fail, and while it’s not explicitly mentioned, I believe it’s due to the occurs check.

   When needing to break a cycle like this, the obvious solution is to employ a newtype, which we can indeed use successfully here. However, this is really just moving the problem around. While something like this:

   newtype Inner = Inner { runInner :: Eff (Reader (Inner effects Int) ': effects) a }

   does enable us to write the handler, now the actions making requests have to be aware that a) they need to use & unwrap Inner, and b) that it’s at the head of the effect list (a constraint imposed by Inner itself). While the former problem is quite minor, the latter means that they instantly become very inflexible, and can’t easily be run in different contexts.

These three problems—really the same problem—are the cause of significant complexity in our use cases. I think we might be able to make some headway by having Eff provide effects with the effect list as a parameter, but I’m not at all certain of that.

It’s also entirely possible that this is just a reality of using this system. In that case, we should at least document some best practices for handling these sorts of situations.

[robrix]

Upon reflection, I don’t think it’ll work for effects to take the effect list as a parameter, since that just moves the problem around again—that would mean that handling an effect would have to change the type of every effect in the list.

[robrix]

Upon reflection, I don’t think it’ll work for effects to take the effect list as a parameter, since that just moves the problem around again—that would mean that handling an effect would have to change the type of every effect in the list.

Upon further reflection, that’s exactly what we want—and we have the handler to do it, when we handle the effect, by definition.

[robrix]

Looks like Syntax and Semantics for Operations with Scopes by Maciej Piróg, Tom Schrijvers, Nicolas Wu, and Mauro Jaskelioff is exactly what we’re looking for here.