hash and nums

hash and nums

[Jean-Christophe Filliatre]

It seems that the properties
   
	(eq_num n1 n2)  =>  (hash n1) = (hash n2)
	(eq_num n1 n2)  =>  (compare n1 n2) = 0

are now true in ocaml  3.00, although not stated in the documentation.
Can we safely assume these properties from now on?

-- 
Jean-Christophe Filliatre    
  Computer Science Laboratory   Phone (650) 859-5173
  SRI International             FAX   (650) 859-2844
  333 Ravenswood Ave.           email  filliatr@csl.sri.com
  Menlo Park, CA 94025, USA     web    http://www.csl.sri.com/~filliatr

  

Re: hash and nums

[Xavier Leroy]

> It seems that the properties
> 	(eq_num n1 n2)  =>  (hash n1) = (hash n2)
> 	(eq_num n1 n2)  =>  (compare n1 n2) = 0
> are now true in ocaml  3.00

Not quite.  All rationals hash to the same value, and all big integers
to the same value (a different one).  Comparisons still fails on
nums that are not small integers and that are not physically equal:

  # open Num;;
  # compare (num_of_string "1/2") (num_of_string "2/4");;
  Uncaught exception: Failure "equal: abstract value".

The new "custom blocks" in OCaml 3.00 would allow proper comparison and
hashing functions to be defined on the type nat (the lowest-level big
integer type), because this type is directly implemented in C.

However, higher-level numerical types such as big_int, ratio and num
are defined as Caml data structures, and thus we can't associate the
right comparison and hashing functions on them. E.g. for rationals,
the generic equality code would still compare 1/2 and 2/4 by comparing
1 with 2 and 2 with 4, without doing any normalization.

So, we chose not to put comparison and hashing functions on the type
"nat", because this would only lead to misleading results on the other
numerical types.  (However, "nat" can now be serialized and
deserialized, and so are the other bignum types.)

It's only for bignum libraries where all numerical types are defined
in C, such as GMP, that we could attach the right comparison and
hashing operators to bignums.

- Xavier Leroy