From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 052307EE5B for ; Tue, 27 May 2014 11:28:29 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of goswin-v-b@web.de) identity=pra; client-ip=212.227.17.12; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="goswin-v-b@web.de"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of goswin-v-b@web.de) identity=mailfrom; client-ip=212.227.17.12; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="goswin-v-b@web.de"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mout.web.de) identity=helo; client-ip=212.227.17.12; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="postmaster@mout.web.de"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Aq0BAHRZhFPU4xEMnGdsb2JhbABZsXWUUAGBDhYOAQEBAQEGDQkJFCiCJQEBBAEnE08LGAklDwUoiGEBDAzNRh+GUheOWYMrgRUEmXKGVRKPew X-IPAS-Result: Aq0BAHRZhFPU4xEMnGdsb2JhbABZsXWUUAGBDhYOAQEBAQEGDQkJFCiCJQEBBAEnE08LGAklDwUoiGEBDAzNRh+GUheOWYMrgRUEmXKGVRKPew X-IronPort-AV: E=Sophos;i="4.98,917,1392159600"; d="scan'208";a="64308791" Received: from mout.web.de ([212.227.17.12]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 27 May 2014 11:28:28 +0200 Received: from frosties.localnet ([78.43.112.61]) by smtp.web.de (mrweb102) with ESMTPSA (Nemesis) id 0LfzxX-1WWOFV357D-00pbps for ; Tue, 27 May 2014 11:28:27 +0200 Received: from mrvn by frosties.localnet with local (Exim 4.82) (envelope-from ) id 1WpDgG-0004N9-RL for caml-list@inria.fr; Tue, 27 May 2014 11:28:24 +0200 Date: Tue, 27 May 2014 11:28:24 +0200 From: Goswin von Brederlow To: caml-list@inria.fr Message-ID: <20140527092824.GB15848@frosties> References: <53835610.9050609@inria.fr> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.23 (2014-03-12) X-Provags-ID: V03:K0:e+CnC7Rst5v/ISW4sBa28CPJay0yxuViVmb+D0X3BnuMraZrHMt M/s77I1E4sSAufas5ltWgxlP/hv5mH15GYj4GFCxBFMIZVnD9mDg5Y478YBSvGaIDmfKmSX zycdG4FFWeyqjuCjkBsyhrux7i0NKL6Ev7zQR5lYkI0Oq5KJqNvYtXgTryJ4E6ArRxYof1o ibwy7NHrX+hxRQ36mybHA== Subject: Re: [Caml-list] Uncaught exceptions in function type. On Mon, May 26, 2014 at 05:25:21PM +0200, Philippe Veber wrote: > Hi Romain! > > > > Some issues: > > > > - One needs to separate exceptions into two groups, the ones that you > > are actually interested in typing (their purpose is to kill the program, > > so to speak) and the ones that you are not (they are actually used for > > control flow). > > > I would not like such a separation, unless the user can decide the kind of > each exception (did you say burdensome? ;o). This kind of separation is > pretty much the reason why there are errors and exceptions in Java, IIRC. An exception that is used for control flow will be thrown and quickly caught. It would not appear in a functions signature if the control flow is done right. But if you made a mistake and didn't catch it then it should appear in the signature and give you cause to recheck your code. I would say that exceptions used for control flow are exactly the ones that you want typed. On the other hand exceptions that kill the programm, like out of memory, would be completly useless to type. Basically anything can throw out of memory and nobody can catch it. It would simply appear in every single (non trivial) function and annoy the programmer. > > - I'm not sure it is easy to infer. For instance, in: > > > > let f g = > > g 1 > > > > should we just assume that g raises nothing? > > No, we should assume g raises something, and that f raises the same. > > > > Or should we use some kind > > of row variable, like: > > > > let f (g: 'a raise ([< ] as 'raises): 'b raise 'raises = > > g 1 > > > > Yes more like that > > > > > > But then what about: > > > > let f > > (g: 'a raise ([< ] as 'raises_h) > > (h: 'a raise ([< ] as 'raises_g): 'b raise [ 'raises_g | 'raises_h ] = > > g 1 + h 2 > > > > is it sound to have those abstract union types [ 'raises_g | 'raises_h ]? > > > > I guess it is not easy because 'raises_g and 'raises_h may have > incompatibilities (same constructors with different arguments). Since you > worked on union of abstract polymorphic variant types, I guess you know > pretty well how difficult that would be ;o). # exception Foo of int;; exception Foo of int # let f () = raise (Foo 1);; val f : unit -> 'a = # exception Foo of float;; exception Foo of float # let g () = raise (Foo 1.0);; val g : unit -> 'a = # let h () = f () + g ();; # let h () = let t = f () in g ();; Warning 26: unused variable t. val h : unit -> 'a = # f ();; Exception: Foo 1. # g ();; Exception: Foo 1.. # h ();; Exception: Foo 1. # try h (); 1.0 with Foo x -> x;; Warning 21: this statement never returns (or has an unsound type.) Exception: Foo 1. Nothing wrong with h () raising [ Foo of int | float ] other than that it makes it impossible to catch because Foo of int is shadowed by Foo of float. The user couldn't catch both, the compiler would infer that anything using h throws at least Foo of int and the user would quickly realize that it wasn't a good idea to have to constructors with different types. Problem solved. Actualy infering exceptions would be a great help there. The user might think that he caught Foo of int in the above code. The compiler would proof him wrong highlighting the problem. But consider the following: let h f = let t = f () in function g -> g () val h : (unit -> 'a raise ([< ] as 'rf)) -> (((unit -> 'a raise ([< ] as 'rg)) -> unit raise 'rg)) raise 'rf Here h raises both 'rf and 'rg, just like in the above example. BUT 'rf is raised on and only on the partial application of f. This is important when you have: let h' f g = let t = try Some (f ()) with Foo x -> None in match t with | None -> None | Some x -> g x The compiler has to see that (at least some of) the execptions of f are cought and only the exceptions of g can be raised (and what isn't cought of f). Types can get rather comvoluted. But hey, if they type gets to complex then maybe you should try using less exceptions and more variant types and options. :) > > Do we want all functions to have these convoluted types? > > > Representing those types could be optional most of the time. The only place > where they would be important would when catching exceptions, to have the > compiler check for exhaustivity. And .mli files and signatures. But I agree that the point of infering exceptions would be to have the compiler check that there are none (or only the short list of allowed exceptions). That just leaves higher level functions. They would all have to be convoluted. Also would # let f g x = g x val f : ('a -> 'b) -> 'a -> 'b = mean that g must not throw any exceptions? Or can the type system infer that f will throw the same exceptions as g because no complex exception type was specified? Can we make the "raise ([< ] as 'raises_g)" part implied? That would greatly help the transition and cut down on convoluted types. The case of higher level functions just passing through any exceptions would be the most common case and should have a simple type. MfG Goswin