I learned quite a lot about extensible effects in the past few days and the puzzle pieces are slowly coming together. Let me summarise.
Dynamic vs. Static effects
I think part of the confusion is this: When people talk about effect systems, it is unclear whether they mean a type system that tracks effects or one which allows to extend the language with custom effects, the implementation of which is determined by a (usually lexically-enclosing) handler. These languages often implement effects and handlers by translating to delimited control operators with special support in the runtime. In particular, delimited control operators allow for custom control effects that may choose to discard the continuation and thus implement stack unwinding.
Haskell libraries such as effectful provide the capability to define such extensible effects and their corresponding handlers. I think an extensible effect is what effectful calls a “dynamically-dispatched” effect, because an effectful program is given meaning dynamically depending on the installed effect handlers.
Edit: However, I think effectful does not support extensible control effects, only effects that do not need delimited continuations.
It is simple to implement Reader, State, Exception, … effects wrt. delimited continuations (which is neither what effectful nor bluefin does).
NB: Effects are actually (uses of) classes, not instances, so the mtl equivalent would be MonadReader, MonadState, MonadThrow. Effectful programs have their semantics fixed by providing them with the corresponding effect handlers (instances at ReaderT, StateT, …).
It is a reality that GHC’s specialiser gives up at some point. If effectful programs cannot be specialised for their handlers, they will be quite inefficient! Yet still much much more efficient than the alluded unspecialised mtl-style encoding, where even (>>=) cannot be specialised.
I think this was the reason that @lexi.lambda wanted to introduce delimited control ops: So that inevitably unspecialised/dynamically-dispatched control-effectful programs still have decent performance in the absence of any custom effect.
Yet, the unspecialised, dynamic effect handler implementation of effects such as Reader, State and Exception in terms of delimited continuations is pretty inefficient, because any operation will need to copy a fragment of the stack, as required by delimited control operators and quite unnecessary for something as simple as ask. Therefore, effectful eschews control operators and furthermore came up with the notion of statically-dispatched effects, which is basically a manual specialisation of effects for a particular effect handler.
These statically-dispatched effects are not implemented in terms of inefficient delimited control ops nor dynamic handles, but in terms of specialised implementations. See also the next section.
As I understand it, bluefin takes the pragmatic stance that people are unlikely to truly need extensible/dynamic effects (question (2) in the OP is exactly about that), and thus only provides static implementations.Case in point: there is not a single occurrence of prompt#/control0# in its repo. It provides means to write custom Compound effects for building larger effects out of the builtin ones, though. Great ergonomics and usefulness of its API aside, I would say it is an effect-tracking library, but not an extensible effects library. effectful is in the latter category.
Edit: This statement was misguided; it appears that bluefin simply does not support extensible control effects and hence does not use delimited continuations, but that’s just like effectful.
bluefin-algae, on the other hand, adds control effects to bluefin as well by providing a wrapper around the delimited control primops.
Specialising for known effect handlers implemented using delimited control
To get a feeling for what is inefficient about the dynamic delimited control implementation: The usual effect handlers for Reader, State, etc., that correspond to mtl instances for ReaderT and StateT, etc., are tail-resumptive. This means their effect handlers do not actually modify the stack.
For example, ask (MkReader tag ref) = control0 tag (\k -> k (readIORef ref)) is equivalent to readIORef ref, and that is at least its static implementation in bluefin.
In general, implementing tail-resumptive handlers in terms of control0# tag (\k -> k e) (which copies the stack into the heap just to immediately resume it) is absolute overkill! Hence I propose to add a rewrite rule to GHC here: #25490: Delimited Continuations: Optimise tail-resumptive operations · Issues · Glasgow Haskell Compiler / GHC · GitLab.
Likewise, Exceptions never resume, meaning they unconditionally discard the continuation k (control# tag (\_k -> handle exn), NB: _k dead), so it is absolute overkill to copy the stack as well.
Hence I propose to add a new primop to GHC that simply aborts the prompt and does not copy the stack at all (pretty much like raiseIO#), plus a corresponding rewrite rule: #25489: Delimited Continuations: Implement `abort#` to avoid copying the continuation · Issues · Glasgow Haskell Compiler / GHC · GitLab.
Net result: Reader, State and Exception can be implemented dynamically just as efficiently as statically. Now, I would like to see GHC improve such that any known, dynamic implementation is as efficient as its static counterpart. This would ensure that dynamic effects implemented by users can be just as efficient as the builtin static ones. Fixing the issues linked above should go some way towards that. However, I can see two problems:
- I’m a bit skeptical about custom
Exception, because prompt/control0 is not expressive enough to express async-exception safe bracket.
- Imagine a computation using a
Reader effect, compiled separately from the vanilla Reader effect handler. In order to get good code for the effectful computation, we would need to specialise it for the effect handler/capability. That is likely to fail at some point when the computation becomes too large. So it seems the effectful design where we can choose between dynamic and static dispatch seems quite important in practice, because AFAIU static dispatch ensures that we do not need to do a costly control0#.
That said, I have mixed feelings about control0#. Since it is not zero-cost and I almost never need the full generality that it offers, I would try to avoid it at all cost, which is impossible when specialisation fails. If GHC had segmented stacks like OCaml seems to have, we could make it near zero-cost, perhaps so much that it doesn’t matter much when specialisation fails. Perhaps that would allow effectful and bluefin to offer extensible control effects as well.
Higher-order effects
Higher-order effects are effect ops that take effectful computations as arguments, for example local.
It is a bit challenging to support extensible (dynamically-dispatched) higher-order effect ops.
NB: local is supposed to be an effect op and not a derived implementation in terms of ask.
In effectful, I think you would write
data Reader r :: Effect where
Ask :: Reader r m r
Local :: (r -> r) -> m a -> Reader r m a
and then have a handler (roughly, not type-checked.)
runReaderVanilla r m = newIORef r >>= \ref -> interpret_ go m
where
go Ask = liftIO (readIORef ref)
go (Local f m) = do
r <- liftIO $ readIORef ref
liftIO $ writeIORef ref (f r)
a <- m
liftIO $ writeIORef ref r
return a
(I think I must actually use interpret instead and do something like a <- localSeqUnlift env $ \unlift -> unlift m instead of a <- m. Bother.)
This is just one effect handler for Reader. Others (i.e. logging ones) are conceivable.
Note how the encoding of Local as part of the Reader data declaration is not entirely trivial, and how I should have actually used interpret instead of interpret_…
If your effect is statically-bound, there is just one effect handler. Any occurrence of local can be specialised for that effect handler and you do not need to think long and hard about how to encode higher-order effects or what they mean.
This also means you cannot monkey-patch the definition of local after the fact to support logging.
(But as Tom has demonstrated, there are often different ways to introduce seams that achieve logging etc.)
My personal summary regarding bluefin: since the encoding of higher-order effect operations is only really challenging in the dynamically-dispatched scenario, and bluefin does not really support extensible, dynamically-dispatched effects, bluefin can be quite a bit simpler.
Users who want dynamically-dispatched effects can use bluefin-algae, though! All the trickyness wrt. higher-order effects apply there. I’m a bit unsure whether the current implementation supports higher-order effects such as Local above. Perhaps @lysxia knows?
Edit: Since a few days ago, bluefin seems to support extensible (non-control) effects as well. I haven’t reviewed it yet.
Edit: Conclusion: bluefin and effectful seem to offer extensible non-control effects. For control effects use bluefin-algae, but be aware that performance of control0# might be insufficient unless someone implements segmented stacks in GHC.
Another conclusion is that perhaps effect systems should offer a means to annotate effect declarations with the class of effect. I.e., whether it is a control effect (so is not tail-resumptive), whether it is aborting (i.e. discards the continuation like raiseIO#), or multi-prompt etc. That would allow for suitably constrained dynamic implementations that would still perform well. I believe specialisation could be achieved by a suitable type class algebra. Aha, indeed this is exactly what Koka does! There you declare the generality of an effect (fun for tail-resumptive, ctl for control-effect). This remark was also pretty interesting.
