[bitc-dev] Accurate static typing vs. Dependent Types

[David-Sarah Hopwood]

Jonathan S. Shapiro wrote:
> The rule in Java is that exception declarations must be exhaustive, but only
> if they are present.

That's not correct. Exception declarations must always be exhaustive, except
that subclasses of Error and RuntimeException are implicitly throwable.

This doesn't really affect your conclusions, though.

> 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.

It's never feasible to compile under the assumption that exceptions are
not thrown, because many common primitive operations (e.g. array index,
referencing a field or method of a nullable variable, etc.) can implicitly
throw exceptions. Whether exceptions are declared has nothing to do with
this, AFAICS.

-- 
David-Sarah Hopwood