Re: Structure sharing

Chet Murthy (murthy@pauillac.inria.fr)
Thu, 17 Mar 1994 10:21:51 +0100

To: John Harrison <John.Harrison@cl.cam.ac.uk>
Subject: Re: Structure sharing
In-Reply-To: Your message of Wed, 16 Mar 1994 17:01:12 +0000.
<"swan.cl.cam.:120340:940316170214"@cl.cam.ac.uk>
Date: Thu, 17 Mar 1994 10:21:51 +0100
Message-Id: <17303.763896111@pauillac.inria.fr>
From: Chet Murthy <murthy@pauillac.inria.fr>

Hi, John,

I also did some work recently with structure-sharing in Coq.
Specifically, I wrote a caml-light generic hash-conser which walks the
in-memory representation in an unsafe manner, "re-sharing" a
datastructure. Since I don't have type information, I can't detect
the fact that something's mutable, so this only works for purely
applicative data.

Whatever. Anyway, I had an application where I wanted to read
something in off of disk, and then "un-share" it completely - walk it
completely, so I could hash the leaves of the datastructure into a
symbol table. But then, well, the datastructure is unshared - I ought
to re-share it, no? Well, hash-consing was a modest loss on a
reasonable-sized benchmark.

That is, for Constructions at least, the datastructures are simple
enough, and small enough, that hash-consing costs more than it is
worth when it is done "globally"

On the other hand, when I did it on the output of the type-checker,
and the term which I fed as input (coupled, so that the type-checker's
output will be hash-consed "onto" the term being type-checked), I got
a slight speedup.

All this to say that it probably isn't a big win either way, in
caml-light, for Coq.

--chet--