Re: [Caml-list] Static exception analysis or alternative to using exceptions

[Goswin von Brederlow <goswin-v-b@web.de>]

"David Allsopp" <dra-news@metastack.com> writes:

> Goswin von Brederlow wrote:
> <snip>
>> > However if the exception is, say, an I/O error reading a disk file,
>> > these should be thrown, and caught somewhere central where you can
>> > display an error message to the user (for GUI programs) or abort the
>> > current transaction (for server programs).  Recovering from such
>> > exceptions properly is still tricky though.  Since OCaml lacks
>> > 'finally', you either have to use a 'finally' impl from a library, or
>> > modify your code to not need it (eg. turning calls to 'open_in' and
>> > 'open_out' into a kind of continuation-passing style).  Or for small
>> > programs, abort the program and don't deal with recovery at all.
>> >
>> > All in all, this is not ideal for writing correct programs.  Some sort
>> > of exception analysis would be most welcome.
>> 
>> It would be nice if the possible exceptions of a function would be part of
>> the type. E.g.
>> 
>> let f1 () = raise Not_found
>> val f1 : unit -> 'a [ Not_found ]
>> 
>> let f2 () = try f1 () with Not_found -> () val f2 : unit -> unit
>> 
>> let f3 f = try f () with Not_found -> () val f3: (unit -> 'a [< Not_found
>> | 'B ]) -> 'a [ 'B ]
>> 
>> and so on.
>> 
>> 
>> Someone would have to write a new type system for that though.
>
> Would it be more practical to have that analysis as part of the .annot file?
> Presumably a patch which merged and updated the codebase of ocamlexc to
> produce exception-annotations in that manner might have a chance of making
> it into the OCaml compiler itself. I'm guessing that what you're getting at
> is the ability to see from your code that an exception could escape at any
> given point rather than trying to add Java-style "checked exceptions" to
> OCaml?
>
>
> David

It want it to fail to compile if the interface specifies one set of
exception and the code produces another that is incompatible. The
following should not compile:

module M : sig
  val f : int -> int []
end = struct
  let h = Hashtbl.create 0
  let f x = Hashtbl.find x
end

Since Hashtbl.find can throw Not_found and the function does not catch
that the function still can throw Not_found. This violates the
declaration in the signature that says it never throws an exception.

This goes beyond just annotating what exception can be thrown. It should
do a real validation.

MfG
        Goswin