interceptPartial - Polysemy

I modified intercept so that the handler must return Maybe:

interceptPartialUsingH ::
  ∀ e r a .
  Member e r =>
  ElemOf e r ->
  (∀ x rInitial . e (Sem rInitial) x -> Tactical e (Sem rInitial) r (Maybe x)) ->
  Sem r a ->
  Sem r a
interceptPartialUsingH pr f (Sem m) =
  Sem \ (k :: ∀ b . Union r (Sem r) b -> m b) -> m \ (u :: Union r (Sem r) x) -> case prjUsing pr u of
    Just (Weaving e s d y v) -> do
      result <- usingSem k $
        runTactics s (raise . d) v (interceptPartialUsingH pr f . d) $
        f e
      maybe (k $ hoist (interceptPartialUsingH pr f) u) (pure . y . (<$ s)) (join (v result))
    Nothing ->
      k $ hoist (interceptPartialUsingH pr f) u
{-# inline interceptPartialUsingH #-}

so that interpretation is deferred to the next interpreter if Nothing is returned, making it possible to create a catch-all case:

data Ip :: Effect where
  Ip :: Ip m Int
  Other :: Ip m Int
  Another :: Ip m Int

makeSem ''Ip

interpretIp ::
  Member (State Int) r =>
  InterpreterFor Ip r
interpretIp =
  interpret \case
    Ip -> pure 23
    Other -> gets (+ 5)
    Another -> pure 42

interceptIp ::
  Members [Ip, State Int] r =>
  Sem r a ->
  Sem r a
interceptIp =
  interceptPartial \case
    Ip -> Just 4 <$ put 3
    _ -> pure Nothing

test_interceptPartial :: UnitTest
test_interceptPartial =
  runTest do
    evalState 0 do
      (interpretIp . interceptIp) do
        i1 <- ip
        i2 <- other
        12 === (i1 + i2)

Not sure this is sane. @Love Waern (King of the Homeless) ?

It's sane, but (somewhat) redundant: the existing pattern to achieve the same thing is to re-send the effect, like this:

interceptIp ::
  Members [Ip, State Int] r =>
  Sem r a ->
  Sem r a
interceptIp =
  intercept \case
    Ip -> 4 <$ put 3
    u -> send (coerce u)

However, as you can see, doing so generically requires 1. using coerce; 2. using the still-internal-for-some-reason send 3. is only possible with first-order effects since interpretH is bad.
Yeah that's not exactly convincing. However, the in-progress rework of higher-order effect interpretation has a solution to all this, so I figure I should really just get to completing that rather than adding interpretPartial to polysemy.

Wait, you're using the inspector in the interpreter, and then discard the functorial state given by the calculation. Yeah, that's not sane.

ah, damn. didn't know about the coerce trick, that looks adequate.

regarding the discarded state, can you demonstrate how this could be preserved in my code?

I don't think you can with the weave abstraction as core. Again, I really should get to completing that core rewrite.

It is done, really. The only thing really holding it up is some questions about complexity, and "how much of the old API do we want to throw away vs. leave alone for backwards compatibility"

I'll work on it once I'm done with my other work for the day.

oh wow, awesome

are you working on your thesis still?

No, that one's complete. I've got an actual job now.

ah, nice :big_smile: did you mention that before? where you working at?

I'm working at Intel, at their simulator department. My thesis is called "Coroutines for Simics Device Modeling Language" -- Simics is the (primary) simulator in question. I'll probably work on implementing what my thesis is about, sooner or later. Anything more probably isn't safe to say.

The report will be public, but the university hasn't published it yet.

wow, sounds very impressive! that simulates cpus?

Simics is a full-system simulator: it simulates CPUs and peripheral devices interacting with the CPU and each-other.

Peripheral devices are simulated through high-level behavioral models, rather than RTL -- this allows simulation to be fast and development of device models simple.

Simics DML is the primary modeling language for such device models.

crazy. does this run in software only or some FPGA stuff?

Simics runs in software. You can probably rig it to make use of/connect FPGA:s; it's flexible.

My thesis concerns the fact that asynchronous procedures (especially communication) is very common in device models, yet DML does not have a dedicated abstraction for it -- so users are forced to roll FSMs, which are insanely boilerplate heavy.

So my thesis develops coroutine designs for use in DML to address that.

Only designs though -- which the thesis does not implement, it only suggests potential implementation approaches.

very curious to read that!

I'll let you know once the university decides to publish it. Beware, it's some like 120 pages long.

I write too much.

:grinning:

Turns out I'm too tired to work on it now. To make up for it a bit, I've pushed up yet another branch where you can look at the current progress of that core rewrite work. It's not completely polished.
I'm so tempted to just rip out all the old interpretH stuff and not care about backwards compatibility. The core rewrite is intended for v2.0 anyway, so there's a real argument to commit to that. That's the sort of decisions I shouldn't do alone, though.

https://github.com/polysemy-research/polysemy/tree/interpreth-powerful-wip

ooh, nice

Most notable, did a rewrite to Final, and RunH is now a very curious beast.

it basically depicts MonadTransControl in all but name

Oh yeah, and you can spot propagate there, too, which is the solution to the intercept stuff we talked about.

wow, interpretNew is crazy :sweat_smile:

so runM is now unified over Final and Embed?

and interpretNew is supposed to be used for first-order effects as well?

Love Waern (King of the Homeless) said:

Wait, you're using the inspector in the interpreter, and then discard the functorial state given by the calculation. Yeah, that's not sane.

I'm wondering, why is the put 3 in the example effectful? shouldn't it be discarded?

The university decided to stop dragging their feet after some nagging and published my thesis!

https://uu.diva-portal.org/smash/record.jsf?dswid=3769

Again, beware, 120 pages long.

The record could not be found. The reason may be that the record is no longer available or you may have typed in a wrong id in the address field.

:((

for some reason it redirects to a random dswid value every time

Found "Coroutines for Simics Device Modeling Language" by searching for "Love Waern"

yaaaay awesome!! :tada: :party_ball:

whoops, sorry, this should be permanent: http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-453889