Re: throws

From: Alain Frisch (frisch@clipper.ens.fr)
Date: Tue Sep 07 1999 - 12:23:21 MET DST


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