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

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

Hi again,

The rule for structure sharing specifications I posted earlier
contained yet a few flaws related to getting the unification of type
names right. Based on the suggestion by Derek Dreyer and Leaf
Petersen, here is my third go for a rule for structure sharing
specifications:
                                                    +----------------+
                                                    | B |- spec => E |
                                                    +----------------+

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

      Reflexivity:
         If   B |- spec => E   and    E' = E(longstrid)  
         then   B |- spec sharing longstrid = longstrid => E

      Reflexivity':
         If   B |- spec sharing longstrid_1 = ... = longstrid_n => E
         then   B |- spec sharing longstrid_1 = ... = longstrid_n
                          sharing longstrid_1 = ... = longstrid_n => E

      Commutivity: 
         If   B |- spec sharing longstrid_1 = longstrid_2 => E 
         then    B |- spec sharing longstrid_2 = longstrid_1 => E 

      Commutivity': 
         If   B |- spec sharing longstrid_1 = ... = longstrid_n
                        sharing longstrid_1' = ... = longstrid_m' => E
         then  B |- spec sharing longstrid_1' = ... = longstrid_m'
                         sharing longstrid_1 = ... = longstrid_n => E

      Transitivity:    
         If   B |- spec sharing longstrid_1 = longstrid_2
                        sharing longstrid_2 = longstrid_3 => E 
         then    B |- spec sharing longstrid_1 = longstrid_2
                           sharing longstrid_1 = longstrid_3 => E

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

In the framework of my thesis work, the rule may be formulated as
follows; see chapters 2 and 3 of my thesis:
                                                    +-------------------+
                                                    | B |- spec => T(E) |
                                                    +-------------------+

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

In this framework, a realisation-closedness property holds:

 Proposition 3.1.10: Let phrase be either a specification or a
 signature expression. If   B |- phrase => (T)E    then
    1.  tynames((T)E) \subseteq tynames(B)
    2.  \rea(B) |- phrase => \rea((T)E) for any realisation \rea

Proposition 3.1.10, which is essential for a proof of type-safety,
continues to hold with the rule for structure sharing added. (This is
not surprising, but important, nevertheless.)

Cheers,

Martin