Continuation Effects

[KingoftheHomeless]

This adds the effects Cont and Shift, for abortive and delimited continuations respectively.

These effects work by being parametrized by s and m, where s is the final result type, and m is the final monad type. Polymorphic code with these effects are intended to be polymorphic in m, and may choose to be polymorphic in s. This way, you can get the traditional callCC/shift/reset operations. If you specialize s, you also get access to abort, which lets you end a computation early.

Unfortunately, the interpreters for these are wonky. The only way to transform Union r (Sem (Cont s m ': r)) x to Sem r x is to "replace" any higher-order use of values of type Sem (Cont s m ': r) within the union with a pure value of Sem r. The effect of this is that any continuation you get with callCC/shift is unaffected by higher-order operations such as local and censor, and listen on a continuation will just return mempty.

Still, it's pretty neat that this is at all even possible, considering ContT is not a functor on monads.

[isovector]

Coooooool! Thanks for the PR --- I think you're the first person to successfully navigate the Yo machinery.

The effect of this is that any continuation you get with callCC/shift is unaffected by higher-order operations such as local and censor, and listen on a continuation will just return mempty.

Is this still true if you invoke it via runReader . runCont, rather than runCont . runReader? Usually that's the way the semantics shake out for nested effects like these.

I'd love some tests for this to help me wrap my mind around what's going on, but happy to merge it after that!

[KingoftheHomeless]

Unfortunately, it's still true no matter the order of effects. The order of interpreters does affect some other stuff, like how continuations interact with errors, but otherwise, as far as I can tell, the way the interpreter is implemented makes it so any higher-order effect can't interact with a continuation in any significant way.

[isovector]

Unfortunately, the interpreters for these are wonky. The only way to transform Union r (Sem (Cont s m ': r)) x to Sem r x is to "replace" any higher-order use of values of type Sem (Cont s m ': r) within the union with a pure value of Sem r.

Can you point this out in the code? Usually the solution is to just hoist your interpreter, but maybe the types don't line up here?

[KingoftheHomeless]

It's specifically how other effects are threaded through. You can't hoist runCont since continuations (ContT) don't amount to a functor on monads. (To be more exact, I'd need to transform Sem (Cont s (Sem r) ': r) x to Sem r x for any x, without being provided a function x -> Sem r s, which just isn't possible.)

Instead, I use this weird embedSem thing, which has the effect I described. https://github.com/polysemy-research/polysemy-zoo/blob/75e8da5540b123b45f8b61921fd8e42541f89f21/src/Polysemy/Cont.hs#L75 https://github.com/polysemy-research/polysemy-zoo/blob/75e8da5540b123b45f8b61921fd8e42541f89f21/src/Polysemy/Cont.hs#L82-L88

[isovector]

Ahh, weird. Ok, one last suggestion before I resign myself to the inevitable weird semantics.

You can use lowerToIO to get a continuation capable of forall r x. Sem r x -> IO x. It comes at the cost of needing to run with IO as your last effect, but would that be enough to get rid of the janky pure semantics you're experiencing?

[KingoftheHomeless]

Maybe? I'll need to look into that a bit more. My gut reaction however is that lowering to IO will probably not fix this.

[isovector]

Fair enough. I'm out of my domain here, but out of curiosity, what is the primitive you'd need in order to implement this correctly? I can do some thinking on my end and see if it's possible to whip up.

[KingoftheHomeless]

The core issue is that I need to transform a Union r (ContT s (Sem r)) a to a ContT s (Sem r) a.

So a primitive would be something in the style of Monad m => (forall x. Sem r x -> m x) -> Union r m a -> m a. I don't think that's possible to implement.

[isovector]

We can do it so long as we have a Lift (Member m) r constraint.

foo :: (Monad m, Member (Lift m) r) => (forall x. Sem r x -> m x) -> Union r m a -> m a
foo lower e = runSem (liftSem $ hoist sendM e) (lower . liftSem)

But maybe this m is supposed to be the one existentialized inside of Yo? If so, we can use the (forall x. f (m x) -> n (f x)) thing to transform it back into a Sem r, and then use the (forall x. f x -> Maybe x) bit to (hopefully) drop the f away. You'd run into problems if an uncaught throw happened, but besides that it should be safe.

[KingoftheHomeless]

Is it possible to implement withLower :: (LastMember (Lift m) r, Monad m) => ((forall x. Sem r x -> m x) -> m a) -> Sem r a? Because then I could implement runContBase :: LastMember (Lift (ContT s m)) r => Sem (Cont s m ': r) a -> Sem r a with the proper semantics.

[isovector]

I don't think so, unfortunately. withLowerToIO works by spinning up a new thread that acts as an event loop, and then sending any unhandled effects off to it. In an arbitrary monad m we can't use that same trick, since there would be nobody to listen.

[KingoftheHomeless]

Perhaps if we also constrict m to be MonadIO, we could reuse your Forklift machinery? I'd then need a variant of withLowerToIO that has (LastMember (Lift m) r, MonadIO m) as a constraint rather than LastMember (Lift IO) r, but that definitely feels possible to do. Is it?

[isovector]

You could do it so long as you also have a forall x. m x -> IO x (since we need to run down to IO in the asynced thread).

[KingoftheHomeless]

Then unfortunately, we're back where we started. forall x. ContT s IO x -> IO x doesn't exist.

Unless a withLower or Monad m => (forall x. Sem r x -> m x) -> Union r m a -> m a primitive could be created, I'm beginning to think there's no solution to the weird semantics problem.

To explain a bit further, the m in the context of Monad m => (forall x. Sem r x -> m x) -> Union r m a -> m a is ContT s (Sem r), so Member (Lift (ContT s (Sem r))) r doesn't really work.

[isovector]

Makes sense. I'll do some pondering on this tonight, but I don't see a reason we couldn't get away with a withLowerToContTIO.

[KingoftheHomeless]

I just discovered that runCont/runShift will actually invalidate all higher-order effects of any interpreters that are run after it:

(run . runReader 1 . runCont) (local (+1) ask) == 1
(run . runCont . runReader 1) (local (+1) ask) == 2

So runCont/runShift should always be run near the bottom of the stack.

That's pretty damn bad, so finding a solution to threading effects through is pretty important if we want to add this effect.

[isovector]

I guess that makes sense; you're explicitly deleting them in embedSem, right? But yeah, scary!

[isovector]

One potential solution is to take a (forall x. Sem r x -> x) parameter a la runFixpoint and use this to solve the purification step. I suspect the only reasonable implementation would be run :: Sem '[] a -> a, which would force Cont to be the last effect in the stack --- though precludes the ability to do IO.

[KingoftheHomeless]

The problem also means that the reset implementations can't be used sanely. Fortunately, for Shift it's possible to implement reset as an action Member (Shift s m) r => Sem r s -> Sem r s (and have it behave sanely.)

I'm going to sleep now. I'll add some documentation/rework reset according to my discovery in the morning.

[ocharles]

Completely randomly throwing this out there, but may be a useful formulation:

https://twitter.com/importantshock/status/1117645530560069632

[ocharles]

See also section 5.2 of http://www.cs.kuleuven.be/publicaties/rapporten/cw/CW699.pdf

[KingoftheHomeless]

After some experimentation with that, it looks like the Jump/Subst formulation can be used to avoid the GADT trickery I used to represent the CallCC operation in the Cont/Shift effect, as well as only having one polymorphic variable instead of two (at the cost of losing abort). However, I still run into the exact same problems as I did for Cont/Shift when it comes to creating an interpreter for the effect.

Solving the effect-threading issue will allow us to use either formulation.

[KingoftheHomeless]

On another note: it's also possible to implement runContBase if its possible to implement the following:

withLower' :: (LastMember (Lift m) r, Monad m)
           => (forall f.
                   Functor f
                => f ()
                -> (forall x. f (Sem r x) -> m (f x))
                -> m (f a)
              )
           -> Sem r a

Perhaps that's easier to do?

[KingoftheHomeless]

Oh, yes. Here's a proof of concept.

data Lift' m m' a where
  WithWeaving :: (forall f.
                      Functor f
                   => f ()
                   -> (forall x. f (m' x) -> m (f x))
                   -> (forall x. f x -> Maybe x)
                   -> m (f a)
                 )
              -> Lift' m m' a

withWeaving :: Member (Lift' m) r
            => (forall f.
                   Functor f
                => f ()
                -> (forall x. f (Sem r x) -> m (f x))
                -> (forall x. f x -> Maybe x)
                -> m (f a)
              )
           -> Sem r a
withWeaving wa = send $ WithWeaving wa

sendM' :: Monad m => Member (Lift' m) r => m a -> Sem r a
sendM' m = withWeaving $ \s _ _ -> fmap (<$ s) m

runM' :: Monad m => Sem '[Lift' m] a -> m a
runM' (Sem sem) = sem $ \u -> case extract u of
  Yo (WithWeaving wa) s wv ex ins -> fmap ex (wa s (runM' . wv) ins)

runContBase :: forall s m a r.
                Member (Lift' (ContT s m)) r
             => Sem (Cont s m ': r) a
             -> Sem r a
runContBase (Sem sem) = sem $ \u -> case decomp u of
  Right (Yo e s wv ex _) -> case e of
    CallCC cc -> withWeaving $ \s' wv' _ -> ContT $ \c ->
      (`runContT` (c . fmap ex)) . wv' . (<$ s') . runContBase . wv $
        cc (\a -> send . Abort $ c (ex (a <$ s) <$ s'))
        <$ s
    Abort m -> sendM' $ ContT $ \_ -> m
  Left g -> liftSem (hoist runContBase g)

(`runContT` pure) . runM' . runReader 1 . runContBase $ local (+1) ask == 2
(`runContT` pure) . runM' . runContBase . runReader 1 $ local (+1) ask == 2

So that's one problem solved. Unfortunately, higher-order effects still don't work with continuations for some reason, implying the effect-threading wasn't the core cause. I'll reformulate in terms of Subst and see what results I get.

[KingoftheHomeless]

Doesn't matter how you formulate the effect, and the reason is that in whatever case, callCC boils down to this:

callCC :: Member (Lift' (ContT s m)) r => ((forall b. a -> Sem r b) -> Sem r a) -> Sem r a
callCC cc = withWeaving $ \s wv _ ->
  ContT $ \c ->
    runContT
      (wv $
        cc (\a -> sendM' . ContT $ \_ -> c (a <$ s))
        <$ s)
    c

Higher-order effects don't affect a lifting unless they are interpreted in terms of the lifting. So if we, say, have a base monad stack of ContT s (ReaderT i (StateT s m)) a then we could apply lift both reader operations (since local is one of the few higher-order operations that ContT can lift), and writer operations (since those can be interpreted in terms of state), and apply them to continuations. Unfortunately, we still can't catch exceptions of continuations, since ContTcan't lift catch.

[KingoftheHomeless]

Here's a gist with an example of how this would look like: https://gist.github.com/KingoftheHomeless/632b5817c8430fa8e47e5b70f81a624b

As a further argument to the usefulness of Lift', I was able to implement runReaderInMonadReader with it, which I don't think is possible with regular Lift.

My initial attempt at a runWriterInMonadState is too janky, and as a result, the results are weird. I'll try to make a better solution in an hour.

[isovector]

I'm really excited about this. It's nice to see that runCont no longer poisons higher order effects.

I agree that runReaderInMonadReader probably isn't implementable using existing abstractions in polysemy. I'm not convinced of its utility, but could be persuaded!

Can you summarize the problems remaining with these effects? I'm afraid I've lost track of the current goal.

[KingoftheHomeless]

Ok, to sum up my discoveries:

The pure interpreters for any Cont/Shift/Subst effects have the double issues that:

1. Continuations are unaffected by higher-order effects.
2. Any higher-order effects whose interpreters are run after the interpreters for Cont/Shift/Subst will be discarded.

These issues for the pure interpreters can only be fixed if there exists a primitive

Monad m => (forall x. Sem r x -> m x) -> Union r m a -> m a

Which I don't believe there is.

However, given access to a withWeaving operation, it's possible to create interpreters for Cont/Shift/Subst that send these effects to a ContT that is lifted within the effect stack. (In fact, Subst's actions can be sent to any MonadCont)

These interpreters avoid problem number 2, which is by far the more severe one. In addition, these allow for higher-order actions to work on continuations, if the interpreters for those effects send those actions to the same monad transformer stack. (For example, runReaderInMonadReader) In this case, the way these effects resolve depends on the monad transformer stack.

I've shown that a withWeaving effect is achievable through Lift'. It's not an option to simply replace Lift with Lift', because runEmbedded and runIO can't handle withWeaving being used onIO. However, I firmly believe withWeaving on a monad m should be implementable given LastMember (Lift m) r, without any issue (because in those scenarios Lift IO isn't the last member of the stack, and thus there can't be any use of withWeaving on IO)

withWeaving is desirable for other purposes, as it allows for greater flexibility when writing interpreters that sends effects to a base monad transformer stack.

So in conclusion, if we have withWeaving, we can get sensible continuation effects.

Perhaps Lift could be expanded like this?:

data Lift m z a where
  Lift :: { unLift :: m a } -> Lift m z a
  WithWeaving :: LastMember (Lift m) r
              => (    forall f.
                      Functor f
                   => f ()
                   -> (forall x. f (Sem r x) -> m (f x))
                   -> (forall x. f x -> Maybe x)
                   -> m (f a)
                 )
              -> Lift m (Sem r) a

[KingoftheHomeless]

I'm looking at making an operation like withWeaving part of LastMember, will report later.

[KingoftheHomeless]

Oh, there's actually a much easier solution!

runM' :: Monad m => Sem [Lift' m, Lift m] a -> m a
runM' (Sem m) = m $ \u -> case decomp u of
  Right (Yo (WithWeaving wav) s wv ex ins) -> ex <$> wav s (runM' . wv) ins
  Left g -> case extract g of
    Yo (Lift m) s _ ex _ -> fmap (ex . (<$ s)) m

This way, everything works out. withWeaving relies on the Lift' m constraint, Lift isn't replaced, so runIO and runEmbedded still work. Plus, things that rely on LastMember (Lift IO) still work.

My opinion is that we give Lift' a better, catchier name, and then add it to polysemy.

[isovector]

I really like the elegance of the '[Lift' m, Lift m] solution. Great intuition on working that out! I'd be more than happy putting it in the core library. Maybe Final would be a better name than Lift'?

How convinced are we that problem 1 is unsolvable? Does it deserve more thinking?

[KingoftheHomeless]

From what I can tell, there's only one higher-order effect in mtl you can get to work on a continuation: local. This works by having the base monad stack be ContT s m, where m is MonadReader, and then use runReaderInMonadReader in order to interpret the Reader effect. This is because ContT actually lifts MonadReader properly!

For anything else, I don't think there's anything we can do.

[KingoftheHomeless]

This is subject to a rework once #35 lands. Will probably be tomorrow's task.

[KingoftheHomeless]

Final has landed. I'll rework this in the morning.

[isovector]

Excellent, thanks! Looking forward to having this in!

[KingoftheHomeless]

This will take a little time, I'm trying to figure out the best way to resolve the problem of the horrible semantics of the pure interpreters.

My idea is that I have "safe" and "unsafe" variants of everything, where the "safe" variants have their types restricted such that they have to be the last interpreter before run/runM. I'm also trying to create weaker versions of Cont/Shift that can always be interpreted safely.

You can probably expect something the day after tomorrow.

[KingoftheHomeless]

The meat is up, will write tests tomorrow.

[KingoftheHomeless]

Tests are up. This is ready to be merged if you are ok with it.

[isovector]

Awesome! I'll do a review pass tomorrow. Thanks again!

[KingoftheHomeless]

If you want. How would we call one another? Discord?

I honestly don't like Cont and Shift very much because of the very weird semantics of the non-Final interpreters. Capture is a fine effect, but I'm actually most proud of Final. I think that effect really is very useful.