Given that exceptions are a logical and necessary hole in the type system, I was wondering if anybody has given serious thoughts to moving towards more formally handling them with !.
Using https://is.gd/4EC1Dk as an example and reference point, what if we went past that, and:
Treat any function that can panic but doesn’t return an error or result have it’s type signature implicitly change from -> Foo to -> Result<Foo,!>any Result<Foo,MyErr> types would have their Error types implicitly be converted to enum AnonMyErrWrapper { Die(!),Error}
Since ! is zero sized ad unhinhabitable, there would be zero cost to converting between the types, and implicit conversion could be added to make it backwards compatible.
The benefit, of course, being that exceptions are effectively lifted into the type system, and it would be possible to reason about them, perform static analysis on them, etc.
I realize that this would be …non-trivial from a community point of view, if not from a technical one.
Also, this probably overlaps with a possible future effects system.
So given that I know it would be far from easy, am curious if there are any theoretical reasons
if it would be a problem given a clean-slate set of libraries?
how bad would the gymnastics have to be to make it an evolutionary change given current starting conditions?
Note: Exceptions and panics aren't quite the same thing. Exceptions are typed and are generally used to return common errors. Panics are an untyped way to say "something went really wrong and I just want to bail".
Treat any function that can panic but doesn't return an error or result have it's type signature implicitly change from -> Foo to -> Result<Foo,!>any Result<Foo,MyErr> types would have their Error types implicitly be converted to enum AnonMyErrWrapper { Die(!),Error}
(Technical Digression 1) Errors and results aren't special in any way; they're just conventions. The compiler can't know if a function already returns an "error" because the compiler can't distinguish between an error and a normal return type (they look the same).
(Technical Digression 2) ! is just a type for things that cannot be "instantiated" (no value of that type can exist). The only relation to panic!() is that panic "returns" ! because panic!() never returns. This means that, logically, value(a) is (type(A) OR type(!)) reduces to value(a) is type(A). So, if you tried to statically analyse Result<Foo, !>, your static analysis program would just reduce it to Foo and you'd be back where you started.
The benefit, of course, being that exceptions are effectively lifted into the type system, and it would be possible to reason about them, perform static analysis on them, etc.
One usually can't (or doesn't want to) reason about panics. That's the entire point of having them; they're an escape hatch to let the programmer toss in the proverbial towel.
So, it looks like you want a way to statically prove constraints about your program. Instead of a runtime panic!(), you want a compile-time statically_unreachable!() (one could use ! as a value to indicate that some block of code is unreachable). Unfortunately, this is impossible to do in the general case (due to the halting problem) and hard to do even in limited cases. This is generally called certified programming and often requires the programmer to either write their programs in non turing complete languages or manually prove their programs correct. If you're interested in this subject, take a look at Coq.
But I think you miss the mark a little bit when you say that i’m looking for something like statically_unreachable!(). What I’m really trying to do is to be able to signal that it is impossible for a result to be covered exhaustively, even using a wild card, and therefore you can’t reasonably assume that any of the code paths in your match statement will be traversed.
That said, most of what you said still applies and is correct.
Yeah…I really shouldn’t have used “exception” in the title. I am not at all interested in actual “exception handling” here. Just static knowledge that the function can cause the thread to terminate (and yes, I do know that it’s theoretically impossible in the general case given vagaries of hardware and operating systems).
Ok, I think I got it. You want a way to figure out what can and can’t panic (for writing unsafe code?)? The current answer is: anything you didn’t write and most of what you did could panic ;). Technically, we use MIR’s control flow graph to mark functions that can panic (and mark everything that calls them) however, this gets a bit tricky:
What about generic functions? They may panic.
What about functions that make dynamic function calls. These would always have to be marked as being able to panic.
Anything that asserts anything can panic.
Any array indexing can panic.
Etc.
One could alleviate this situation by providing some form of #[never_panics] annotation for telling the compiler that function never panics even if it calls a function that can. Additionally, we could introduce two different ways to panic:
panic!() – programmer invariant violated (e.g., index out of bounds).
bug!() (or just use unreachable!()?) – something happened that shouldn’t be possible.
This would reduce the number of necessary #[never_panics] annotations.
Unfortunately, correctly annotating everything and converting all appropriate panic!() calls to bug!() calls would be very tedious and probably not worth it.
However, this is one of the beautiful things about the MIR control flow graph. You can write plugins (even out of tree) to statically determine what can and can’t panic, crash, etc. They just may not be very useful.
On the other hand, it might be useful to have some form of annotation (#[panics]) to indicate that a function is expected to panic on certain inputs. However, this would be purely for documentation purposes and probably isn’t any better than just documenting the behavior in the method description (although it may help tools/syntax highlighters highlight things that are expected to panic in certain cases).
