From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id 1EC60BC57 for ; Tue, 8 Jun 2010 11:16:25 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AmkCAC+nDUzZSMDdkWdsb2JhbACeQRUBAQEBCQsKBxEDH70PhRYE X-IronPort-AV: E=Sophos;i="4.53,383,1272837600"; d="scan'208";a="60857408" Received: from fmmailgate01.web.de ([217.72.192.221]) by mail1-smtp-roc.national.inria.fr with ESMTP; 08 Jun 2010 11:16:24 +0200 Received: from smtp03.web.de ( [172.20.0.65]) by fmmailgate01.web.de (Postfix) with ESMTP id 62AAA15DD8F88; Tue, 8 Jun 2010 11:16:23 +0200 (CEST) Received: from [78.43.204.177] (helo=frosties.localdomain) by smtp03.web.de with asmtp (TLSv1:AES256-SHA:256) (WEB.DE 4.110 #4) id 1OLuv1-0000SI-00; Tue, 08 Jun 2010 11:16:23 +0200 Received: from mrvn by frosties.localdomain with local (Exim 4.72) (envelope-from ) id 1OLuv0-0002IQ-LI; Tue, 08 Jun 2010 11:16:22 +0200 From: Goswin von Brederlow To: "David Allsopp" Cc: "'Goswin von Brederlow'" , "'Richard Jones'" , Subject: Re: [Caml-list] Static exception analysis or alternative to using exceptions References: <20100527170122.GA28273@annexia.org> <87y6f0cf4p.fsf@frosties.localdomain> <002c01cb00e6$20bfcd30$623f6790$@romulus.metastack.com> Date: Tue, 08 Jun 2010 11:16:22 +0200 In-Reply-To: <002c01cb00e6$20bfcd30$623f6790$@romulus.metastack.com> (David Allsopp's message of "Mon, 31 May 2010 18:24:28 +0100") Message-ID: <87aar5995l.fsf@frosties.localdomain> User-Agent: Gnus/5.110009 (No Gnus v0.9) XEmacs/21.4.22 (linux, no MULE) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Sender: goswin-v-b@web.de X-Sender: goswin-v-b@web.de X-Provags-ID: V01U2FsdGVkX18RX6SAG0Vi6DK2y4SYnE0JZbUMKH1ppcfNxxD+ GG8C820jEoza0exCvBCJiMAQoCWq5jtAdAQG5owcswtJIeggYq t5L2pqU9Y= X-Spam: no; 0.00; ocaml:01 lacks:01 impl:01 'open:01 'open:01 val:01 val:01 ocamlexc:01 ocaml:01 compiler:01 specifies:01 sig:01 struct:01 hashtbl:01 hashtbl:01 "David Allsopp" writes: > Goswin von Brederlow wrote: > >> > 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