Pardon my ignorance, but how do you deal with asynchronous exceptions when you don’t have exceptions?
I know e.g. with Unix processes you can have signals and signal handlers. That’s just another color for the bikeshed, though. There’s always got to be some way to handle real, no-shit exceptions that break the IO abstraction barrier. If not exceptions as we currently have them, wouldn’t you still need some mechanism that would end up with a slightly different set of tradeoffs?
I think there’s room for both. Haskell lets you do both. Failures as return values is nice in some cases like parsers and whatnot. Failures as exceptions is nice when you’ve got a load of I/O based code that can fail in myriad ways and you don’t care to enumerate them nor would benefit in doing so.
At first I liked Rust’s angle until I saw people using it at work and saw that it’s actually an inconvenience: people sprinkle “anyhow” everywhere as a way to avoid having to produce a well typed error, and every function is littered with “?” on almost every line to the point of meaninglessness. Java has checked exceptions, and not everybody is too happy about them.
Haskell lets you be blasé like Erlang (throw and forget) or meticulous like Java/Rust, depending on your discretion. It’s not perfect but I feel lucky to have it.
MzScheme differentiated exceptions from termination of a thread by a custodian (Custodians) that couldn’t be stopped, IIRC. That was really neat. And Common Lisp folk use restarts (Beyond Exception Handling: Conditions and Restarts) all the time to provide a developer experience, which is another island of behavior quite far away from Haskell/Rust.
Pardon my ignorance, but how do you deal with asynchronous exceptions when you don’t have exceptions?
That’s the thing, Rust (and Go) only pretend they don’t have exceptions. Rust has panic and catch_unwind, Go has panic and recover.
I consider this pretense to be a massive flaw of these languages.
I agree with @chrisdone, sometimes you want unchecked exceptions, sometimes you want to track them in types. It generally depends on the use case and it’s nice that Haskell lets you do both. The problem with this is that it’s subtle and IME people don’t like this answer, they expect to be given a simple solution to a complex problem and both Rust and Go pretend they have it, but in practice it results in tons of noise in the code from manual passing of errors downstream everywhere (it’s a hot mess in Go in particular, at least Rust has some syntactic sugar for it).
Matt Parsons has a nice blog post describing the main pain point when no exception mechanism exists (or its use is verboten in a given code base): The Trouble with Typed Errors
To make typed errors work well (i.e. compose) you really need open variants. Unfortunately it’s a rare feature, and bringing it to haskell is hard.
My main gripe with exceptions that are not tracked in the type is that they make it more complicated to include linear logic features. If you have a file handle or channel that needs to be closed, or memory that needs to be freed, then we want to guarantee that this happens in every code path. And the possibility of untracked exceptions makes this more difficult. This is a problem for both Haskell and Rust. Nikos describes the problem for Rust in Must move types · baby steps and Arnaud for Linear Haskell here: On linear types and exceptions
I think this is a misconception. Effect systems can compose exception types without open variants by (something isomorphic to) passing them in as arguments. For example, to get the “sum” of errors Foo and Bar you can use in Bluefin
(e1 :> es, e2 :> es) =>
Exception Foo e1 ->
Exception Bar e2 ->
Eff es r
or in effectful
(Error Foo :> es, Error Bar :> es) =>
Eff es r
This is perfectly composable, no new type system features necessary.
This is independent of whether they’re tracked in the type, isn’t it? For example, you can consider IO as ExceptT SomeException UIO, where UIO is a monad that doesn’t throw exceptions. I think the problem is having any throw operation where you can write
do
r <- acquire
throw MyException
release r
and abort the execution of the block before release. This is so regardless of whether the do block is running in IO, ExceptT MyException SomeOtherMonad, or anything else.
Tbh I have yet to try that out in earnest. I recall using a similar feature in the past that also relied on constraints (I think MonadError + classy prisms). But I found it difficult to use at the time.
Your example looks intriguing, thanks!
We probably mean the same thing, I was just too concise in my comment 
I am not too worried about a throw operation that just crashes the program if some invariant has been broken, but only about throw operations that can be handled, since only these introduce a new control flow mechanism that can break linear logic reasoning. Through your work on bluefin I think you probably agree that exceptions should be handled lexically (i.e. the handler responsible for catching the exception should be determined by lexical scope, not dynamic scope), so a sensible throw operation needs to also be passed a capability, and this capability/continuation must be tracked in the type system, which makes it possible again to use linear logic reasoning.
there are a ton of open variants libraries one of them is vary sure i guess it isn’t as nice as if it were a language feature but it certainly works.
Indeed, I am also aware of variant (ghcup uses it, for what it’s worth). I have always balked at the (perceived?) complexity, however.
Async exceptions in particular are why Haskell is better than Rust or Go for concurrency. It just has a better concurrent RTS with fewer footguns.
And as others have said, Rust doesn’t ensure code doesn’t unsafeExplode
As it so happened, someone recently expressed a similar interest for I/O:
But in the context of Haskell, what exactly is “idiomatic code” ?
effect-free expressions? Haskell is nonstrict, which is why it’s so nice to program in. Hence the lack of those effects (unless something unsafe... is being used)-;
the absence of effect-centric actions (functorial, applicative, monadic, arrow, comonadic et al )? Alright, just provide some other way to manage exceptions or other effects in Haskell (and remember: even effect systems rely on one or more of those interfaces - usually the monadic one).
Otherwise, perhaps this could be of interest:
(with abstract monadic I/O first appearing officially in Haskell 1.3).
Instead of IO a, a program would have the type:
type Dialogue = [Response] -> [Request]
…it would be one big effect-free expression, with all that imperative ugliness confined to the interpreter (which does use abstract monadic I/O). But since Haskell 2010 also provides an FFI:
foreign import ccall runDialogue :: Dialogue -> IO ()
(if the in-Haskell interpeter is too slow ;-)
This is very interesting, because variant is using an analogous encoding to effectful anyway. For example, see the definition of V
V :: c :< cs => c -> V cs
and note the resemblance to the effectful type signature I gave. If you use variant for exceptions then you start with separate constructor types c satisfying c :< cs, wrap them up in a V cs, and then later unwrap them to handle them. But if you’re using effectful then you may as well keep them all separate as Error c :> es constraints and avoid the middleman of wrapping and unwrapping!
The author fails to convince me that there is some principle involved. In the last paragraph, he even mentions how to deal with checked exceptions, which brings me to this:
The Trouble with Checked Exceptions
There are a few points here, but the main is, IMO, that people just don’t care to handle all of those exceptions. They either don’t care because they have some exception handler in place already (provided by a web framework, for example) or they just want to stay on the happy path and build that useful functionality. They will circumvent checked exceptions anyhow, and it is only trouble for them that they have to do that.
Whenever Go folks call if err != nil exception handling, I’m in disbelief. Just a quick search on GitHub, they either do panic(err) or return nil, err or myLogger.Fatal(err). I’m sure there are examples of actual exception handling, but most aren’t. The three above are just exceptions with extra steps, code that could be added by the Go compiler. I just don’t see the benefits.
Now Rust might be different due to its goals (close to metal/exceptions don’t mix?), but a quick look at Rust book and the first example of exception handling is this.
fn main() {
let greeting_file_result = File::open("hello.txt");
let greeting_file = match greeting_file_result {
Ok(file) => file,
Err(error) => panic!("Problem opening the file: {error:?}"),
};
}
To be fair, this is what I would do in Haskell if open returned Either.
That being said, I really like checked exceptions, if I want to force myself to do something consistently. Forcing others just doesn’t work that well.
Hmm, I’m not sure it makes it possible again to use linear logic reasoning. Even if we use Bluefin, say, where an exception can only be thrown if there’s a suitable capability in scope, and even if we completely avoid imprecise exceptions (i.e. from pure code), I still don’t see we can use linear logic reasoning. We can still write
\ex -> do
r <- acquire
throw ex MyException
release r
and lose access to r, so we can’t release it. Nonetheless, we could bracket the ability to acquire r, and put some bounds on the lifetime of r, but it still doesn’t seem like linear logic reasoning to me. Maybe I’m misunderstanding you though.
Since it’s already been mentioned three times…in section 3.3 of How to Declare an Imperative (Interaction by linear logic, pages 21-24 of 33), Philip Wadler provides an example based on uniqueness types rather than just linear parameters. This is an interesting choice, given that Wadler’s previous literature (for example, Linear types can change the world!) advocated the use of linear parameters.
But in this topic, the term “linear logic” has only been associated with linear parameters (presumably because only those are provided by Glasgow Haskell). So could it be this specialisation of linear logic (rather than linear logic itself) which is at fault, with regards to breakage of reasoning?
I think this is what David wants to prevent when he writes
I would think that you need to associate “cleanup handlers” with ex for every linear resource that is in scope at a use site of ex. Such a cleanup handler would consume the particular resource upon unwinding, triggered by a call throw ex.
It seems quite complicated to support this (i.e., “ensure that every use of ex comes with a cleanup handler of linear resources”) in the type system.
Perhaps a finally or bracket-like combinator could avoid this reasoning, but how do we ensure that this combinator affects all exception effects in the Eff stack?
(I suppose this has been discussed in the effect systems research community before, which is why I’ll defer to David here :).)
I think the main problem with the reasoning of tracking exceptions at the type level is that they break encapsulation when working with higher order functions (the bread-and-butter of FP): If I have a function that requires an operation that provides the current time, how do I handle different implementations that might or not fail? Knowing precisely how it might fail requires the consumer to be coupled to a specific implementation so the usual approach is to say “this operation might fail”, yet this is not very helpful since everything could technically fail. At the end you end up with something like go’s error, something opaque that at best you can print.
I would have thought something like Throws e m does that - for example:
{- Exception e => Throws e IO -}
data TimeFailure = ... -- or a newtype
instance Exception TimeFailure
How to make that work in an effects system is left as an exercise…