Open arybczak opened 1 year ago
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).
I'm thinking, since Sp forbids effectful fork
ing, maybe we could just alter Env
to store IORef
s 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.
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.
I was curious why
speff
is so much better at countdown thaneffectful
and saw that access to an effect handler is just a single array access (for comparisoneffectful
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 https://github.com/hasura/eff/issues/12.I presume
interpose
exhibits similar behavior, i.e. given effectsA
andB
, if you make an effect handler ofA
use operations ofB
, theninterpose
handler ofB
and call an operation ofA
, it'll use the old handler ofB
, not the interposed one.