Date: Tue, 7 Sep 1999 12:23:21 +0200 (MET DST)
From: Alain Frisch <frisch@clipper.ens.fr>
To: David Monniaux <David.Monniaux@ens.fr>
Subject: Re: throws
In-Reply-To: <Pine.GSO.4.03.9909061924050.9516-100000@basilic.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
This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:25 MET