From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 48ECABC51 for ; Mon, 29 Nov 2004 12:27:48 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id iATBRlt9029358 for ; Mon, 29 Nov 2004 12:27:48 +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 MAA22340 for ; Mon, 29 Nov 2004 12:27:47 +0100 (MET) Received: from decis.be ([194.78.219.157]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id iATBRkn2029355 for ; Mon, 29 Nov 2004 12:27:47 +0100 Received: from decis.be by decis.be (MDaemon.PRO.v7.2.0.R) with ESMTP id md50000150688.msg for ; Mon, 29 Nov 2004 12:27:55 +0100 Message-ID: <41AB07B3.E2F0DF1D@decis.be> Date: Mon, 29 Nov 2004 11:27:47 +0000 From: Frederic van der Plancke Organization: Decis X-Mailer: Mozilla 4.77 [en] (Windows NT 5.0; U) X-Accept-Language: en,fr-BE,fr MIME-Version: 1.0 To: caml-list@inria.fr Subject: Re: [Caml-list] Why doesn't ocamlopt detect a missing ; afterfailwith statement? References: <1101438486.9291.138.camel@pelican.wigram> <20041126.142525.93385094.garrigue@math.nagoya-u.ac.jp> <20041129.094035.02308731.garrigue@math.nagoya-u.ac.jp> Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-Authenticated-Sender: fplancke@decis.be X-MDRemoteIP: 192.168.0.20 X-Return-Path: fvdp@decis.be X-MDaemon-Deliver-To: caml-list@inria.fr Reply-To: fvdp@decis.be X-Miltered: at concorde with ID 41AB07B3.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 41AB07B3.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; plancke:01 caml-list:01 ocamlopt:01 wrote:01 damien:01 damien:01 failwith:01 forall:01 failwith:01 foo:01 foo:01 inference:01 annotation:01 compiler:01 noreturn: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: Jacques Garrigue wrote: > > From: Damien Doligez > > > I believe the problem with failwith is solvable, albeit rather > > > complicated. The idea is that you want to be warned when you apply a > > > function of type (\forall 'a. 'a) to something, because no such > > > function may exist, so that this application will never actually take > > > place. > > > > More generally, you want to output a warning whenever the computation > > of such a value is not immediately followed by a join in the control > > flow graph, because at that point you know you're compiling dead code. > > > > Then you would also get a warning for things like this: > > > > failwith "foo"; > > print_string "hello world" > > > > or > > > > f (a, b, failwith "foo", c, d) > > > > etc. > > > > Don't ask me to implement it, though. > > This is not specially hard to implement case by case. > 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]) * a warning would be issued - for an "apply" node when any input term has type noreturn - for a ";" node when the first term has type noreturn - etc * problem: one could write [Obj.magic 123 : noreturn] (or similarly in other cases like marshalling where a lone 'a *can* correspond to a value) and defeat the system. possible solution: forbid or restrict explicit casts (er, type annotations, sorry ;-) to noreturn. (i.e. since 'a annotates "a value of any type" and noreturn annotates "no value", there's no reason to allow "casting" 'a as noreturn.) Frédéric vdP