On Thu, 30 Jan 2014, David Matthews wrote:
The intention of PolyML.pointerEq is that if pointerEq(x, y) is true
then x = y will be true, assuming the type of x and y admits equality.
It is really intended for use where a user function wants to test for
equality in some general sense and knowing that actually the values are
the same pointer can short circuit the process.
The only safe way to maintain identity of cells is to use a counter or a
ref. An alternative to a ref is to use a locally generated exception and
this may be more efficient than a ref. As a work-around to avoid the
problem with duplication in the multi-threaded collector you could force
it to be single-threaded with --gcthreads=1.
Thank you for the nice explanations, and the implementation behind it.
The puristic approach to structutal equality in SML turns out as a benefit
these days, when the system runs with loosened brakes on multicore
hardware. Neither the JVM nor OCaml could afford that (but I think
Haskell / GHC does).
I did not know about the unique status of locally generated exceptions
yet. Does the SML standard actually say anything about exception
equality? Would you recommend that as a practical approach? It seems to
be a candidate for incompatibilities between non-equal SMLs.
In Isabelle/ML we had unit ref as "stamp" over many years, but we now do
it in a fairly standard way via some global (synchronized) counter:
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2013-2/src/Pure/ML-Systems/multithreading_polyml.ML#l177
This involves some overhead to create a fresh item, but later comparisons
are pure, and there is also a conical time-stamp order on it.
Makarius
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
