The status of eio and effects composition

Community
,
10

As mentioned in my last post, it’s true that I have only considered effects that immediately resume so far (or at least that resume unconditionally without introducing interdependencies). Having these would already be a great. Regarding effects with more complex resume conditions, it’s clearly a dangerous game and you might introduce deadlocks, but at some point GIGO, you get what you asked for.

I was really puzzled about why this would be “nonsensical”, but I think the quiproquo might be this : I am not expecting any forked fiber to magically inherit exception or effects handler, as indeed I don’t even see how to properly specify this. I am only thinking of structured concurrency. If some scheduling API call runs a fiber independently in the background, or in a worker pool, etc, in other words detached from the current flow, indeed expecting any handler to be preserved is foolish. But when the scheduler structures the execution flows, it looks pretty well defined to me and very desirable. I think it’s not even exclusive to effects, anything relying on the execution stacks exhibits the same semantics.

Consider:

(* No effects *)
Sql.with_transaction @@ fun transaction ->
  sql_stuff_1 transaction;
  sql_stuff_2 transaction

I notice that stuff 1 and 2 are independent and can be run in parallel. Being a good developer and using Eio, I parallelize it :

Sql.with_transaction @@ fun transaction ->
  Eio.Fiber.both
    (fun () -> sql_stuff_1 transaction)
    (fun () -> sql_stuff_2 transaction)

Surely, this is well defined and legitimate? One is not going to argue that one of the fibers could be detached or outlive its parent, and use a defunct SQL transaction, I think. Even in the case of exceptions, the greatness of structured concurrency guarantees that both fibers will be finished or canceled before we exit with_transaction.

But this only works because of Fiber.both; if one completely detach an execution thread, à la Lwt.dont_wait, nothing is guaranteed. I’m not sure there’s such a feature in Eio, but imagining Eio.detach exists:

Sql.with_transaction @@ fun transaction ->
  Eio.detach (fun () -> sql_stuff_1 transaction);
  sql_stuff_2 transaction

Clearly, this will not work, as stuff_1 captured the transaction and might use it after it’s been committed / rolled back. I don’t think anyone would expect these to magically work.

In short, it’s really the structured nature of Fiber.both, Fiber.all, … that ensure this works.

What I strive is for this to be true for effects too. Imagine that Sql.with_transaction is implemented via effects (not a good idea and a clear overuse of them, but bare with me for the sake of the example).

(* Same with effects *)
Sql.with_transaction @@ fun () ->
  Eio.Fiber.both
    (fun () -> sql_stuff_1 ())
    (fun () -> sql_stuff_2 ())

I think it’s very easy to make the parallel with the effect-less version, and that the same argument applies : I can’t see why one would argue that one of the fibers may outlive the with_transaction, and consequently this seems very well define semantically to me. Likewise, I don’t suppose Fiber.both will run the subfiber in a different domain without telling me (otherwise I have much more pressing problems :sweat_smile: ), so we don’t have the “separate thread” issue. Starting a fiber in a different domain is, AFAIK, an explicit instruction, and one we cannot expect to preserve effects.

Regarding not resuming the continuation immediately, you’re “just” going to stale Fiber.both until you resume. If you create a deadlock doing so, it’s on you, you’re playing a dangerous game scheduling things behind the scheduler’s back. I also have trouble buying this point since one of the two fibers (the second, interestingly) is run directly from the current stack, and in that one you do have all the effect handlers installed, so in practice you call already perfecly do that.

Again, maybe I missed a crucial step that makes it technically impossible even in the very specific cases I’m talking about, but I’m failing to convince myself of this so far.

In short, to address @polytypic point :

the reason I don’t see this would work is that you are trying to solve a toy version of the problem

I think you’re correct, I’m only trying to have a very well defined subset of this to work, but it’s no toy to me, it’s the part I’m interested in. Maybe the issue is that I badly defined the scope of what I’m trying to achieve.

Or put more cheekily, well maybe but it’s MY toy and I like it :slight_smile:

3 Likes