From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 2AC14BB91 for ; Fri, 28 Jan 2005 01:57:29 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j0S0vSNG009246 for ; Fri, 28 Jan 2005 01:57:28 +0100 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id BAA11955 for ; Fri, 28 Jan 2005 01:57:28 +0100 (MET) Received: from smtp1.adl2.internode.on.net (smtp1.adl2.internode.on.net [203.16.214.181]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j0S0vQ8T013852 for ; Fri, 28 Jan 2005 01:57:27 +0100 Received: from [192.168.1.200] (ppp205-248.lns1.syd3.internode.on.net [203.122.205.248]) by smtp1.adl2.internode.on.net (8.12.9/8.12.9) with ESMTP id j0S0vJTX081259; Fri, 28 Jan 2005 11:27:20 +1030 (CST) Subject: Re: [Caml-list] Re: '_a From: skaller Reply-To: skaller@users.sourceforge.net To: Vincenzo Ciancia Cc: caml-list In-Reply-To: References: <1448756C-6FF9-11D9-8411-0003939A19AA@fas.harvard.edu> <20050127.095119.88330421.garrigue@math.nagoya-u.ac.jp> <1106818474.6734.152.camel@pelican.wigram> Content-Type: text/plain Message-Id: <1106873838.12114.128.camel@pelican.wigram> Mime-Version: 1.0 X-Mailer: Ximian Evolution 1.2.2 (1.2.2-4) Date: 28 Jan 2005 11:57:19 +1100 Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 41F98DF8.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 41F98DF6.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 sourceforge:01 wrote:01 wrote:01 ocaml:01 enforces:01 inference:01 ocamlexc:01 ocamlexc:01 hashtbl:01 rec:01 endline:01 compiler:01 monadic:01 gotos:01 X-Spam-Checker-Version: SpamAssassin 3.0.0 (2004-09-13) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.0 X-Spam-Level: On Fri, 2005-01-28 at 01:13, Vincenzo Ciancia wrote: > skaller wrote: > > > An exception free implementation of List.hd would > > always produce the correct typing: > > > > let hd x = function > > | [] -> None > > | h :: _ -> Some h > > > > In effect, Ocaml first pretends unsound typing is actually sound, > > and then enforces this at run time by throwing an exception > > where one would otherwise accuse the type system of unsoundness, > > but claims the error is not a type error. > > What about the possibility to include possible exceptions into a function > signature (a la java)? Does this have problems with type inference? Well I doubt the Java technique is any more meaningful than the C++ one. There are three meanings of exceptions: (a) the function domain was mis-specified, there is actually an unstated constraint on it: the correct signature for division is: divide: integer - { 0 } -> integer (b) the codomain is mis-specified, we actually have List.hd: 'a list -> Some 'a but enforce codomain 'a instead by throwing in the None case (c) The function depends on some complex details not considered part of the program, which can fail, for example status of a file. Documenting the exception instead of the constraint on the signature doesn't seem very nice. > Also, > there is the ocamlexc tool: > > http://caml.inria.fr/ocamlexc/ocamlexc.htm > > what about it? > If I recall, this is a superb tool backed by some very smart theory -- but in practice the output is extremely hard to interpret. Exceptions are often used where the constraint is expected to be satisfied -- I myself say: .. Hashtbl.find table key ... without any try/with wrapper when I 'know' the key is in the table, and I may write .. List.hd l ... instead of match l with | [] -> assert false | h :: _ -> h However these uses of cast 'magic' are distinct from alternate returns, where one sometimes has to cheat the type system in the opposite direction, adding a dummy value to code that will never be used just to get the type right: let x = let rec f l -> | [] -> raise Not_found | h :: t -> if h == v then (raise Found; 0) else f t in try f l with Found -> 1 | Not_found -> 2 in print_endline (string_of_int x) ;; where the compiler doesn't know f l cannot return, so it needs a useless '0' after the Found case to get the typing correct. (Or you could add it after the 'try f l', either way it's equivalent to a safe use of Obj.magic, safe since the cast will never be applied). I guess some of these cases would be better handled with a monadic technique, static exceptions, or just doing the nasty testing: in many ways, exceptions are *worse* than gotos, since at least the latter in ISO C require the target to be visible. BTW: Felix actually uses goto to replace exceptions, and makes you pass handler into the code if necessary: proc error() { goto endoff; } fun g(e:unit->void) { ... error(); ... } ... endoff:> // error found .. Thus if you can't see the handler target in the code, you can pass a closure which can. This guarrantees you cannot fail to catch an exception. It is still flawed though. -- John Skaller, mailto:skaller@users.sf.net voice: 061-2-9660-0850, snail: PO BOX 401 Glebe NSW 2037 Australia Checkout the Felix programming language http://felix.sf.net