[Sml-implementers] sharing vs. definitional specs

[Matthias B. <bl...@re...>]

I am still not convinced about the need for an asymetric "where type".
Consider the following scenario (which, in fact, has happened to us
in similar form, and it was a very annoying experience).

Suppose we have the following signatures A, B, C, and D:

   signature A = sig type a end

   signature B = sig type b end

   signature C = sig
      structure A : A
      structure B : B where type b = A.a * A.a
   end

   signature D = sig type d
                     val f : d -> unit
                 end

Now, suppose further that we want to construct a signature E (perhaps
the formal argument of a functor) consisting of two substructures that
match C and D, respectively:

   signature E = sig
      structure C : C
      structure D : D
   end

Further, we want to be able to apply D.f to values of type C.B.b, so
we must specify that D.d and C.B.b are the same type.  All I want to
convey to the compiler is that D.d = C.B.b, but I can't do this --
neither using "sharing" nor using "where type" because C.B.b
is not flexible anymore!  So I have to say something like:

   signature E = sig
      structure C : C
      structure D : D where type d = C.A.a * C.A.a
   end

In other words, the language forces me to trace back what C.B.b was
defined to be -- even though this information is completely
irrelevant to what I am trying to express.  Moreover, it is
intuitively clear that the compiler could infer the above automatically
from the equation D.d = C.B.b.

I see not conceptual difficulty with making "where type" (or any
type abbreviation in signatures) symmetric.  The meaning should be this:
An attempt is made to "unify" the two types in question, with currently
"flexible" type names playing the roles of type variables.

  - "unifying" two flexible type names generates a traditional sharing
    constraint for them, i.e., it throws the two names into an equivalence class
  - "unifying" a rigid type name, i.e., one that already has a definitonal
    spec, applies recursively to the RHS of its spec
  - "unifying" a flexible type name with a type constructor application
    generates a definitional spec for the name (and its equivalence class)
  - "unifying" two type constructor applications with equal head constructor
    causes the respective arguments to be "unified" recursively
  - "unifying" two type constructor applications with unequal head constructor
    causes elaboration to fail with an error message

Why can't we have this?  It seems simple and intuitive and expressive.

Matthias