[bitc-dev] Accurate static typing vs. Dependent Types
Jonathan S. Shapiro
shap at eros-os.com
Mon Dec 8 10:15:32 CST 2008
On Mon, Dec 8, 2008 at 8:07 AM, Rodrigo Kumpera <kumpera at gmail.com> wrote:
> Declared exceptions in Java sucks because there is no language help to cope
> with proper capture and propagation.
Not so. I didn't do a good job describing the problem earlier, so let me try
again. There are several problems with declared exceptions.
First, note that exception propagation cannot be inferred reliably. If f()
calls g(), and g() potentially raises ExAwkward, and f() does not include a
catch block at all, it does not follow that f() can raise ExAwkward. This is
a dependent typing problem. See the other thread on that subject. So two
issues here: (1) inference of exception propagation is not straightforward,
and (2) in the absence of dependent typing, declared exceptions inevitably
forces the declaration of exceptions *that cannot actually be thrown*.
Next point: declared exceptions are unstable. The exceptions raised by a
library routine f() are partly a consequence of the functions that f()
calls. These can change, rendering the declarations obsolete, breaking code
in the field. In most cases, both the new and the old exceptions weren't
going to be caught anyway, so breaking linkage for this isn't worthwhile. In
some cases, if I am *prohibited* from introducing a new exception throw, I
can't fix a critical bug. Any feature that has the effect of suppressing
critical bug fixes in existing code better have a damned compelling
The rule in Java is that exception declarations must be exhaustive, but only
if they are present. In Java, the workaround for all of this rests in the
object hierarchy, and the common fix is to declare that a procedure throws
the Exception superclass, which serves as a catch-all.
Note that the existence of a catch-all eliminates the possibility of more
efficient compilation. This is an all or nothing sort of thing, and the
"all" position has been shown not to work out in the field. In BitC, the
position is that declarations are not required. We probably ought to *permit
* them for documentation purposes, but such a declaration would not be part
of the function's type.
Let me come back to the compilation issue in a separate note, but hopefully
this makes my view on declared exceptions clearer.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the bitc-dev