From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id OAA28201; Wed, 22 Sep 2004 14:03:41 +0200 (MET DST) Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id OAA25776 for ; Wed, 22 Sep 2004 14:03:40 +0200 (MET DST) Received: from nef.ens.fr (nef.ens.fr [129.199.96.32]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id i8MC3doM028069 for ; Wed, 22 Sep 2004 14:03:40 +0200 Received: from clipper.ens.fr (clipper-gw.ens.fr [129.199.1.22]) by nef.ens.fr (8.12.11/1.01.28121999) with ESMTP id i8MC3bE2061385 ; Wed, 22 Sep 2004 14:03:37 +0200 (CEST) Received: from localhost (frisch@localhost) by clipper.ens.fr (8.13.1/jb-1.1) id i8MC3aZJ021700 ; Wed, 22 Sep 2004 14:03:36 +0200 (MEST) X-Authentication-Warning: clipper.ens.fr: frisch owned process doing -bs Date: Wed, 22 Sep 2004 14:03:36 +0200 (MEST) From: Alain Frisch X-X-Sender: frisch@clipper.ens.fr Reply-To: Alain Frisch To: "Marcin 'Qrczak' Kowalczyk" cc: skaller@users.sourceforge.net, caml-list Subject: Re: [Caml-list] Re: OCAML Downcasting? In-Reply-To: <87d60eizlh.fsf@qrnik.zagroda> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Virus-Scanned: by amavisd-milter (http://amavis.org/) X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-1.3.3 (nef.ens.fr [129.199.96.32]); Wed, 22 Sep 2004 14:03:37 +0200 (CEST) X-Miltered: at nez-perce with ID 41516A1C.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Loop: caml-list@inria.fr X-Spam: no; 0.00; alain:01 frisch:01 alain:01 frisch:01 caml-list:01 downcasting:01 marcin:01 'qrczak':01 kowalczyk:01 checker:01 checker:01 statically:01 checkers:01 cduce:01 compile-time:01 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk On Wed, 22 Sep 2004, Marcin 'Qrczak' Kowalczyk wrote: > This is the catch: "where possible". I would add: "where practical"; > sometimes the cost outweights the benefits. For example static > detection of possible division by 0 would be impractical. You would > have to either embed a proof checker in the language in order to be > able to convince the compiler that the number can't be 0, or not use > exceptions at all and have all partial functions return a result in > "option" type or similar, with manual propagation of errors. You don't necessarily have to use a proof checker. What about using a type system, or a(nother kind of) static analysis ? E.g. detection of division by 0 can be done with interval arithmetic, and it might work well in practice. > And guess what? No language I know checks division by 0 statically > (except proof checkers, but they are not suitable for writing big > programs - too much work). CDuce version 0.2.1+1 # fun (x : Int) : Int = 1 div x;; Warning at chars 22-29: This operator may fail - : Int -> Int = # fun (x : 0--*) : Int = 1 div x;; Warning at chars 23-30: This operator may fail - : 0--* -> Int = # fun (x : 1--*) : Int = 1 div x;; - : 1--* -> Int = # fun (x : 1--*) : Int = 1 div (x + x);; - : 1--* -> Int = # fun (x : 1--*) : Int = 1 div (x - x + x);; Warning at chars 23-40: This operator may fail - : 1--* -> Int = (type 1--* means: "positive integers") To get rid of warning (or compile-time error) when the type system is not precise enough (the last example above), you can always do an explicit check: # fun (x : 1--*) : Int = match x - x + x with | y & (1--*) -> 1 div y | _ -> raise "Bla";; - : 1--* -> Int = -- Alain ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners