Re: [Caml-list] Are you sure the new "=" of 3.08 is good ?

[Xavier Leroy <Xavier.Leroy@inria.fr>]

> 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