From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 34959BC51 for ; Mon, 29 Nov 2004 12:43:46 +0100 (CET) Received: from kurims.kurims.kyoto-u.ac.jp (kurims.kurims.kyoto-u.ac.jp [130.54.16.1]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id iATBhijW004168 for ; Mon, 29 Nov 2004 12:43:45 +0100 Received: from localhost (suiren [130.54.16.25]) by kurims.kurims.kyoto-u.ac.jp (8.13.1/8.13.1) with ESMTP id iATBhcHD010428; Mon, 29 Nov 2004 20:43:38 +0900 (JST) Date: Mon, 29 Nov 2004 20:43:24 +0900 (JST) Message-Id: <20041129.204324.40572703.garrigue@math.nagoya-u.ac.jp> To: fvdp@decis.be Cc: caml-list@yquem.inria.fr Subject: Re: [Caml-list] Why doesn't ocamlopt detect a missing ; afterfailwith statement? From: Jacques Garrigue In-Reply-To: <41AB030B.EA2E9530@decis.be> References: <20041129.094035.02308731.garrigue@math.nagoya-u.ac.jp> <41AB030B.EA2E9530@decis.be> X-Mailer: Mew version 4.0.64 on Emacs 21.3 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Miltered: at nez-perce with ID 41AB0B70.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 ocamlopt:01 plancke:01 inference:01 annotation:01 compiler:01 noreturn:01 compiler:01 exn:01 noreturn:01 failwith:01 unification:01 surprising:01 foolproof:98 assert: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: From: Frederic van der Plancke > > The problem is rather that the technique I use, based on type > > inference, is not foolproof (you can avoid the warning with a type > > annotation for instance) and is wrong in presence of Obj.magic. > > So the question is in which cases having a warning is worth the > > inconvenience and the extra code in the compiler. > > Why not create a special type "noreturn" or "empty" with special typing properties ? in most respect it would act like 'a; but the compiler would know the difference. > * raise : exn -> noreturn (and hence: failwith : string -> noreturn) > (similarly: [assert false : noreturn]) > but Obj.magic keeps its type : 'a -> 'b > * noreturn can be unified to any type t (including 'a), this yields type t > (so [function [] -> assert false | x::_ -> x] has type ['a list -> 'a]) This just looks like a much higher cost in terms of changes to the compiler. And the danger of introducing bugs in unification, just for a warning in some strange cases. (You should realize that what you are proposing is not a new type, but a new kind of type variables.) The generalization technique works well. It is not surprising that it doesn't mix that well with Obj.magic, but then Obj.magic is clearly unsound, so you know what to expect. Objective Caml version 3.09+dev9 (2004-11-29) # fun () -> raise Exit print_int 3;; ^^^^^^^^^ Warning X: this argument will not be received by the function. # fun () -> raise Exit; "Hello";; ^^^^^^^^^^ Warning X: this statement never returns. # fun f -> ((Obj.magic f) 3);; ^ Warning X: this argument will not be received by the function. # fun f -> ((Obj.magic f : _ -> _) 3);; - : 'a -> 'b = Jacques Garrigue