Algebraic effects

[Lysxia]

Since Bluefin.Eff is just IO, it's quite feasible to adopt the delimited continuations primops from GHC 9.6 (base 4.18) in bluefin and do all of the algebraic effect machinery on top.

Effects, now algebraic Delimited continuations are the main difference between "bluefin/effectful effects" and "algebraic effects". While bluefin is an effect system, its expressiveness without delimited continuations is basically limited to what you call Coroutine: all of the "effects" boil down to passing impure functions around (modulo some defunctionalization). Delimited continuations let you implement all of the existing effects and more from scratch, without any other form of impurity ("IO"):

• State without built-in IORef
• Exceptions without built-in throw/catch
• Nondeterminism, which is not present in IO
• Concurrency without built-in scheduler

(Some of these implementations can be found in my experimental repo.)

(You might actually not want to implement all of your effects that way, State using delimited continuations seems not very efficient, and the dynamism of native exceptions has its uses (even in this very PR). Nondeterminism and concurrency (including first-class coroutines/generators) remain as newly achievable items with these delimited continuations/algebraic effects, so that's exciting.)

To be tested; but it compiles (with GHC 9.8 at least), so it must work, as the saying goes:

• Delimited continuations primops Bluefin.DelCont
• Algebraic effects Bluefin.Algae (sticking with the oceanic theme)

Taking inspiration from OCaml, I implemented a further extension with cancellable continuations:

• Dynamic exceptions (that is, port Control.Exception to bluefin, without any of the existing static exception's scoping shenanigans) Bluefin.Exception.Dynamic
• Algebraic effects with cancellable continuations Bluefin.Algae.Cancellable

Cf the headers of those respective modules (not the internal ones) for details.

Would you like to include this in bluefin?

Possible reservations are that it's a lot of untested code, and that it requires GHC 9.6 (base 4.18; whereas the current bound allows base 4.12).

At a minimum, the dynamic exceptions module seems useful independently of the rest.

[tomjaguarpaw]

Very nice! This possibility is one of the things that prompted me to develop Bluefin in the first place. It was only later that I realised the effectuful strategy meant that I could obtain the same API without delimited continuations.

Would you like to include this in bluefin?

I would like to include this somewhere. Requiring GHC 9.6 makes this a non-starter for including in bluefin itself. Should we start a new package? We could just add a new package to this repo, alongside bluefin and bluefin-internal.

I'm curious though: is this really safe to mix with arbitrary IO? I haven't thought about it very hard, but perhaps there are restrictions on what sorts of other IO operations play safely with delimited continuations. Could exceptions interact badly with them, for example?

By the way, I love the name!

[Lysxia]

Sounds good. I'll go make a bluefin-algae then.

I'm curious though: is this really safe to mix with arbitrary IO?

Yeah there could be more sharp edges beyond those I've documented here. I am hoping that single-shot continuations close most remaining holes. At least OCaml decided they're fine with that.

For example, I just realized that multishot continuations let you observe the difference between the current IORef-based State and an algebraic-effect-based State. The continuation must start under a runState and ends outside it: the idea is that you then "end" runState twice to see if something spooky happens. With IORef you will see the same IORef in the second run, so state changes persist across multiple resumptions, whereas a truly pure State would "backtrack" the state to its value just before the call.

[tomjaguarpaw]

That sounds annoying but worth it for an experiment. Are we at least confident that there are no segfaults? I seem to recall the delimited continuations design ruling out segfaults, but I am not certain.

[Lysxia]

Yes the PromptTag# design guarantees type safety (and I don't do any unsafeCoerce). The only thing that could go wrong is a shift0 (control0#) without a reset (prompt#), which an effect system can then prevent.

[Lysxia]

Closing this in favor of a separate library, due to the GHC 9.6 requirement and the extra safety precautions needed to mess with continuations.

[Lysxia]

Would you consider adding just the dynamic exceptions feature instead? That still seems useful for interfacing with IO primitives.

[tomjaguarpaw]

Yes, I agree we need bracket. It doesn't require GHC 9.6 right? And in fact doesn't involve delimited continuations at all?

Can we just add it as a feature of Bluefin.Exception?

[tomjaguarpaw]

Can we just add it as a feature of Bluefin.Exception?

Actually, maybe that doesn't make sense ...

I'll let you explain what exactly you're thinking of.

[Lysxia]

Indeed that doesn't depend on delimited continuations.

The selling pitch is that since IOE lets us call arbitrary IO functions, we should be able to handle their exceptions as well.

Adding this stuff to Bluefin.Exception would be conceivable too. I preferred a different module because in my mind these two kinds of exceptions are quite different (so you would usually only import one) and it is a shame to give up the existing names from base to the other kind. But I don't feel strongly about it.

[tomjaguarpaw]

I think I just don't understand DynExn. What is its purpose beyond what Exception already provides?

[Lysxia]

DynExn is the capability to throw and catch dynamic exceptions, so that one can write error-handling code without needing the capability to launch missiles. (And in this PR I would say that applies to bracket (as it is implemented using catch) and discontinue.)

As I see it, this is a minimal wrapper around GHC's existing exception subsystem in bluefin. I didn't feel a need to change the existing API beyond creating a dedicated capability for it.

[tomjaguarpaw]

By "dynamic exceptions" do you mean Haskell native exceptions that are normally caught in IO? If so then I don't understand why one would want those if you are already using Bluefin and have access to scoped exceptions. Am I missing a use case?

I think I'll add a bluefin-contrib package for people to place things that they think are useful but that I don't understand or see the utility of. I'd be happy to put DyxExn there. But if you think I'm missing something important then please continue trying to persuade me of the value of DynExn.

I agree that Bluefin needs bracket though.

[tomjaguarpaw]

For example, couldn't we leave the DynExn out of onException? Isn't this good enough?

onException :: ex :> es => Eff es a -> Eff es () -> Eff es a

I don't understand why we should need DynExn to have Bracket.

[Lysxia]

If so then I don't understand why one would want those if you are already using Bluefin and have access to scoped exceptions.

If I call openFile and I want to catch its exceptions I can't do that with Bluefin.Exception because it only catches Bluefin.Internal.MyException which wrap around arbitrary user-provided values.

I could catch the exception before wrapping it in effIO, but that only works for individual calls. If I am making many effIO calls interspersed interspersed with other effects, then the catch should live in Eff.

[tomjaguarpaw]

I can see that DynExn is a restricted form of IOE that only allows you to deal with exceptions. That seems fine. I'm not convinced it's worth adding for that purpose, because anything that requires IO (like openFile) will require IOE anyway, and anything that doesn't can use a scoped exception.

But that aside, I don't understand why bracket (and onException, etc.) is done in terms of DynExn. It seems like it should work fine without that parameter. Am I missing something?

[tomjaguarpaw]

Maybe this is another way of putting the first part:

Can you give an example of using DynExn, where IOE is too much, and Bluefin.Exception is too little?

For the second part:

Can you give an example of using onException :: ex :> es => Eff es a -> Eff es () -> Eff es a (i.e. without DynExn) that goes wrong (because of the lack of DynExn)?

[Lysxia]

Can you give an example of using onException :: ex :> es => Eff es a -> Eff es () -> Eff es a (i.e. without DynExn) that goes wrong (because of the lack of DynExn)?

catch and derived exception handlers requiring a capability maintains the free theorem that any function f :: forall es. Eff es () -> Eff es () can only be replicate n for some n. This property would be lost if you could write join onException :: Eff es () -> Eff es () for example.

Can you give an example of using DynExn, where IOE is too much, and Bluefin.Exception is too little?

Bluefin.Exception is too little

You can't catch FileDoesNotExist from openFile using Bluefin.Exception.

Imagine logging IO exceptions using DynExn and some Log capability. I think you can write a lot of error handling code like this, with just catch and throw, without knowing anything about the specific IO that the handled computation is doing.

-- | log exceptions thrown by the third argument and re-throw them
logException :: (log :> es, ex :> es) => Log log -> DynExn ex -> Eff es a -> Eff es a

Another example is evaluate to catch exceptions from a pure value. That does not do any actual "IO" (talking to the OS). Does this look like a reasonable type:

evaluate :: (ex :> es) => DynExn ex -> a -> Eff es a

[tomjaguarpaw]

You can't catch FileDoesNotExist from openFile using Bluefin.Exception

Sure, I agree Bluefin.Exception is too little there, but I don't agree that IOE is too much, because you have to have IOE to run openFile.

Imagine logging IO exceptions using DynExn and some Log capability

But again, either the Eff es a argument uses only scoped exceptions, in which can you don't need DynExn, or it uses IOE, in which case you don't need DynExn.

Another example is evaluate to catch exceptions from a pure value

This seems more plausible, but wouldn't it be better as

evaluate :: e :> es => Exception SomeException e -> a -> Eff es a

[Lysxia]

evaluate :: e :> es => Exception SomeException e -> a -> Eff es a

I'm starting to see how you would imagine handling IO exceptions with scoped exceptions. If we wanted to account for all IO actions potentially throwing exceptions, we could add an exception handle to effIO

effIO :: (io :> es, e :> es) => IOE io -> Exception SomeException e -> IO a -> Eff es a

which would catch any exception in IO natively before passing it to the bluefin Exception SomeException handler.

Now I'm wondering how to intercept scoped exceptions like bracket does, or for logging purposes. I see one "principled" way and one "magical" way.

The "principled" way would be to syntactically intercept the handle. bracket would have the following type, where the handled argument gets a fresh exception handle into bracket, and the old exception handle is used in bracket to re-throw the exception.

bracket :: ex :> es =>
  Exception e ex ->
  Eff es a ->  -- ^ acquire
  (a -> Eff es ()) ->  -- ^ release
  (forall ex'. Exception e ex' -> a -> Eff (ex' :& es) b) ->
  (Eff es b)

IMO this is not so great because it only intercepts one exception handle. If there are n exception handles in scope, then you'd need n calls to bracket or some construct to merge exception handles into one. And it's not easy to be sure you've got them all. For example if you're using a higher-order function:

let f = ... in
(\exn -> f (throw exn E)) `catch` handler

A bracket in the definition of f cannot ever hope to intercept this throw exn E because it doesn't have the exn handle.

Another solution is to use the fact that bluefin exceptions go through native exceptions, so the bracket from base can see them. So Bluefin.bracket = coerce Control.Exception.bracket.

It's magical, it breaks the illusion of exceptions being scoped (somewhat), but I guess it does its job. This magic can't actually look at the exception, specifically the value that was thrown by the user, because its type is unknown at that point. So it enables bracket but not logging (which might or might not be desirable).

My initial thought was to let scoped exceptions be scoped, which forbids using magic. So the "principled" solution above is the only possible one, and IMO an inherent weakness of scoped exceptions. That's why I proposed to add dynamic exceptions, which naturally allow bracket.

All things considered, the "magical" bracket might still be acceptable because it seems to only slightly break the abstraction of scoped exceptions.

Does that seem like a reasonable summary?

[tomjaguarpaw]

Does that seem like a reasonable summary?

Yes, I think so. In practice I suspect the "magical" version is good enough.

[tomjaguarpaw]

At some point I'll make a bluefin-contrib package and you can put anything you like into it.

[tomjaguarpaw]

This magic can't actually look at the exception, specifically the value that was thrown by the user, because its type is unknown at that point. So it enables bracket but not logging (which might or might not be desirable).

Exception has Show as a super class, so it can log, but I wouldn't say that's desirable :(