Re: [Sml-implementers] Sensible Structure Sharing for Standard ML

[Martin E. <ma...@di...>]

Hi again,

The rule for structure sharing I posted earlier contained a few flaws;
a better rule is given below.

Based on the suggestion by Derek Dreyer and Leaf Petersen, I came up
with the following rule for structure sharing specifications:

           B |- spec => E      E_i = E(longstrid_i)     i=1..n
    E_i(longtycon_j) = (t_ij, VE_ij)     t_ij \not\in T of B     i=1..n, j=1..k
               \rea_j = { t_1j -> t_j, ..., t_nj -> t_j }    j=1..k  
             t_j admits equality if some t_ij does,  j=1..k
          \rea = \rea_k o ... o \rea_1     \rea(E_1) = ... = \rea(E_n)
    ----------------------------------------------------------------------------
           B |- spec sharing longstrid_1 = ... = longstrid_n => \rea(E)

Notes:

   1. Structure sharing is transitive, reflexive, and commutative,
      thus the rule is less permissive than SML'97 in this respect;
      see The Def. page 85.

   2. The requirement \rea(E_1) = ... = \rea(E_n) forces all long type
      constructors bound to flexible type names to be considered.

I counted the number of structure sharing constraints in the ML Kit
sources and found 123 such constraints, thus I won't consider the
SML'97 notion of structure sharing completely useless. On the other
hand, if the major sml-implementers agree on some (better) rule for
structure sharing, I would consider implementing the rule in the ML
Kit implementation.

Cheers,

Martin