[Sml-implementers] nailing down structure sharing

[Derek D. <dr...@cs...>]

Back to the question which inadvertently brought on this email frenzy:
What is the right design for structure sharing?  We (at TILT) would
really like to nail this down, and we don't feel it should be too hard
to come to a consensus.

To recap the discussion:

1) David Matthews made a point about structure sharing being overly
restrictive because you can effectively only write a sharing constraint
between two structures with fully opaque signatures.  SML/NJ employs a
strategy whereby two structures can be shared if they have the same
signature *variable* but this is semantically rather dubious.  An
example of where this comes up is in the Twelf compiler, which compiles
under SML/NJ but is not Definition-compliant because it makes use of
sharing between structures with translucent signatures.

2) Stephen Weeks replied that he doesn't find completely avoiding type
definitions in signatures very restrictive.  I find this surprising,
since translucent signatures are one of the major advances of SML '97.

3) We posted the TILT proposal for loosening the definition of structure
sharing.  In short, what we propose is that structure sharing should
first add sharing constraints between all flexible (i.e. opaque) type
components contained in the signatures of both structures.  Then, the
remaining type components contained in both signatures should be checked
to ensure that they are equivalent.  At the very least, our proposal
(unlike the Definition) allows structure sharing between any structures
with the same signature.  See our proposal for more details at:

http://www.cs.cmu.edu/~dreyer/structure_sharing.txt

4) Martin Elsman proposed a Definition-style rule for structure sharing
that he said was based on the TILT proposal.  I'm still not sure what
its effect is, but it seems offhand quite different from ours.  In
particular, it appears to require all the structures being shared to
have all the same value components as well, unless I read it wrong.  I
see no reason to be so restrictive.  Structure sharing is supposed to be
a convenient way of summarizing a long list of type definitions, not a
hindrance.

5) There was also some discussion of "where structure" instead of
structure sharing.  The advantage of "fixing" structure sharing instead
of adding "where structure" is that it doesn't involve changing the
syntax of SML.  Personally, however, I (and I think also Bob Harper)
would prefer "where structure" if I had a choice.  The semantics of type
sharing is much harder to define and to explain than the semantics of
"where type", and likewise for structures.  Matthias Blume disagrees and
prefers symmetric equality constraints on types to asymmetric ones.

Thoughts?

Derek