Semantics of higher order effects

[arybczak]

I was curious why speff is so much better at countdown than effectful and saw that access to an effect handler is just a single array access (for comparison effectful accesses a few arrays, an IORef and performs safety checks), so that makes sense. However, looks like this approach suffers from the same problem described in hasura/eff#12.

import Sp.Eff
import Sp.Util

data SomeEff :: Effect where
  SomeAction :: SomeEff m String

bad1 :: Either String String
bad1 = runEff . runError @String $ do
  interpret0 (\SomeAction -> embed $ throw "not caught") $ do
    send SomeAction `catch` \(_ :: String) -> return "caught"

bad2 :: String
bad2 = runEff . runReader "unlocaled" $ do
  interpret0 (\SomeAction -> embed $ ask) $ do
    local (\_ -> "localed") $ send SomeAction

>>> bad1
Left "not caught"
>>> bad2
"unlocaled"

I presume interpose exhibits similar behavior, i.e. given effects A and B, if you make an effect handler of A use operations of B, then interpose handler of B and call an operation of A, it'll use the old handler of B, not the interposed one.

[re-xyr]

Your observation is correct, and the reason why I haven't implemented it is that I really want Sp to be sound (the current semantics is - it's just unintuitive), but we all don't know if the "handler pointer" implementation in cleff actually is sound. Alexis has hinted that, given scoped resumptions, we can actually have this semantics, but she never described that in detail, whether formally or with code. It'd probably take some time for me to come up with a sound implementation (or with a conclusion that such an implementation is just impossible).

[re-xyr]

I'm thinking, since Sp forbids effectful forking, maybe we could just alter Env to store IORefs to handlers? Therefore

interpose = dynamicWind (...write in new handler...) (...restore old handler...)

The only way to escape caller's scope and actually do something outside is via control, and dynamicWind takes care of that; as soon as control skips over the prompt frame of interpose, the old handler is restored.

This proves to have some interesting interactions. Your program will return Right "caught" now, and if we rewrite the handler of SomeEff to

\SomeAction -> control \k -> throw "not caught"

then it will return Left "not caught", and this is not unintuitive as well - control is explicitly supposed to bring you out of the scope of the caller!

Next we can also consider:

\SomeAction -> control \k -> k (embed $ throw "not caught")

This produces Right "caught" and rightly so, because the action passed into the continuation is supposed to be within caller's scope. This semantics seem pretty neat, and it'd be nice if it turns out to be sound.

[re-xyr]

I experimented a bit and here's the benchmark numbers:

All
  countdown
    10000
      sp.shallow: OK (0.22s)
        213  μs ±  19 μs, 1.3 MB allocated, 116 B  copied, 6.0 MB peak memory,       same as baseline
      sp.deep:    OK (0.22s)
        214  μs ±  16 μs, 1.3 MB allocated, 304 B  copied, 6.0 MB peak memory,       same as baseline
  pyth
    32
      sp.shallow: OK (0.20s)
        1.67 ms ±  99 μs, 3.2 MB allocated,  12 KB copied, 6.0 MB peak memory,       same as baseline
      sp.deep:    OK (0.14s)
        4.32 ms ± 423 μs, 8.5 MB allocated,  37 KB copied, 6.0 MB peak memory,       same as baseline
  catch
    10000
      sp.shallow: OK (0.38s)
        1.43 ms ±  50 μs, 5.6 MB allocated, 681 KB copied,  11 MB peak memory,       same as baseline
      sp.deep:    OK (0.76s)
        1.47 ms ± 147 μs, 5.7 MB allocated, 679 KB copied,  11 MB peak memory, 23% less than baseline
  local
    10000
      sp.shallow: OK (0.48s)
        928  μs ±  59 μs, 4.0 MB allocated, 111 KB copied,  11 MB peak memory, 55% more than baseline
      sp.deep:    OK (0.23s)
        861  μs ±  78 μs, 4.0 MB allocated, 112 KB copied,  11 MB peak memory, 29% more than baseline

Regression is present in runReader but not runError, which is pretty strange.