cross-interpreter errors - Polysemy

Greetings, fellow humans!

As a follow-up to this topic https://funprog.zulipchat.com/#narrow/stream/216942-Polysemy/topic/Either.20vs.20Error where @Love Waern (King of the Homeless) produced a brilliant bit of code, I have riffed on that code some more to produce this experiment:

https://github.com/tek/polysemy-resume

I introduced an effect Stop that is Error without the catch, for the purpose of marking errors that should be handled by the Resumable effect (called Exceptional in the original).
What I added is the possibility to handle the error totally so that the requirement for an additional Error constraint on the consuming program/interpreter is removed.

@Love Waern (King of the Homeless) , I would be very grateful if you could look over the implementation, especially to see if I'm doing unnecessary decompositions and weavings and the like.

oh, a significant mechanism here is that I pass the backing interpreter into the wrapper and execute it in the unwrapped Sem, I think

first problem I'm seeing is that other dependencies of the consumer seem to be causing confusion

:thumbs_up: I figured Exceptional (or Resumable) had promise. Looking through this more closely now.

resumable and resumableFor can be relaxed significantly:

resumable ::
  ∀ eff err r .
  InterpreterFor eff (Stop err ': r) ->
  InterpreterFor (Resumable err eff) r
resumable interpreter sem = Sem $ \k -> runSem sem $ \u ->
  case decomp (hoist (resumable interpreter) u) of
    Right (Weaving (Resumable e) s wv ex ins) ->
      let
        sem' =   interpreter
               $ liftSem
               $ weave s (raise . raise . wv) ins (injWeaving e)
      in
        distribEither s ex <$> runSem (runStop sem') k
    Left g -> k g

I recommend getting rid of those helper functions with the extremely large signatures (like injectStopand injectWithStop). Here, I simply inlined what they're doing.

it was way worse before :big_smile:

mostly in order to understand the types

True, Weaving is weird. When I first learned the internals of the library I had stare at it for a while before I got it.

I will have to stare a bit longer, but this thing definitely gave me some helpful insights

The deeper implementation of runState is probably a good place to look at. That was one of my learning resources.

Here's resumableFor:

resumableFor ::
  ∀ eff smallErr bigErr r .
  Member (Stop bigErr) r =>
  (bigErr -> Maybe smallErr) ->
  InterpreterFor eff (Stop bigErr ': r) ->
  InterpreterFor (Resumable smallErr eff) r
resumableFor from interpreter sem = Sem $ \k -> runSem sem $ \u ->
  case decomp (hoist (resumableFor from interpreter) u) of
    Right (Weaving (Resumable e) s wv ex ins) ->
      let
        sem' =   interpreter
               $ liftSem
               $ weave s (raise . raise . wv) ins (injWeaving e)
      in
        fmap (distribEither s ex) $ runSem (runStop sem') k >>= \case
          Left exc -> maybe (k $ inj $ Stop exc) (return . Left) (from exc)
          Right a  -> return (Right a)
    Left g -> k g

That should allow you to clean up most boilerplate. Everything else in the modules looks alright (although I won't touch Polysemy.Resumable.Prelude). Some observations:

• You may want to add more Resumable interpreters. I think a parallel of runExceptional is still warranted. You may also want to add

resumableSimple :: (forall q x. eff q x -> Sem r (Either err x)) -> InterpreterFor (Resumable err eff) r

Or something of the like.

• Stop is intended to be used only by an interpreter that signals when a Resumable should abort, right? In that case, resumableFor's Stop bigErr constraint seems weird; you may want to change that to Error.

yeah the Prelude is just copied from another project, don't mind it. and providing some more convenient combinators is definitely on my list

and the Stop constraint, I noticed as well

I think I just generally find it helpful to have these signatures explicit when I come back to it later to change something

btw, could you imagine a way that errors could be made a first-class component of the weavings?

Not sure what you mean by that. As in, having error management be part of the definition of Weaving? I don't think that's a good idea.

yeah, something like that, like bifunctor IO approaches. I'm just thinking that it is such an integral part of (at least empirically from my perspective) effects that I feel it should be more prominent

That would be a big change I wouldn't know how to approach properly. I feel that's something best left for future work, once effect systems are more properly understood.

I wouldn't be a proponent of having it be part of polysemy.

It's... maybe-ish possible? But the paths I see wouldn't gel with polysemy's architecture.

I didn't want to propose this as a feature for Polysemy, just a general idea

would be interesting, in any case

I'm sympathetic; exceptions are important enough to be given special treatment. It's something that warrants more research.

Perhaps something I can look into once I finally release the effect library of my own.

oh, is that in the works??

It's honestly already finished. I'm really only putting a few finishing touches on the documentation.

Probably be releasing it in the weekend.

just casually breaking some huge news :sweat_smile:

I think I gave hints here and there. :P Eh; I don't think it'll rival polysemy. It's too complicated for that. However, it does do stuff no other effect library does that makes it very powerful, which is why I'm releasing it.

sounds intriguing!

It's also why I'm documenting the hell out of it.

could you explain what you did in the rewrite of resumableFor where you use the k twice?

So k :: forall x. Union r (Sem r) x -> m x for the universally quantified monad m. This can be thought of as a m-based handler for effects in r; i.e. an implementation of those effects for m. In k $ inj $ Stop exc, I'm using k explicitly to perform the Stop exc effect in m (which I can do since Member (Stop exc) r). This is equivalent to runSem (stop exc) k.

is there an advantage over runSem (stop exc) k?

Faster. That's it, really. With enough inlining, GHC will reduce runSem (stop exc) k to k $ inj $ Stop exc.

ah, ok. and why did I not have to use k twice? what is the equivalent of that in my implementation?

you can also just do:

  fmap (distribEither s ex) $ (`runSem` k) $ sem' >>= \case
    Left exc -> maybe (stop exc) (return . Left) (from exc)
    Right a  -> return (Right a)

Which is perhaps easier to understand

Maybe that's what you did.

ah, it's in resumePartial

great, got it!

just a few hours and half the knowledge about the data flow is already gone

gotta stare at it a little longer!

alright, implemented most of your suggestions. can't deny that the code duplication makes me itchy though :sweat_smile:

also I added a variant of resumeFor that uses Either for the small exception, so the unhandled error can be transformed as well.

You forgot the most important part: the updated type signatures!

resumable ::
  ∀ eff err r .
  InterpreterFor eff (Stop err ': r) ->
  InterpreterFor (Resumable err eff) r

That's what I meant by "relaxed significantly".

The way resumable looks now, you can't make use of any effects in r in the provided interpreter.

ahhhh

wonderful

I haven't put any thought into runResumable though, it just catches Error

do you think it is reasonable to have that separate Stop effect?

I'd say so. The ability to catch is meaningless inside the interpreter provided to resumable. Stop exc also means it doesn't conflict with a potential Error exc effect the user may make use of.

runResumable looks fine, btw.

but it means that with runResumable, you can't use Stop

what would be a use case of runResumable that wouldn't be possible with resumable?

Yeah. Stop is only intended to be used specifically by the interpreters provided to resumable/For, right? runResumable is a different beast. It uses Error exc because it needs to catch, and the Error exc effect is also used by other parts of the program -- including the eventual eff interpreter, which may throw an exception when interpreting eff.

There is no use case of runResumable that wouldn't be possible with resumable. resumable can be used to implement everything else. runResumable and resumableFor are useful specializations.

right, right. maybe it should be renamed as catchResumable or so.

I'm still trying to wrap my head around what precisely we're abstracting here, I've basically started from the middle

I still view this as Exceptional. It's for safely using effects that may throw exceptions by forcing application code to eventually handle them.

The interpreter provided to resumable defines both how to interpret eff and when an exception is thrown (through Stop).

I guess I'm wondering about what intention is being signaled when using stop, and how it would be more indicated than throw in isolation (i.e. not relating it to other interpreters)

Love Waern (King of the Homeless) said:

The interpreter provided to resumable defines both how to interpret eff and when an exception is thrown (through Stop).

right, we're explicitly providing the interpreter as a stopping one

To me, stop signals throwing an exception. Perhaps the naming is unfortunate, but throw is already taken. We don't want to use Error in resumable because we have no use for catch.

Love Waern (King of the Homeless) said:

I still view this as Exceptional.

is there any preexisting connotation to this term that I don't know of?

Nah, I mean it as a simple play on words: Exceptional err eff: "the effect eff is exceptional! I.e. it may throw exceptions of err".

Love Waern (King of the Homeless) said:

To me, stop signals throwing an exception. Perhaps the naming is unfortunate, but throw is already taken. We don't want to use Error in resumable because we have no use for catch.

right, I think about it as being less "fatal" than an error

it all makes sense but I have the feeling there's much more to it :sweat_smile: errors are really complex

alright, I guess I'm satisfied. now to implement some combinators

one thing I do a lot is to just rethrow errors, maybe wrapped in a larger one

still wondering about a better name. I like resume, but stop is not optimal. something like short-circuiting…

abort is the one left from typical names for throwing exceptions, but even that feels too fatal. I dunno.

that's what I used at first :sweat_smile:

but then I felt weird talking about abortions all the time

Anyway, I need to sleep now. Talk to you later.

good night!

released!

https://hackage.haskell.org/package/polysemy-resume

todo now: multiple errors?

added an operator for Resumable:

Member (Http ! HttpError) r =>