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 <[email protected]> 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 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 >
_______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
