English version
Accueil     Ŕ propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis ŕ jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml ŕ l'adresse ocaml.org.

Browse thread
Static exception analysis or alternative to using exceptions
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2010-06-08 (09:16)
From: Goswin von Brederlow <goswin-v-b@w...>
Subject: Re: [Caml-list] Static exception analysis or alternative to using exceptions
"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

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.