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

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

Hi there,

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 = { t_11 -> t_1, ..., t_1k -> t_1, ..., t_n1 -> t_n, ..., t_nk -> t_n }
    t_i admits equality if some t_ij does                        i=1..n, j=1..k
                               \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.

The question is whether the requirement \rea(E_1) = ... = \rea(E_n) is
too strong for some practical purposes? I counted the number of
structure sharing constraints in the ML Kit sources and found 123 such
constraints, which would all elaborate with the rule above. Although I
do not consider the SML'97 notion of structure sharing completely
useless, I would consider implementing a (better) rule for structure
sharing in the ML Kit implementation if the major sml-implementers
would agree on such a rule.

Cheers,

Martin