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 KAA20071; Sat, 9 Oct 2004 10:58:10 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f 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 KAA20060 for ; Sat, 9 Oct 2004 10:58:09 +0200 (MET DST) Received: from yquem.inria.fr (yquem.inria.fr [128.93.8.37]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id i998w6gm023515; Sat, 9 Oct 2004 10:58:06 +0200 Received: by yquem.inria.fr (Postfix, from userid 18180) id 8327ABC40; Sat, 9 Oct 2004 10:58:06 +0200 (CEST) Date: Sat, 9 Oct 2004 10:58:06 +0200 From: Xavier Leroy To: "Harrison, John R" Cc: caml-list Subject: Re: [Caml-list] Are you sure the new "=" of 3.08 is good ? Message-ID: <20041009085806.GB17072@yquem.inria.fr> References: <012676D607FCF54E986746512C22CE7D0FE7B8@orsmsx407> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <012676D607FCF54E986746512C22CE7D0FE7B8@orsmsx407> User-Agent: Mutt/1.3.28i X-Miltered: at concorde with ID 4167A81E.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Loop: caml-list@inria.fr X-Spam: no; 0.00; caml-list:01 provers:01 high-level:01 subgraphs:01 raffalli:01 floats:01 settling:99 pervasives:01 pervasives:01 floats:01 damien:01 hash-consing:01 clarifies:01 compiler:01 implements:01 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk > For LCF-style theorem provers, I think it's quite important that when > comparing terms (or similar tree structures) for equality, there should > be a quick "yes" when two high-level subgraphs are pointer eq. [...] > I guess like Christophe Raffalli I had just assumed this would be > the case based on long experience with ML-family languages, rather than > through any explicit discussion in the documentation. I agree the behaviour your describe (x == y implies x = y) is very reasonable. Unfortunately, nan <> nan is also very reasonable, at least if you believe in IEEE floats, and you cannot have both... We agonized a long time on this issue before settling on the current compromise: "=" is compatible with IEEE float equality, and Pervasives.compare implements the behaviour you expect (early stop if ==). > Can you clarify what we need to do in order to guarantee this > behaviour? As I said in an earlier post, you can do let (=?) x y = (Pervasives.compare x y = 0) and use =? instead of = in places where you need the "early stop" behaviour. I advise against Damien's suggestion of defining let (=) x y = (Pervasives.compare x y = 0) because the predefined "=" operator is known to the compiler and is type-specialized to much more efficient code when comparing ints, floats or strings. No such type specialization takes place when "=" is defined in terms of Pervasives.compare. Of course, if the speed of equality is critical, you can also define your own comparison functions for the types of interest, or even (as Damien suggested) implement hash-consing. Hope this clarifies the issue. - Xavier Leroy ------------------- 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