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
1 Like
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 somethingunsafe...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 ;-)
1 Like
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.
3 Likes
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 :).)
1 Like
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.
1 Like
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…