-
Notifications
You must be signed in to change notification settings - Fork 18
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Incorrect semantics for higher-order effects #12
Comments
Error
effect
bad :: String
bad = run $ runReader "unlocaled" @String $ interpret (\SomeAction -> ask) $
local (\_ -> "localed") someAction And |
@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" |
This issue touches upon a few different things. Let me try to address them each in turn. First, you are correct that 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 In my experience, this is almost always the desired semantics. Consider a handler that installs an extra local 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 In that case, However, this on its own does not resolve your problem, because Here’s an example of how such a situation could arise. Suppose the programmer writes some code using a local Now, suppose the caller of (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:
This seems pretty fundamental, but let’s take a step back for a moment. Clearly, Well, no: the answer is that Is there a way out? Well, in theory, it ought to be possible to implement your But it turns out that even if we did that, your example would still do the wrong thing—the This has been a lot of information. Let me try to recap the key takeaways so far:
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:
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 |
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 That said, I'm afraid I have my wall of text of my own; my opinion is still that 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 If a handler wants an extra local The solution is to install a local 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 Given these points, I don't see what benefit As an example as to why 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 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
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 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 Note the following:
And alright, that's all well and good. In fact, maybe requiring 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 And of course, the same problem occurs with 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, About 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 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 The reason I'm skeptical towards Admittedly, I'm not very confident about these topics specifically (whether 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 To summarize my points:
|
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
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 problemIn 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:
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 But An alternative model of scopingThe root of the tension in
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 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 The current approach In a better world, handle @(Error e) h (... (catch (... (throw exn) ...) f) ...) then we want the 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 encodingsReifying
|
First-order effect systems like
freer-simple
can make use of interpreters/effect interception to have pseudo higher-order actions, likehandleError
andcatchError
.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
:Note that the exception doesn't get caught here even though both the use of
throwError
andcatchError
target the sameError
effect. Compare this topolysemy
, 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,Confirmed by @TheMatten.eff
uses the same approach asfreer-simple
for its higher-order effects -- the only difference betweenfreer-simple
'shandleError
andeff
'scatch
is that the interpretation done on-site withhandleError
is done within the interpreter forcatch
. In this case,eff
should have the same issue.The text was updated successfully, but these errors were encountered: