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

[Christophe Raffalli <christophe.raffalli@univ-savoie.fr>]

I spend one complete day to adapt Phox (my theorem prover) to 3.08
because the new = does not check first physical equality. Hopefully, the 
backtracking ocamldebugger let me pin point the many "=" which were 
looping, otherwise I would have spend a month !!!

I was assuming two things about equal:
- scan of block from left to right
- a test on adress equality on pointer before follwing the pointer 
(which is now wrong in 3.08).

Then in a data type with some structure starting with an identifier 
filed like

type symbol = structh { id : int; ... },

if you have the property that two structures with the same id are always 
physically equal, the old "=" would never scan the structure itself.

The new "=" can dramatically change the complexity of a program using 
such a structure. It can even loop if your data type are cyclic but all 
cycle need to traverse a structure with the above property (in this case 
the old "=" did not loop).

I imagine there are other examples where the old "=" can be much faster 
than the new one.

So the comparison between both "=" gives

old "=":
- can have much better complexity of some specific data structure
- nan = nan => true

new "="
- can have a small linear speedup on some specific data structure
- nan = nan => false

Clearly for most ocaml programmer the old "=" was better.

Moreover, code relying on, nan = nan to give false are very suspicious 
to me !!! If you need to debug, you have better to insert assertion 
about your floats.

Finally, the IEEE norm about floating point arithmetic is not perfect 
yet. For instance it makes nothing about transcendentals function (see 
below) so I really do not think this norm is so good that OCaml MUST 
respect it for polymorphic equality (a new better norm may appear one day).

--
Here are two small problems with the actual implementation of float:

asin 1.000001 gives nan while some floating point expression which you 
can mathematically prove to be in [-1, 1] gets computed as 1 + epsilon !
so asin x should be equal to asin 1 if x > 1 (idem for -1) otherwise all 
call to asin shoud do a comparison with 1 and -1

sin x with x > 10e100 gives a value which is certainly wrong since you 
can not compute the modulo 2 pi for such a big number.
sin x should give nan when |x| is too big.

-- 
Christophe Raffalli
Université de Savoie
Batiment Le Chablais, bureau 21
73376 Le Bourget-du-Lac Cedex

tél: (33) 4 79 75 81 03
fax: (33) 4 79 75 87 42
mail: Christophe.Raffalli@univ-savoie.fr
www: http://www.lama.univ-savoie.fr/~RAFFALLI
---------------------------------------------
IMPORTANT: this mail is signed using PGP/MIME
At least Enigmail/Mozilla, mutt or evolution
can check this signature
---------------------------------------------

-------------------
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