From: Matthias B. <bl...@re...> - 2001-09-21 17:31:39
|
"Derek R. Dreyer" wrote: > > 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? Well, you are right, the example was not quite what I wanted it to be. (Also, see the followup to my own message.) As long as one of the two sides of the equation is still flexible, you can add a definitional spec. However, sometimes this is not the case. Moreover, when it is the case, then it forces an ordering on other things: C _must_ come before D. If there is another pair of types for which you also want equality but where the flexible type is in C, then you have a problem. You can always get it to work by applying the recursive algorithm that I outlined "by hand". But that is not very convenient, it may obscure what you are really trying to say, and it is fragile with respect to future revisions. Say D.d was defined to be some D.d' * D.d' (D.d' still being flexible). Then all you can do is express the desired type equality by saying "C.A.a = D.d'" -- which completely obscures the original purpose of saying "D.d = C.B.b" and which will break if the definition of D.d is changed to, say D.d'' * D.d'' at some later time. Anyway, I don't see what the _advantage_ of the assymetric solution is. I definitely see its disadvantages, even though others might disagree with me as to whether these disadvantages are really a big problem or not. So all else being equal, I don't see why we should not adopt a symmetric approach. Matthias > 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 > > _______________________________________________ > Sml-implementers mailing list > Sml...@li... > https://lists.sourceforge.net/lists/listinfo/sml-implementers |