Rewrite PureIO on top of coop

[djspiewak]

Mega-change of doom! This PR does a couple of things:

• Adds an implementation of @SystemFw's mask/poll combinator (called uncancelable for now) as described in Cats Effect 3.0 Interruption Model Proposal #681
  • Random note: I chose to keep bracketCase primitive, despite the slight overlap with uncancelable. This is mostly because of inversion of control between Bracket and Concurrent. There is no way (that I'm aware of) to define bracketCase in Bracket in terms of onCase and guarantee without making it aware of cancelability. And if we don't make it aware of cancelability, then we can define it, but we would need to override it in every Concurrent with Bracket implementation, which seems very annoying. So instead I made bracketCase primitive while guarantee and onCase are derived from it, and we'll have a law which codifies the relationship between uncancelable and the bracket.
• Pushes F[A] into the Completed case of ExitCase. This has the interesting side-effect of making ExitCase kind of behave like a monad transformer, but only when F forms a Traverse. When it doesn't form a Traverse, ExitCase is only Applicative! Fixes CE3: ExitCase.Completed #643
• Rewrite PureIO as PureConc (names are hard) on top of https://github.com/djspiewak/coop Eventually, if this works, I'll move coop under the Typelevel org

The last point is an important one. PureConc is now the following:

type PureConc[E, A] =
  Kleisli[                    // 1.
    ThreadT[                  // 2.
      Kleisli[                // 3.
        ExitCase[Id, E, ?],   // 4.
        FiberCtx[E],
        ?],
      ?],
    MVar.Universe,
    A]

The type seems imposing but it's actually relatively easy to deconstruct. Taking it one stage at a time:

1. The ability to use MVar from coop
2. Cooperative multithreading implemented with FreeT
3. A lexically-scoped context for the currently running fiber
4. Final results produced by an effect

The nesting is actually somewhat arbitrary: we could have put ThreadT on the outside, and even merged the two Kleislis together into one if we wanted to.

Laws are currently not passing, presumably because of bugs. I'm working on that, and in the process working on making ThreadT structures a bit more introspectable for debugging purposes, but this is good enough to get some review eyes on it. Also getting it into the upstream branch allows everyone else to pitch in and help out!

[djspiewak]

@SystemFw @LukaJCB Any thoughts on this? (singling you out since you self-assigned the reviews 😄; I'd love feedback on this from absolutely anyone who is interested in giving it) I ask because I'm getting close to a follow-up change which would supersede this PR which has working laws and things.

[SystemFw]

I'm going to just offer two high level thoughts for lack of more time:

• let's merge the kleislis if possible. I don't know this isn't a big deal semantically but the whole purpose of this model is simplicity

Random note: I chose to keep bracketCase primitive, despite the slight overlap with uncancelable.

This is an interesting point, I can't make up my mind but it really irks me that bracketCase is primitive, it's a very hefty primitive if you think about it (in terms of the assumptions it makes about cancelation of acquire, for example), and I can tell you for a fact that in the real IO has caused quite a lot of issue when using eq reasoning to simplify some code to analyse buggy behaviour.
Basically the point is that substituting onCancel/guarantee with their definitions in terms of bracket makes the code harder to understand.

[LukaJCB]

I really like this 👍

[LukaJCB]

Maybe this should be by-name?

[djspiewak]

pure isn't. The idea here is basically that you're inserting a cancelation if not masked. fallback is what you get if you are masked. So it's exactly the same as the following (if we could push the .start et al outside whatever context we're in):

pure(fallback).start.flatMap(_.cancel)

…with the guarantee that the cancel hits the bind either immediately before or after the pure. Making the argument by-name would mean that canceled is more analogous to delay, with the tighter bound that the cancel is checked before it runs. That seems like unnecessary added complexity.

[LukaJCB]

I understand your sentiment, but I'm not really sure it has to be analogous to delay which is an FFI entry point and has totally different semantics. In this case it'd be simply about evaluation, staying as lazy as possible.

[djspiewak]

Cats very consistently avoids these kinds of things though in favor of Eval, except when almost straight-up mandatory (e.g. ifM). It also breaks the pure-related laws, since pure itself is eager. If you can show me a compelling example, I'm open to being convinced (a la ifM). :-) Absent a really compelling rationale for laziness here though, I'm strongly leaning towards keeping it eager, at the very least to maintain equivalence with pure.

[djspiewak]

@SystemFw

let's merge the kleislis if possible. I don't know this isn't a big deal semantically but the whole purpose of this model is simplicity

The main reason I didn't is because I basically need to prism around and interpret them independently. The inner Kleisli gets interpreted before anything happens, and then has to get re-instantiated a few times later on (in results) due to the recursion in the types. The outer Kleisli is interpreted exactly once, in a relatively straightforward fashion. Additionally, there is no mechanism to materialize an ApplicativeAsk for some type which has a prism projecting it within some other type.

So it would just create a ton of boilerplate throughout the implementation, and would definitely be somewhat tricky in the interpreter due to the split instantiations. Not at all impossible, but is that better than simply having it in two distinct layers?

To be clear here, the Kleisli of MVar.Universe is really just an implementation detail of MVar, which is in coop itself. It's not at all an interesting component of the type, beyond the fact that it means that we can use MVar. The inner Kleisli is what actually carries meaningful contexts. So in a sense, keeping them split apart is actually semantically cleaner, since anyone reading the types can effectively ignore the outer Kleisli.

[SystemFw]

I think I'm convinced yeah

[djspiewak]

Splitting this out…

This is an interesting point, I can't make up my mind but it really irks me that bracketCase is primitive, it's a very hefty primitive if you think about it (in terms of the assumptions it makes about cancelation of acquire, for example), and I can tell you for a fact that in the real IO has caused quite a lot of issue when using eq reasoning to simplify some code to analyse buggy behaviour.

Basically the point is that substituting onCancel/guarantee with their definitions in terms of bracket makes the code harder to understand.

I agree that the code becomes harder to understand in this case, but I literally just can't get past the fact that bracket cannot be validly defined in terms of other primitives until you get to Concurrent. If we want to say that bracket is not primitive (which, for any Concurrent, it certainly doesn't need to be), then Bracket as a typeclass can no longer exist.

As an example, think about trying to write laws for Bracket, assuming it's just guarantee and onCancel, without having a Concurrent. You really can't. For starters, onCancel doesn't really have meaning at all. You could work with the slightly more general onCase, but even still it's awkward. guarantee becomes entirely lawless. You can only define this stuff in Concurrent.

Once you get down into Concurrent, of course, many things become relatively easy, but if Bracket is going to be a separate typeclass, then it needs to have meaning unto itself. The problem I have with eliminating it as a separate thing is that we almost immediately run into issues with Region, and it becomes unclear if we can even meaningfully define that class. Losing Region would in turn mean that we cannot generalize the hierarchy to the class of dynamic monadic regions, which would be frustrating. Like, I don't think that's a dealbreaker, but it's a pretty serious consequence for something as simple as "bracket is primitive".

In Functor, map is defined to be primitive. Once you get to Applicative, though, map is redefined in terms of pure and ap and further restricted with a new set of laws. I don't think bracket is really any different in this case.

Note that the code complexity issues shouldn't affect IO, since IO is perfectly free to… not define bracket to be primitive. bracket is primitive in the calculus, but not necessarily in the implementations. In fact, I'm strongly tempted to revise bracket in PureConc to be defined solely in terms of uncancelable and onCase, and then reimplement onCase to manipulate the finalizer stack.

[SystemFw]

Your considerations on the hierarchy are why I'm torn yeah
I think the problem with IO is that actually they are both defined independently.
I think I could settle with your proposal of changing it in pureConc. Like, it still irks me, but the considerations on the hierarchy are strong

[djspiewak]

I think the problem with IO is that actually they are both defined independently.

Agreed. And I think that's a smell unless it's being done for performance reasons. (and even then, I'm tempted to say "don't", since bracket is hardly something that happens as frequently as other combinators, like flatMap)

I think I could settle with your proposal of changing it in pureConc. Like, it still irks me, but the considerations on the hierarchy are strong

I'll change it in PureConc. I think there's no reason it should have bracket as its own thing.

[ChristopherDavenport]

Based on the above, am I appropriately understanding that perhaps Bracket being merged with Concurrent may be appropriate?

[djspiewak]

Based on the above, am I appropriately understanding that perhaps Bracket being merged with Concurrent may be appropriate?

If we did that, then bracket could cease to be a primitive, but then we would also lose the ability to abstract over dynamic monadic regions. Basically we would put ourselves back into the same boat as CE2, where Resource and Stream are these weird things that can't be Sync or Concurrent or anything.