Closed KingoftheHomeless closed 3 years ago
I suspect you can implement unsafeInterleaveIO
with IOE
+Coroutine
+locally
using a similar tactic, so it's probably more control0
+locally
that's dangerous.
Edit: yup.
data Interleave r :: Effect where
Interleave :: m () -> Interleave r m r
runInterleave :: IOE :< effs
=> IO a
-> Eff (Interleave a ': effs) b -> Eff effs b
runInterleave io = handle pure (\(Interleave m) -> locally m >> liftH (liftIO io))
effUnsafeInterleaveIO :: forall a. IO a -> IO a
effUnsafeInterleaveIO io = do
stat <- runIO
$ runInterleave io
$ lift
$ runCoroutine
$ app' @a
return $ run $ interpret (\(Interleave _) -> undefined) $ case stat of
Yielded () c -> runCoroutine (c ()) >>= \case
Done a -> return a
app' :: Eff '[Coroutine () (), Interleave r] r
app' = send $ Interleave (yield ())
> a <- effUnsafeInterleaveIO (putStrLn "interleaved")
> a `seq` pure ()
interleaved
>
I think this issue is fundamental for effect systems with the following properties:
Eff r
where r
is the row of effects.raiseUnder :: Eff (e1 ': r) a -> Eff (e1 ': e2 ': r) a
) launch :: Eff (Coroutine i o ': r) a -> Eff r (Status r i o a)
)locally m >> liftH (globalAction)
, if m
executes a yield
, then liftH (globalAction)
will be suspended as part of the local coroutine).This should be enough to do the dance in the OP that allows you to smuggle a computation that relies on a handler scope effect to outside of that scope, at which point you can't have any reasonable semantics (since doing this circumvents type-safety). So at least one of these has to go.
Perhaps the most attractive target is the last property. polysemy
doesn't have it, since within a interpretH
all stateful operations of more local effects are reified within a functorial value, so any local effects can't affect the interpretation of more global effects.
The problem then is that locally
can't keep the signature it has. Imagine if we had a local computation m :: Eff effs' e
and a global effect Error e
. Then you could write locally m >>= throw
, and so the only way throw
can be executed here is if it were, in fact, dependant on the local effects of m
.
Perhaps you can do something similar to polysemy, where you reify statefulness of local effects:
locally :: Eff effs' a -> Handle localState eff effs i r effs' (localState a)
But then you've probably reimplemented weave
, and weave
has many noted issues, including not supporting coroutines and nondeterminism.
The easiest solution is probably to get rid of coroutines, but that means discarding or heavily restricting the control
combinators, which may also kill nondeterminism.
Another option is to become first-order (discard locally
) and implement higher-order actions using freer-simple
's pseudo higher-order actions approach. This isn't that bad, since it won't cause any change in semantics compared to how eff
's predefined higher-order effects work today. However, it means users won't be able to define and interpret their own higher-order effects.
Perhaps there are some other solutions than the ones I listed above, but I can't imagine one which wouldn't require a big change to eff
's interface.
This is obviously a bug (and a rather bad one), but I have a different diagnosis, probably because I’m thinking in terms of continuations. The issue is that locally
is just fundamentally busted, in a far more egregious way than I had considered. It only works properly if it is called in tail position with respect to the handler function.
The conceptual idea behind locally
is to have a way to express “hey, I want to resume the computation right where I am, I just want to add a bit of new context.” The hope was that this would allow certain patterns (such as scoping operations) to be implemented very efficiently, since we wouldn’t need to capture and restore the continuation. Alas, your example illustrates this fundamentally cannot work.
I like the following simpler example to illustrate why this is so hopeless. Consider a handler like this:
runSomeAction :: Eff (SomeAction ': effs) a -> Eff effs a
runSomeAction = handle pure \case
SomeAction m -> locally m >> locally m
Here we execute an action “right where we were,” then do it again after it returns. But what does the second use of locally
mean? The computation has run off and done other things, and those things may have thrown all the local evaluation context (i.e. the evaluation frames between runSomeAction
and someAction
) away; the only way to do the same thing safely is to restore the local evaluation context again.
In other words, we want
E1[runSomeAction E2[someAction m]]
to reduce to something like
E1[runSomeAction E2[m >> control \_ -> runSomeAction E2[m]]]
so that once we finish the first evaluation of m
, we throw the new context away, replace it with the old context, and try again. This is possible to implement, but it cannot be implemented efficiently (Handler
is a monad, and we can’t predict whether or not locally
will be called), so it’s a lost cause.
locally
is currently just a hack for supporting scoped operations. As discussed in #12, it’s a bad hack. I’ve been thinking about how to replace it with something else that fixes the problems discussed in #12 and would allow eliminating it altogether, avoiding the problems discussed in this issue. I am still working out the details, but I think it’s doable, and that would kill two birds with one stone.
As I was studying @lexi-lambda's comment here, I realized that disappearing handlers through coroutines could be unsafe as-is. After some experimentation, turns out I was right:
This, unsurprisingly, still works if you use
Error
instead ofabort
directly.runCoroutine
internally usescontrol0
, so the culprit here is a nefarious interaction betweencontrol0
+locally
+abort
.