throws

throws

[David Monniaux]

[resume: suggestion d'implementer une analyse statique et sommaire de
detection de fuites potentielles d'exceptions semblable a celle de Java]

The Java language has a nice feature: static detection of exception
leaks (or, more exactly, a conservative and simple approximation of it,
since the full problem is of course undecidable).
That is, functions must declare the exceptions they can throw
(except those generated by the runtime system); exceptions that can be
thrown from function f are inferred by looking at those that can be thrown
by the functions called from f, those that are explicitely thrown in f and
those that are caught in f.

Pardon me if I'm mistaken, but this sounds easy and cheap to implement.
Could it be possible to add a construct like this:

throws
<list of throwable exceptions>
in <expression> ?

Only terms tagged such as above would be checked so as to allow upwards
compatibility.

Does this sound nifty? And implementable?

---
David Monniaux     Tel: +33 1 44 32 20 66    Fax: +33 1 44 32 20 80 
Laboratoire d'informatique de l'École Normale Supérieure,
45 rue d'Ulm - 75230 PARIS cedex 5 - FRANCE

Re: throws

[Alain Frisch]

Hi David,

On Mon, 6 Sep 1999, you wrote:

> The Java language has a nice feature: static detection of exception
> leaks (or, more exactly, a conservative and simple approximation of it,
> since the full problem is of course undecidable).
> That is, functions must declare the exceptions they can throw
> (except those generated by the runtime system); exceptions that can be
> thrown from function f are inferred by looking at those that can be thrown
> by the functions called from f, those that are explicitely thrown in f and
> those that are caught in f.

If I understand what you mean, I think that it would be necessary to
annotate functionnal type expressions with throwable exceptions.

For instance :

let eval f x =
 throws Not_found
 in
  f x;;

would have type 
(('a -> 'b; [Not_found]) -> 'a ->'b) [Not_found]

meaning that f is a function that can only throw Not_found.

I think that the consequences of this annotation would be quite
important on the type system and type inference algorithm.

--
Alain Frisch

Re: throws

[Markus Mottl]

[snip]
> The Java language has a nice feature: static detection of exception
> leaks (or, more exactly, a conservative and simple approximation of it,
> since the full problem is of course undecidable).
> That is, functions must declare the exceptions they can throw
> (except those generated by the runtime system); exceptions that can be
> thrown from function f are inferred by looking at those that can be
> thrown
> by the functions called from f, those that are explicitely thrown in f
> and
> those that are caught in f.
[snip]

This problem very closely resembles the one I once mentioned about
declaration/inference of purity (side-effect-free functions):

Tagging system- and interfaced C-functions as pure/impure would allow the
compiler to infer purity (conservatively since otherwise also undecidable)
for any function. This would allow some very interesting optimizations,
which would free the programmer from the task of thinking about *when*
to evaluate a function (if it is a pure one).

Debugging would become easier, too: pure functions never depend on the
state of the system so they can be debugged without any consideration
of the rest of the code.

Are there further (still missing?) features besides detection of exception
leaks and purity that could be statically analyzed in a similar way?

Regards,
Markus Mottl

-- 
Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl