Extra Sync[F] laws for map and flatMap

[edmundnoble]

SyncLaws[F] have nothing to say about the result of throwing an exception from within a function passed to map or flatMap being equivalent to the result of using raiseError. To my mind this is one of the biggest practical differences between Sync and MonadError, because MonadError is incapable of offering this as a law (despite the instances for Try and Future doing so).

I think this is necessary because all of the exception-centered mechanisms in cats-effect being fully-specified greatly decreases the chance of unsound usage and relying by accident on properties which are not necessarily shared in common by all Sync instances; I also think it's more consistent, seeing as behavior like F.delay(throw e) <-> F.raiseError(e) is defined as a law.

[alexandru]

I'm 👍 on map and flatMap catching exceptions.

Exceptions are the result of side effects and even though we expect people to pass pure functions in map and flatMap, users will expect for Sync types to suspend exceptions.

Thus this is also a problem of usability. Instead of having only one mechanism for dealing with exceptions (e.g. attempt and handleWith from MonadError), for code abstracting over Sync users will also have to do try/catch blocks, just in case.

Actually these laws really have to be available for Async as it becomes a huge safety issue if the behavior isn't defined for exceptions thrown for asynchronous computations, since they can be thrown on some thread somewhere with no way left for the user to catch them at all.

[djspiewak]

While in principle I agree with this idea (especially for Async, rather than just Sync), in practice I think it would actually be strictly less useful than the current formulation. The reason for this is it would eliminate literally all of the auto-derived inductive instances on common data types. We would no longer be able to get an Async for StateT[F, S, ?] given Async[F], for example, because we would have no way of ensuring that map and flatMap were imbued with exception-catching behavior. Similarly, the very-useful Sync[EitherT[Eval, Throwable, ?]] would be impossible to define.

So while I agree that leaving things undefined in terms of map/flatMap behavior is undesirable from an abstraction standpoint, adding it to the laws would rule out far more use-cases than it would "rule in", as it were.

[djspiewak]

I'm going to close this for now. Scalaz 8's IO does not catch exceptions in map/flatMap, and I think it's pretty important that it is at least possible to define lawful instances of the cats-effect typeclasses for that datatype.

I also think, upon long discussion with @jdegoes and others, that this is really one of those subjective design decisions that shouldn't be enforced. Specifically, cats-effect IO (and Monix Task) are taking the position that "innocent" exceptions (e.g. SOE) from within the call stack of IO should be caught and managed, to avoid potentially silently dropping async threads and/or leaving applications in an invalid state without feedback. I still believe this is the right decision. However, the tradeoff here is that we violate the applicative laws as a consequence. Note the following:

pure f <*> pure x = pure (f x)

Rewritten into a slightly more familiar style in Scala (using Monad rather than Applicative, since both apply for IO):

val left = for {
  a <- F.pure(f)
  b <- F.pure(x)
} yield a(b)

left <-> F.pure(f(x))

If we instantiate f to throw new Exception, then this law is violated when we instantiate into an expression of the form ioa.attempt.unsafeRunSync(): the left formulation will result in an IO which produces a Left when run, while the right formulation will immediately and eagerly throw the exception.

As a pedagogical note, these are the sorts of examples which motivate the oft-cited fact that throwing an exception is pure, but catching one is impure. You cannot see the violation of the applicative laws without attempt (since you would get an exception either case, just with a different trace).

At any rate, I'm not comfortable codifying behavior into a law which in turn conflicts with behavior codified into another law applied to the same abstraction. And for the same reason, I'm not comfortable telling people that the cats-effect semantic is objectively the one and correct way of doing things. It's still the right approach in my view, but I admit arguments to the contrary.

Thus, we will not be codifying this semantic in the laws.