Re: throws

[Alain Frisch <frisch@clipper.ens.fr>]

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