Hi Ramana,
I've thought about this and I really don't think it would be a good idea
to allow weak references to contain immutable data. It's not just that
sometimes entries could be retained unexpectedly it's that they could
also be discarded while the data is still reachable. The multi-threaded
GC uses weak coherency for immutable data which means that there is a
finite possibility of a cell being duplicated. That in turn could mean
that the entry in the weak reference would be set to NONE while the data
still exists. From the point of view of your users it could mean that
your identifiers would change from run to run. I think if you want to
use weak references you're going to have to accept the overhead of an
extra mutable cell in order to get consistent behaviour.
Regards,
David
On 06/10/2015 23:48, Ramana Kumar wrote:
Hi David,
Thanks very much for the explanation.
My motivation for hash-consing is as follows. I want to add an id (an
integer) that is (at least) unique for every distinct value of certain
types in the HOL4 kernel. (The motivation for these ids is on-the-fly
proof-recording by emitting a trace of kernel operations.) Hash-consing
would allow me to re-use ids for new constructions of values that are equal
to existing values.
From your explanation, I understand that Poly/ML's garbage collector is
already effectively doing hash-consing via its "sharing" phase. However, if
I add ids to my values, they will no longer be equal from the garbage
collector's perspective and I will lose the benefits of sharing. (An
alternative perspective: if I add ids, I will not know when to re-use the
same id because the garbage collector doesn't expose information about
whether a structurally equal (modulo the id) value is reachable already.)
So this leaves me with two avenues to pursue:
1. Would it be easy to add an alternative interface to the garbage
collector wherein weak pointers can point to immutable data? (So I could
use that with my own hash-consing, given that I don't care about being
precise about discovering whether some object is reachable or not.)
2. Or, could Poly/ML expose some primitives by which I could add unique
ids to certain objects (or simply read existing ids if you already have
them) while benefiting from the garbage collector's own
hash-consing/sharing implementation?
Thanks,
Ramana
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
