Opened uncancelable region to the right #1800
Conversation
laws/shared/src/main/scala/cats/effect/laws/MonadCancelLaws.scala
Outdated
Show resolved
Hide resolved
| * to be a bit off. | ||
| */ | ||
| def onCancelAssociatesOverUncancelableBoundary[A](fa: F[A], fin: F[Unit]) = | ||
| F.uncancelable(_ => F.onCancel(fa, fin)) <-> F.onCancel(F.uncancelable(_ => fa), fin) |
There was a problem hiding this comment.
does this hold?
uncancelable(poll => fa(poll).onCancel(fin)) <-> uncancelable(poll => fa(poll)).onCancel(fin)
There was a problem hiding this comment.
Yes. If you see cancelation on the inside, you'll see it on the outside. If you don't see it on the inside, you won't see it on the outside.
There was a problem hiding this comment.
right, as expected. Worth documenting it in its full form then, somewhere.
There was a problem hiding this comment.
I want to do a full deep-dive discussion in the docs about cancelation in general
|
Did the following not hold in the current encoding? Particularly thinking about when uncancelable(_ => fa.onCancel(fin)) <-> uncancelable(_ => fa).onCancel(fin)Also does this mean the laws are violated in the other direction as well? uncancelable(_ => fa).onCancel(fin).map(identity) <-/-> uncancelable(_ => fa).onCancel(fin) |
I think external cancelation is still a bit of a blind spot. To answer your question though, that particular law would not have held prior to this PR. If
Actually, no! Those two sides are equivalent both before and after this PR. |
| @@ -88,16 +88,24 @@ trait GenSpawnLaws[F[_], E] extends MonadCancelLaws[F, E] with UniqueLaws[F] { | |||
| } | |||
|
|
|||
| def raceCanceledIdentityLeft[A](fa: F[A]) = | |||
| F.race(F.canceled, fa) <-> fa.map(_.asRight[Unit]) | |||
| F.race(F.canceled, fa.flatMap(F.pure(_)).handleErrorWith(F.raiseError(_))) <-> fa.map( | |||
There was a problem hiding this comment.
Moving surfacing of cancelation into the argument might make the intent of the laws clearer. Something like
final class CancelationSurfaced[F[_], A](fa: F[A]) // where the generator for CancellationSurfaced applies the flatMap -> handleError transformatiuon
def raceCanceledIdentifyLeft[A](fa: CancelationSurfaced[F, A]) = ...especially as the particular sequence used to ensure cancelation is visible isn't unique in that function.
Arguably, if you're reasoning over the laws then you're also likely aware of these cancelation semantics and why the "identity" is applied, so maybe it's a feature, but you have to learn to look through it anyhow to see the intent of the law.
The new type would also give a place to document the effect on the laws.
There was a problem hiding this comment.
Oh this is a really really good idea. It breaks bincompat so we have to do it now if we're going to do it.
| @@ -62,13 +65,6 @@ class IOSpec extends IOPlatformSpecification with Discipline with ScalaCheck wit | |||
| fa.flatMap(i => IO.pure(i)) must completeAs(42) | |||
| fa must completeAs(42) | |||
| } | |||
|
|
|||
| "preserve monad right identity on uncancelable" in ticked { implicit ticker => | |||
Fixes #1744
Requesting expedited reviews from @SystemFw, @wemrysi, @RaasAhsan, and @vasilmkd. Also anyone else who wants to pile on, please do so quickly. I would ideally like to get this merged today so we can release quickly.
This is a major semantic shift in several ways. Bottom line up front: this change violates the functor laws. If you're looking for a thing that Cats Effect is choosing to do in the name of "pragmatism over purity", this is it. We didn't take this decision lightly.
Just to provide a bit of context, consider the following construction:
uncancelable(_(uncancelable(fa) /* think carefully about this spot */))In the encoding which is present in the current HEAD, the commented location in the expression above represents a very small gap in which cancelation may be observed but not suppressed. This in turn means that
pollanduncancelabledon't compose safely, and this has some quite profound impacts on everything from Fs2 toResource. Ultimately, any function which wraps its contents inuncancelableand returns was actually unsafe because the caller couldn't close the gap.This PR changes
uncancelableto be an open region to the right. In other words, we no longer perform a cancelation check upon completion of the region. This is well exemplified by the new law:Which, transitively, also means the following:
How does this violate the functor laws? Well, imagine an identity
flatMap:uncancelable(_ => fa).flatMap(pure).onCancel(fin)(by the monad laws, this is equivalent to
.map(identity), which is why this is about the functor laws specifically)The above is not equivalent: the
onCancelwill sequence the finalizer iffais canceled. If you think about it, this is fundamentally necessary if we want to allow auto-cancelableflatMap, but it's also a violation of the functor laws because identity mappings must be identity.As it turns out, violating the functor laws has… some implications. Nearly all of this PR is just running through and trying to correct all of the problems which arise when you do something like that, though I did also fix a very subtle bug in
Resource#allocatedas well as implemented a more optimizedIO#guarantee, which should helpResourceperformance a bit.The hand-wavy justification here is that the violation of functor laws is only observable within confined runtime scopes. Like, for example, what we do in the tests. 😢 The requisite incantation to resurface the old semantics is as follows:
Obviously these two expressions should be equivalent, and if we ignore confined runtime scopes such as
unsafeRun, they are indistinguishable. However, the latter expression will guarantee that cancelation is detected iffawas indeed canceled, whereas in the former expression, iffais secretlyuncancelable(fa'), you aren't guaranteed to observe the cancelation.The one place where this gets really strange is
race, becauseraceactually represents a confined evaluation scope similar tounsafeRun. However,racealready violates a whole series of laws, which is why we exclude it from the generators, so uh… I guess it's fine?All in all, this should result in a semantic which is much safer and much more intuitive for users and the ecosystem, with the only serious casualty being our self-respect every time we have to look at what I did in this PR.