Sharing

Sharing

[Pierre Weis]

Hi John,

As far as I know nobody have ever tried to implement global hash
consing in CAML. However structure-sharing on terms handled by the coq
system have been used once. It revealed to be interesting but not
decisive for efficiency.

On the other hand, there exists at least one implementation of ML
featuring hash-consing: HiML written by Jean Goubault
(J.Goubault@frcl.bull.fr). He showed that this can be feasible and efficient.

If you don't want to share everything ever allocated in the memory but
some well identified objects, you can perfectly use hash tables. The
problem is, as you mentioned it, that objects you put in a global hash
table cannot be reclaimed by the garbbage collector, since they are in
used (in the hash table!). This is not a problem, if you already know
that these object are structures or parts of structures already used
elsewhere. That's why sharing was used in coq for theories, that were
necessarily manipulated by the theorem prover.

Finally, the hash tables in the "hashtbl" module are not magic: they
are written in Caml, and you can read the source code which is in the
standard distribution. We do not claim that these hash tables got
the most efficient implementation: their implementation is reasonably
good and works very fine in most cases. But since you have the source
code, you can adapt this code to your particular problem, it a very
common practice to redefine some of the library functions to tune it
to a particular use.


Pierre Weis