unsafeCoerce derivable from Coroutine+locally+abort

[KingoftheHomeless]

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:

import Data.Either
import Control.Effect
import Control.Effect.Coroutine

data SomeAction :: Effect where
  SomeAction :: m () -> SomeAction m a

someAction :: SomeAction :< effs
           => Eff effs ()
           -> Eff effs a
someAction = send . SomeAction

runSomeAction :: b -> Eff (SomeAction ': effs) a -> Eff effs (Either b a)
runSomeAction b = handle (pure . Right) $ \(SomeAction m) ->
  locally m >> abort (Left b)

effUnsafeCoerce :: a -> b
effUnsafeCoerce a = fromLeft @_ @() undefined $ run $ do
  eta <-   runSomeAction a
         $ runCoroutine
         $ app
  interpret (\(SomeAction _) -> undefined) $ case eta of
    Right (Yielded () c) -> undefined <$ runCoroutine (c ())

app :: Eff '[Coroutine () (), SomeAction] a
app = someAction (yield ())

>  effUnsafeCoerce (False :: Bool) :: Int
140208895230160

This, unsurprisingly, still works if you use Error instead of abort directly.

runSomeAction :: b -> Eff (SomeAction ': effs) a -> Eff effs (Either b a)
runSomeAction b =
      lift
  >>> interpret (\(SomeAction m) -> locally m >> liftH (throw b))
  >>> runError

runCoroutine internally uses control0, so the culprit here is a nefarious interaction between control0 + locally + abort.

[KingoftheHomeless]

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
>

[KingoftheHomeless]

I think this issue is fundamental for effect systems with the following properties:

• Free monad-like, revolving around a central monad like Eff r where r is the row of effects.
• Supports effect introduction (raiseUnder :: Eff (e1 ': r) a -> Eff (e1 ': e2 ': r) a)
• Supports coroutines (launch :: Eff (Coroutine i o ': r) a -> Eff r (Status r i o a))
• Supports even basic Higher-Order effects, as long as you still have some way to execute handler-scope effects when interpreting a HO effect.
• Handlers can be affected by stateful operations of local effects. (E.g. when executing 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.

[lexi-lambda]

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

1. E1[runSomeAction E2[someAction m]]

to reduce to something like

2. 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.