From mboxrd@z Thu Jan  1 00:00:00 1970
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id NAA26030 for caml-redistribution; Tue, 7 Sep 1999 13:33:31 +0200 (MET DST)
Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id MAA20323 for <caml-list@pauillac.inria.fr>; Tue, 7 Sep 1999 12:23:25 +0200 (MET DST)
Received: from nef.ens.fr (nef.ens.fr [129.199.96.12])
	by nez-perce.inria.fr (8.8.7/8.8.7) with ESMTP id MAA23869
	for <caml-list@inria.fr>; Tue, 7 Sep 1999 12:23:23 +0200 (MET DST)
Received: from clipper.ens.fr (clipper-gw.ens.fr [129.199.1.22])
          by nef.ens.fr (8.9.3/beig-1.0) with ESMTP id MAA14403
          ; Tue, 7 Sep 1999 12:23:22 +0200 (MET DST)
Received: from localhost (frisch@localhost) by clipper.ens.fr (8.8.7/jb-1.1)
	id MAA17492 ; Tue, 7 Sep 1999 12:23:22 +0200 (MET DST)
Date: Tue, 7 Sep 1999 12:23:21 +0200 (MET DST)
From: Alain Frisch <frisch@clipper.ens.fr>
X-Sender: frisch@clipper
To: David Monniaux <David.Monniaux@ens.fr>
cc: Liste CAML <caml-list@inria.fr>
Subject: Re: throws
In-Reply-To: <Pine.GSO.4.03.9909061924050.9516-100000@basilic.ens.fr>
Message-ID: <Pine.GSO.4.04.9909071214160.16464-100000@clipper>
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
Sender: weis

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