Incorrect semantics for higher-order effects

[KingoftheHomeless]

First-order effect systems like freer-simple can make use of interpreters/effect interception to have pseudo higher-order actions, like handleError and catchError.
Unfortunately, such actions have semantic issues, since they rely on inspecting what effects are used of the target computation or rely on all uses of the relevant effect targeting a top-most effect of the effect stack -- either of which leads to incorrect results if intermediary effects get in the way.

Here's an example of freer-simple:

data SomeEff a where
  SomeAction :: SomeEff String

someAction = send SomeAction

-- returns (Left "not caught")
bad :: Either String String
bad = run $ runError @String $ interpret (\SomeAction -> throwError "not caught") $
  someAction `catchError` \(_ :: String) -> return "caught"
-- doesn't matter if "handleError" is used instead of "catchError"

Note that the exception doesn't get caught here even though both the use of throwError and catchError target the same Error effect. Compare this to polysemy, where the exception does, indeed, get caught.

I can't check this myself because I can't figure out custom compilers with cabal, but from what I've seen, eff uses the same approach as freer-simple for its higher-order effects -- the only difference between freer-simple's handleError and eff's catch is that the interpretation done on-site with handleError is done within the interpreter for catch. In this case, eff should have the same issue. Confirmed by @TheMatten.

[KingoftheHomeless]

local should have the same issue too:

bad :: String
bad = run $ runReader "unlocaled" @String $ interpret (\SomeAction -> ask) $
  local (\_ -> "localed") someAction

And listen and censor (plus the other issues censor has which you're aware of).

[KingoftheHomeless]

@TheMatten confirms:

import Control.Effect
import Control.Effect.Error

data SomeEff :: Effect where
  SomeAction :: SomeEff m String

someAction :: SomeEff :< r => Eff r String
someAction = send SomeAction

bad :: Either String String
bad = run $ runError @String $ interpret (\SomeAction -> throw @String "not caught") $
  someAction `catch` \(_ :: String) -> return "caught"

λ> bad
Left "not caught"

[lexi-lambda]

This issue touches upon a few different things. Let me try to address them each in turn.

---

First, you are correct that eff provides ways to “skip” handlers in the stack when sending an effect. However, I strongly believe that, in general, this is a feature, not a bug! Consider the sample FileSystem effect: the pure handler internally uses a State handler to do its bookkeeping, and it would be very bad if that handler accidentally intercepted State actions from clients of runFileSystemPure. This concept of “effect encapsulation” turns out to actually be extraordinarily important in practice.

Under the delimited control model of extensible effects, there is a very simple explanation for what’s happening here: during execution of the effect handler, control temporarily aborts to the location of the interpret call. During the dynamic extent of the handler’s execution, any more-local handlers are ignored, because they’re genuinely not in scope. When the handler returns, the local evaluation context is restored, and execution continues. (This corresponds to the semantics of the control operators given in “Handling Control” by Dorai Sitaram, published at PLDI 1993.)

In my experience, this is almost always the desired semantics. Consider a handler that installs an extra local Error handler so that it can short-circuit the computation on certain operations. It does not want those throws to be caught by more-nested Error handlers simply because they happened to be throwing the same type of value. So in general, this behavior is a very good thing.

---

Okay, so let’s agree “handler encapsulation” is important (I don’t think your issue actually disagrees with that). What if it turns out you still sometimes want to avoid that “implicit abort” performed by interpret? What if you want to execute SomeAction’s handler directly in the local evaluation context?

In that case, eff still has your back: you can use handle instead of interpret. handle is eff’s “advanced” effect handler API; interpret is a shorthand for handle . liftH. liftH is the “execute this in the original context of the handler” operation, but you can explicitly opt to use locally instead, if you want. locally, as the name implies, says “execute this operation right here, in the local context,” so all the more-local handlers in scope are preserved.

However, this on its own does not resolve your problem, because locally doesn’t promise that any of the handlers that were in scope at the point of the handle call will still be in scope in the more-local context. At first blush, that sounds absurd: of course they’re in scope, we’re in a more local context; by definition all the handlers higher up in the call stack are still present. And indeed, right now, they must be. But eff is very flexible, and subtly, they might not continue to be.

Here’s an example of how such a situation could arise. Suppose the programmer writes some code using a local Coroutine effect, then they call someAction. Now suppose someAction resumes execution using locally, and during the execution of the handler, it triggers a yield. Now control yields back to the point of the runCoroutine handler, which receives a suspended computation that can be resumed later.

Now, suppose the caller of runCoroutine stashes the suspended coroutine somewhere, then leaves the scope of the SomeAction handler altogether. Now suppose it installs a completely different SomeAction handler, then resumes the Coroutine. The handlers in scope might now be totally different! It’s possible that the same set of effects aren’t even in scope anymore, even though the coroutine is executing a bit of code that “came from” the old SomeAction handler. This is the kind of mind-bendy behavior you can get when you start using control-manipulation effects like Coroutine.

(I apologize that I’m not providing any code here, but putting together the examples and explaining what all the pieces mean would be incredibly time-consuming, and I just don’t have the time and energy for that right now. But hopefully you can get some idea of what I’m talking about.)

---

Okay, so all this leaves us in a bit of an awkward spot:

• If we use interpret (or handle + liftH), our handler executes outside the scope of the catch, so the more-local catch doesn’t take effect.

• If we use locally, we execute in the scope of the catch, but we aren’t allowed to call throw because we can’t guarantee that the handler for our throw will still be in scope by the time we get there.

This seems pretty fundamental, but let’s take a step back for a moment. Clearly, polysemy gets around this issue somehow, so what does it do differently? Can eff do the same thing?

Well, no: the answer is that polysemy just doesn’t support Coroutine. So this is unfortunately one of these awkward tradeoffs: we can pick one behavior or the other, but not both (at least, not if we want the overall system to be predictable). eff chooses to support more expressive types of control manipulation (such as Coroutine), while polysemy chooses a more restrictive system that makes the edge case I described above impossible.

Is there a way out? Well, in theory, it ought to be possible to implement your SomeAction handler, even in eff. We could provide another low-level Handler operator alongside liftH and locally, named something like sendLocally, which behaves just like locally . send. The difference is that sendLocally has access to all the effects currently in scope, which is possible because we can be certain that the only thing it does is immediately call a handler, so something else can’t possibly yield first. That is very restrictive, but it avoids the pathological case.

But it turns out that even if we did that, your example would still do the wrong thing—the catch handler would be skipped! Why? Because of handler encapsulation: now we’ve finally managed to expose the implementation detail that catch is a local handler, not a modification of the throw handler, so handler encapsulation will cause it to be skipped. That, arguably, would be an actual bug.

---

This has been a lot of information. Let me try to recap the key takeaways so far:

• Currently, eff doesn’t make it possible to write a handler that exposes the difference between a more-local handler and a local modification to an existing handler, so currently there is no bug, just perhaps a missing feature.

• The missing feature could be added, but it would have to be very restrictive, given the additional expressiveness eff provides over polysemy in other ways.

• If such a feature were added, it would make it possible to observe the difference between a more-local handler and a local modification to an existing handler, which would be an actual bug (or at least a misfeature).

So far, I have written completely objectively. None of the above is editorialized, it’s just a description of the status quo. Let me now change that by offering my subjective thoughts:

1. It is not immediately clear to me that this missing feature is particularly useful. I do not personally know of any real-world programs that would take advantage of it. But I also don’t know for certain that it wouldn’t be useful, so if someone can provide a good use case to motivate what the right semantics need to be, I think that would provide justification for doing the extra work.

2. If it were to come to that, the bug that would be exposed could be fixed. I have thought a little about what the right semantics probably ought to be and whether it permits an efficient implementation, and I think the answer is “yes, it does.” There may be a small additional indirection cost, but I think it should be feasible.

3. I am interested in pursuing the aforementioned alternate approach to higher-order effects even if sendLocally turns out to not be very useful, because the current implementation leaks through in two other ways:

   1. It shows up in the types, where operations like catch and local add redundant elements in the type-level list of effects.

   2. It can be observed if you do this “yield then restore a coroutine with a different handler in scope” dance, since the behavior of any suspended catch operations will be determined by the old Error handler, not the new one. This is arguably a bug.

   So either way, I’d like to give it a try. But it’s a real edge case, and I suspect essentially nobody will actually get bitten by that issue, so I’ve been prioritizing other things.

To me, the truly important detail is that it can be made to work better in the future, i.e. it isn’t a fundamental limitation of the current design. Fortunately, I’m confident that’s the case; there is a fairly natural way of thinking about these higher-order operations in terms of a sort of “interposition semantics” (which I think is even sort of supported by the recent “Syntax and Semantics for Operations with Scopes,” so I suspect it’s on the right track, though I don’t fully understand that paper, so I could be off the mark).

Anyway, this has become an extremely long comment. These issues are very, very subtle. But to summarize: I think what you describe is not observable in eff today (so is not a bug), I think something slightly different is observable (and is a bug that should be fixed), but it’s an extraordinary edge case, so I have not tried to fix it yet. Hopefully I managed to get at least some of those points across. 🙂

[KingoftheHomeless]

Thanks for the write-up, Alexis. In particular, thanks for explaining why coroutines complicate this matter as much as they do; it's something that I've encountered before during my own experimentation on my way to developing a new effect system, but I did
not properly understand it until now.

That said, I'm afraid I have my wall of text of my own; my opinion is still that eff's HO semantics present an issue -- even if they follow from the model in place, I believe these semantics are ultimately undesirable.

---

Regarding effect encapsulation: I'm not sure how this is related to the HO semantics on display in the OP. Effect encapsulation is achieved by effect introduction, which is exactly what the sample FileSystem interpreter does through lift in order to introduce the local State effect. polysemy also uses effect introduction for the same purpose (reinterpret and raiseUnder), while having semantics that allows for actions within interpreters to be interacted with in application code.

If a handler wants an extra local Error effect for the purposes of short-circuiting while not exposing it to the outside world, it can simply introduce that effect, and that way it's impossible for any code from the outside world to target that Error effect when using catch.
If you're talking about something like runFileSystemPure, where the intention is (presumably) to signal failure using a global Error effect later down the line (which application code may also have access to), without letting application code catch your throws, then you can actually do that too, even with polysemy's HO semantics.

The solution is to install a local Error effect, do your throws in that effect, and then use either throw pure at the end to throw whatever exception that has been generated:

runFileSystemPure :: Error String :< effs => Eff (FileSystem ': effs) a -> Eff effs a
runFileSystemPure =
      -- same as in README.md, but with the extra line below:
  >>> runError @String >>= either throw return

Since the error effect the throws are done in aren't translated into the global 'Error String' until the very end,
there's no way for application code to catch the throws done in the handler.
This is the only situation I see where you'd want "skip" semantics, and I can't imagine it being particularly common.

Given these points, I don't see what benefit eff's HO semantics have.

---

As an example as to why effs HO semantics can become problematic (the reason why you'd need sendLocally), consider something like runFileSystemPure, but where the intention actually is that application code should be able to catch the exception. The first go for a beginner (or someone expecting the semantics of polysemy and fused-effects) would be something like this:

data FileIOException
  = AlreadyInUse FilePath
  | DoesNotxist FilePath IOMode
  | NotPermitted FilePath IOMode

ioExcToFileIOExc :: IOException -> Maybe FileIOException
ioExtToFileIOExc = ...

runFileSystemIO :: (IOE :< effs, Error FileIOException :< effs)
                => Eff (FileSystem ': effs) a
                -> Eff effs a
runFileSystemIO = interpret \case
  ReadFile path  -> liftIO (tryJust ioExcToFileIOExc (IO.readFile path))
                >>= either throw return
  WriteFile path -> liftIO (tryJust ioExcToFileIOExc (IO.readFile path))
                >>= either throw return

But because of effs HO semantics, this doesn't work, without that being obvious to the user.
It's a pretty nefarious source of bugs; I can easily imagine an end user growing frustrated when they find out that their catches don't work, and they can't figure out why.

But even if the bug is identified, how would you fix it? You need some way to throw the exception locally. There are two ways to go about it: either you modify the actions you implement for the effect so they transform the returned Either to an exception at use-site, or you use handle+locally to throw the exception in the handler directly.
I'll go with the former, since it's easier and locally is pretty broken at the moment, but these are essentially equivalent solutions, and they both have the same problems:

1. They require redefining the effect. (Returning a Either or
   demanding an Error effect to be in scope locally)
2. They require the Error FileIOException :< effs constraint in application
   code to use actions of the effect.

Both of these hurt. 1. restricts how flexibly the effect may be interpreted, and 2. makes application code forced to have an effect in scope it may not care about (until later, when you perform the catch).

But you can actually fix 2... sort of, by using the following construction:

data Exceptional eff exc :: Effect where
  Exceptionally :: eff q a -> Exceptional m (Either exc a)

exceptionally :: Exceptional eff exc :< effs
              => Eff (eff ': effs) a
              -> Eff effs (Either exc a)
exceptionally = handle (pure . Right) $ \e ->
  liftH (send (Exceptionally e)) >>= either (abort . Left) return

catching :: Exceptional eff exc :< effs
         => Eff (eff ': effs) a
         -> (exc -> Eff effs a)
         -> Eff effs a
catching m h = exceptionally >>= either h return

This is actually a construction I cooked up a way back for safe exception-handling, but here it can be repurposed to fix this issue.

Instead of interpreting FileSystem, runFileSystemIO will now interpret Exceptional FileSystem FileIOException, and application code will be able to use FileSystem in wild abandon without access to an Error effect, and use exceptionally at the points of the program where it wants to catch exceptions.

Note the following:

• Instead of catch in application code, you now use exceptionally or catching.
• You need an Exceptional for every effect that may throw exceptions that you want
  to catch in application code.
• Any eff in Exceptional eff must be first-order to make exceptionally implementable. This is due to limitations of handle.

And alright, that's all well and good. In fact, maybe requiring Exceptional is a good thing, because it guarantees that no exception slips by. But what if we go further; let's say we also want to do some logging in runFileSystemIO -- say, what file we opened -- and that logging should be listenable in application code. Then we have the same problem again.

Ok, let's fix it with the following:

data Telling eff w :: Effect where
  Telling :: eff q a -> Telling eff w m (w, a)

telling :: '[Telling eff w, Writer w] :<< effs
        => Eff (eff ': effs) a
        -> Eff effs a
telling = interpret $ \e -> do
  (s, a) <- send (Telling e)
  tell s
  return a

listening :: '[Telling eff w, Writer w] :<< effs
          => Eff (eff ': effs) a
          -> Eff effs (w, a)
listening = telling >>> listen

But unlike Exceptional, there's no convincing reason as to why Telling is a good thing; so what if a tell goes unlistened? Also, we now need to stack Telling and Exceptional, since runFileSystemIO needs both; Exceptional (Telling FileSystem). How pretty.

And of course, the same problem occurs with Reader which also needs its own Exceptional variant.
If you have multiple effects that you want to interact with in multiple ways, the sheer number of these kinds of interaction-enabling helper effects becomes ridiculous.

So while there are work-arounds, they significantly impact both interpretation of effects and application code, and may not always be possible to use (like if the effect isn't first-order).

In comparison, polysemy/fused-effects HO-semantics fixes all of that. To be honest, I consider it so important to the point I don't feel a proper HO effect library can be without it. With eff not having it, I'd class it as only slightly more powerful in comparison to freer-simple, since its HO actions behave the same as freer-simple's pseudo HO actions.
The big difference is locally, which allows you to choose what interpreter is used for the HO-action at interpretation time, and allows users to create HO-actions interpreted using FO-actions. This is admittedly a big upside, but as it now turns out that locally is unsafe in combination with coroutines, I'm not sure this feature can be kept (and still retain coroutines).

---

About sendLocally: I'm not as certain as you are that it's possible to extend eff with this feature, nor that HO-effects can be modified to be "handler-modification" oriented rather than "run local-handler" oriented. I admit, I'm not sure what you mean by handler modification. Are you referring to changing the context within the handler of an effect so the handler itself behaves differently -- something closer to polysemy and fused-effects -- or do you mean effect interception, like interpose and intercept?

If the former, that would be really cool, but I have no idea how you would go about it if you restrict yourself only to a free monad-like construction and delimited continuations without ending up with something similar to weave again.

If the latter, as noted in the OP, you get the same problems with effect interception as you would get relying on local handlers as eff currently does, so this doesn't really fix the issue.

The reason I'm skeptical towards sendLocally is that I feel that it may be possible to smuggle in a dangerous yield anyway, especially if sendLocally is allowed to send higher-order actions. It depends on how restricted it is.
This goes double now that locally has turned out to be unsafe for the reasons you've talked about: smuggling an action past its handler's scope!

Admittedly, I'm not very confident about these topics specifically (whether eff could support these things). This is a case of "I don't know how", and not "I couldn't possibly imagine it happening". I'll be happy to see my concerns be proven wrong.

---

Bleh. I didn't want to write an even larger post, trust me, but I felt I needed to describe in detail why I find polysemy/fused-effects's HO-semantics to be so important, and why the work-arounds you can (currently) build in eff don't really hold up.

To summarize my points:

• Effect encapsulation is only related to eff's HO-semantics in very niche cases, and in those cases polysemy can opt into the same semantics too.
• eff's HO-semantics require extensive boilerplate that has a high impact on both application and interpretation code if you want something similar to polysemy's HO-semantics. polysemy's HO-semantics require negligible additional work that only affects interpretation code if you want something similar to eff's HO-semantics.
• I'm uncertain how eff could be extended to include sendLocally or effects that rely on handler modification instead of local handlers, such that eff would allow you to opt into polysemy's HO-semantics.

[lexi-lambda]

I think one of the main reasons I’m struggling to communicate some of the finer points of this is that they depend on understanding (a) delimited continuations and (b) reduction semantics. When I first started writing this response to your comment, I said “okay, maybe I should just try to explain the essential ideas of both those things but stay handwavy enough to be quick,” but I’ve now written 200 lines of markdown and still haven’t gotten to the key payload. So I’m giving up on that for now; there’s just a little too much to cover in a GH comment.

But when you say

Regarding effect encapsulation: I'm not sure how this is related to the HO semantics on display in the OP.

this is a totally fair, understandable comment, but explaining precisely how it’s related involves talking about both of those things. Obviously I need to write up a better resource that explains all this stuff for people who care about the nitty-gritty, but while it’s something I can explain to most programmers in 5–10 minutes on a whiteboard, writing all of it up in a way that is understandable to everyone (without having a back-and-forth conversation) is a lot more involved. Alas.

Restatement of the problem

In any case, while I can’t discuss the how or the why as much as I’d like, I can still address the overall thrust of your comment. I see your point, and I think that it’s totally valid. The root of the issue is this:

1. Effect operations can fail, which is most naturally modeled using an Error effect.

2. Programmers expect the failure to be associated with the point where the operation is used, not where it’s handled. But eff treats handlers as if they run at the point of the handler, not the use of send.

There is clearly a mismatch here, and it is a great example that gets right to the heart of the problem of what “scoping operations” ought to mean.

In my previous comment, I explained why executing effect handlers in the context of the send call is playing with fire when coroutine-like effects are involved: the handlers in play can get swapped out from underneath us at any time. If we’re executing inside a handler, the computation suspends while inside the handler, and when computation resumes the handler (and other handlers above it) isn’t there anymore, we have essentially no way to proceed.

But eff’s current workaround of only evaluating handlers in a context where that can never happen can lead to this kind of baffling behavior you describe. Clearly something must be done.

An alternative model of scoping

The root of the tension in eff as implemented today is, as far as I understand it, in this and this alone:

1. “The coroutine problem” means handlers aren’t allowed to “see” more-nested handlers when responding to a send call.

2. Currently, eff implements operations like catch using nested handlers.

Point 1 is pretty immutable. So point 2 has to go—but what do we replace it with?

The key idea: scoping operations are a way to introduce interposition into the handling of an effect.

Currently, in eff, operations like catch are represented as simply other constructors in the effect datatype. They look a little different, but not enormously so:

data Error e :: Effect where
  Throw :: e -> Error e m a
  Catch :: Eff (Error e ': effs) a -> (e -> Eff effs a) -> Error e (Eff effs) a

The idea is that the Error handler should install a new, local handler for the first argument to Catch before continuing with evaluation. This is important because operations like Catch don’t do anything on their own; rather, they affect the meaning of containing occurrences of Throw.

The current approach eff takes is a hack, and it is unsatisfying on a fundamental level: it means further uses of Throw are no longer handled by the “real” Error handler, but a more-nested one. If the handler is swapped out halfway through, the new handler won’t get to interpret Catch its way, because the old handler has been captured in the suspended computation.

In a better world, catch wouldn’t actually do anything on its own. Rather, it would interpose on future throw calls, giving the current handler several chances to interpret the Throw, once per occurrence of Catch. In other words, if we have

handle @(Error e) h (... (catch (... (throw exn) ...) f) ...)

then we want the h handler to have two “chances” to handle the throw call, once at the point of the catch, and a second time at the point of the initial use of handle. This solves our “swapping out the handler later” problem, since whatever handler is in place at the time of the throw gets to handle the call, but it also allows us to resolve our “throw inside an effect handler” problem, because the interposition can be based on the location of the send, not the location of the handle.

Making this more precise would require a lot more words and/or some formal reduction rules, but I believe the core idea is sound. And in fact, I’ve been thinking about this implementation strategy for the better part of the past 4–5 months. The problem is that I don’t know how to neatly encode this idea into Haskell, at least not yet.

Possible Haskell encodings

Reifying Catch calls

One way to encode this would be to adjust the Error type to look something like this:

data Error e :: Effect where
  Throw :: e -> Error e a
  Catch :: Error e a
        -> (e -> m b)
        -> Error e b

The idea is that when a throw exn call is evaluated, it starts as a Throw exn value, but it’s wrapped in a Catch constructor each time it “passes through” a use of catch. In other words, we have reduction rules like this:

• throw x ⟶ send (Throw x)
• catch E[send x] f ⟶ send (Catch x f)

(Sorry, I couldn’t avoid some reduction semantics.)

But this isn’t actually enough. Note the m in the Catch constructor, which is existential—it’s totally useless to the Error handler. The Catch constructor would need to bundle a continuation that accepts an m b so that the handler can choose to resume from that point should it decide to do so. But wait—that means we have to capture the continuation eagerly for every catch involved, which eff takes great pains not to do! This is especially annoying given that any reasonable handler will unconditionally call that (most-nested) continuation.

The way I think about this is that eff takes great pains to be a very, very final encoding of algebraic effects, while free-like constructions are initial encodings. The fact that eff is a final encoding is what allows it to avoid reifying the entire computation as a tree, which breaks it up into many, many small continuations even if most of those continuations are not used in any interesting way. The above way of representing Catch is moving back in the direction of “reifying the computation as a tree,” but the reification happens “on demand”—i.e. when throw is called—rather than all the time.

“On demand” sounds great, like it’s an optimization, but in some situations it might actually be a deoptimization, since it can require duplicating work. If there are a lot of nested catch calls, you’d need to capture the continuation once per catch per call to throw, which could be expensive. A free-like encoding would only capture each continuation once (though to make that possible, it must capture them in lots of tiny chunks, which is what eff gets to avoid).

Local dispatch

To be more eff-like, we need to do less reification. Instead of reifying the program as a tree and passing that tree to the handler, we want to yield to the handler directly, then let it make decisions about what to do. If the handler says “capture the continuation,” then we say “whelp, guess we have to reify part of the program after all,” but if it says “resume computation” (extremely common!) we can save a lot of work.

This means that in an ideal world, the Error type would just look like this:

data Error e :: Effect where
  Throw :: e -> Error e a

When defining a handler for an Error effect, you would supply two functions:

1. Something to handle uncaught Throws, which runs if there’s no intervening catch. This is just like the handlers you write in eff today.

2. Something to handle a Throw in the context of a catch. This is a new kind of handler, because it would have to somehow get access to the e -> m a function associated with the call to catch.

This is totally doable, in theory. The problem is that the API for Haskell effect libraries relies on a nice trick that allows us to reuse GADT syntax as “effect definition” syntax. But now that we have these two different things—effect operations and scoping operators—how do we express that to the type system? We need some kind of separate Scope datatype now:

data Error e a where
  Throw :: e -> Error e a

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

throw x = send (Throw x)
catch m f = scoped (Catch f) m

And now handlers need to provide two functions: one for handling an unscoped send, and another for a scoped send. There are probably various ways of simplifying this API, but I don’t think it’s possible to make it as simple as the current eff API. Oh well. I think this is the only way forward, in the long-term, and I think this can (and must!) resolve the issues you describe. But we’re entering truly uncharted territory now.