So what about option 2 then? Can Poly/ML expose some other primitives by which I can obtain identifiers for immutable values, such that equal values always have the same identifier? (The other direction (i.e., perfect sharing) would be nice, but is not necessary.)
On 8 October 2015 at 18:29, David Matthews <David.Matthews at prolingua.co.uk> wrote:
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 Icould 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 polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml