Re: [Sml-implementers] sharing vs. definitional specs

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

I don't understand the problem with using where type in your example.  Define
signature E as follows:

signature E = sig
  structure C : C
  structure D : D where type d = C.B.b
end

This is precisely an example of where a symmetric sharing constraint doesn't
work but an asymmetric where type constraint works fine.  Where type allows you
to introduce a type sharing between a flexible type in the signature and *any
other type* in the context of the signature.  Am I missing something here?

Derek

Matthias Blume wrote:
> 
> 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
> 
> _______________________________________________
> Sml-implementers mailing list
> Sml...@li...
> https://lists.sourceforge.net/lists/listinfo/sml-implementers