Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 1999-09-07 (11:33)
From: Alain Frisch <frisch@c...>
Subject: Re: throws
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
  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