Chromium Code Reviews
|
|
Chromium Code Reviews
Issue
1177073002:
An attempt to add generic methods to the spec. This is just a draft for purposes of evaluation and …
|
Created:
5 years, 6 months ago by gbracha Modified:
5 years, 6 months ago CC:
reviews_dartlang.org Base URL:
git@github.com:dart-lang/sdk.git@master Target Ref:
refs/heads/master Visibility:
Public. |
DescriptionAn attempt to add generic methods to the spec. This is just a draft for purposes of evaluation and experimentation. It does not entail any commitment to the feature in any particular time frame. Keep calm!
BUG=
Patch Set 1 #Patch Set 2 : sync with other spec changes #
Total comments: 35
Patch Set 3 : responses to review #Patch Set 4 : r = 0 #Patch Set 5 : s = 0 #
Total comments: 8
Messages
Total messages: 10 (2 generated)
leafp@google.com changed reviewers: + leafp@google.com
Hi Gilad - Great to see this start to get fleshed out! I put a bunch of comments inline based on an initial pass. Some high level comments: I didn't see any predicativity restrictions - I remain skeptical that the cost/benefit of going impredicative is worth it. In the absence of contra-variance we may still get decidability, but it feels like skating on thin ice, and I don't see much bang for the buck. If we go with non-prenex polymorphism, we need syntax for the types, which I think isn't addressed yet? Maybe we can chat about options here. Perhaps we should consider addressing the lack of a function type syntax as part of this. cheers, -leaf https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... File docs/language/dartLangSpec.tex (right): https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:3671: If type arguments are absent, they are taken to \DYNAMIC. s.b "to be \DYNAMIC" https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:3677: 2. If there are no type parameters ($r = 0$), any type arguments are ignored. Otherwise the number of type arguments must match the number of formal type parameters ($r = s$). s.b. ($s = 0$) ? https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:3908: the static method \code{Function.apply()} with arguments $v.g, [o_1, \ldots , o_n], \{x_{n+1}: o_{n+1}, \ldots , x_{n+k}: o_{n+k}\}, [A_1, \ldots, A_r]$. s.b "with arguments $v_g, " ? https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:3909: I think there's a small issue with expressing this in terms of Function.apply here since not all types are allowed to appear in expressions contexts (e.g. if A_1 is List<int>). This applies in the NSM case and the corresponding super call cases below as well. https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:3917: \item \code{im.typeArguments} evaluates to an immutable list with the same values as \code{[$A_1, \ldots, A_r$]}. \rationale{We need to pass the actual type arguments used to \cd{noSuchMethod}, which is why we use the $A_i$ rather than the $V_i$. If no argument were passed, the handler can choose to use \DYNAMIC{} at its discretion.} What are the $V_i$? I looked in the surrounding text but didn't find a place they were introduced, did I miss it somewhere? https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:4334: \} Is it intentional that the type parameters are dropped here? This seems wrong - why allow closurization if the types just get dropped? https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:4346: If I'm reading this correctly, neither the closurization rules nor the application rules allow for partial applications of generic functions (e.g. var intId = id<int>; where id is the polymorphic identity). Did I miss something? If not, is this intentional? My sense was that allowing this would be useful for a number of different reasons, and I don't think it substantially adds to the implementation complexity. https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:7427: \subsubsection{Generic Function Types} This is missing the treatment of assignability and more specific than, which I think become necessary if we move to a non-prenex system (as I believe this draft spec proposes). https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:7442: \rationale{ Just as an aside, I think this is a fairly natural rule from a technical perspective as well. If you take the view that subtyping is entailment, then the \forall t.\tau is naturally a subtype of \tau with \sigma substituted for t (that is, a universal entails any of its instantiations). I believe that the substitution of dynamic for the T_i essentially implements this: rather than search for the exact instantiation, we simply check that the instantiation with dynamic is a subtype. If it is, then there is * some* instantiation and we're happy. If it's not, I believe that the Dart type system is structured such that no instantiation would work. https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:7445: Even if we did not insist on the former point on principle,, there are many functions in the Dart libraries that would benefit from the use of type parameters. If these are to be changed, it is also crucial for compatibility that their callers may continue to use them without type arguments. Double comma after "principle". https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:7456: It would be extremely attractive to have this rule, allowing ordinary functions to be used where generic functions are expected. The motivation here would also be compatibility. If an existing method were converted to be generic, subclasses and implementors would no longer be valid. At the very least, their declarations would now provoke warnings. Worse, if existing uses of such APIs evolved to pass actual type arguments, the code would crash. I agree with the motivation for wanting this, but i seems to me that this is solving a short term problem (transitioning libraries to use generic method) at a long term cost to the language (surprising behavior, implementation complexity). Essentially, this rule makes the "dynamic" type definable: for any type S, \forall(T).() => T <: () => S // since S <==> dynamic (or Object) for any S () => S <: \forall(T).() => T // since S <==> Object for any S Put another way, you essentially lose all typechecking with universal types: any function type of the right arity is going to be assignable to a universal type with Object bounds. Universal types with concrete bounds will be a little more restricted. This also means that every method must be prepared to accept any number of type parameters and silently ignore them, since every method can be called as a generic method. Overall, this seems like a large cost to pay for a small benefit. It's true that it allows implementors of genericized interfaces to ignore the change (though they may still break in checked mode), but a small extra burden on the subset of library writers who don't want to use generics seems small compared to the cost of making universal types fairly meaningless as types. https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:7648: \item If I think this is wrong. It's not symmetric, and I think it gives the wrong answers. Consider finding the LUB of: \forall T <: int . int => int \forall S <: String . S => S LUB[int, String] is Object LUB[int => int, T => T] where T <: int is int => int so the LUB we compute is \forall T <: Object. int => int. But if we switch the order of the inputs, we end up using S <: String for the variable, and computing \forall S <: Object. Object => Object Unless I'm misconstruing something? I think each successive recursive LUB needs to use the LUB computed for the previously encountered bounds, rather than the original bounds. Then we have: LUB[int => int, Q => Q] where Q <: Object is Object => Object and we get a LUB which has the presumably desired property that each of the inputs is a subtype of the output, and which (at least for this example) seems to be symmetric.
PTAL. I'll send you a PDF as well. https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... File docs/language/dartLangSpec.tex (right): https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:3671: If type arguments are absent, they are taken to \DYNAMIC. On 2015/06/16 23:23:10, Leaf wrote: > s.b "to be \DYNAMIC" Done. https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:3677: 2. If there are no type parameters ($r = 0$), any type arguments are ignored. Otherwise the number of type arguments must match the number of formal type parameters ($r = s$). On 2015/06/16 23:23:10, Leaf wrote: > s.b. ($s = 0$) ? No, why? This specifically describes the semantics where any number of type arguments may be passed. https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:3908: the static method \code{Function.apply()} with arguments $v.g, [o_1, \ldots , o_n], \{x_{n+1}: o_{n+1}, \ldots , x_{n+k}: o_{n+k}\}, [A_1, \ldots, A_r]$. On 2015/06/16 23:23:10, Leaf wrote: > s.b "with arguments $v_g, " ? Done. https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:3909: On 2015/06/16 23:23:10, Leaf wrote: > I think there's a small issue with expressing this in terms of Function.apply > here since not all types are allowed to appear in expressions contexts (e.g. if > A_1 is List<int>). This applies in the NSM case and the corresponding super > call cases below as well. Yes and no. I'm not saying this is the call Function.apply(v_g, ... [A1, ..., Ar]). I'm saying the function got invoked with those values. They do exist (e.g., new List<int>().runtimeType). You can argue that the list [A1, .., Ar] isn't really valid, and I should say something like a list with the elements A1, ..., Ar in that order. But section 5 already gives license to such abuse of notation. So I think I'm in the clear. https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:3917: \item \code{im.typeArguments} evaluates to an immutable list with the same values as \code{[$A_1, \ldots, A_r$]}. \rationale{We need to pass the actual type arguments used to \cd{noSuchMethod}, which is why we use the $A_i$ rather than the $V_i$. If no argument were passed, the handler can choose to use \DYNAMIC{} at its discretion.} On 2015/06/16 23:23:10, Leaf wrote: > What are the $V_i$? I looked in the surrounding text but didn't find a place > they were introduced, did I miss it somewhere? There used to be V_i, representing the type arguments passed in practice (e.g., using dynamic when no arguments are present. I eventually centralized that in section 16.14.2 and eliminated the V_i in the process. I forgot to clean up this rationale. Will rephrase. https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:4334: \} On 2015/06/16 23:23:10, Leaf wrote: > Is it intentional that the type parameters are dropped here? This seems wrong > - why allow closurization if the types just get dropped? No, it's not intentional. It's called a bug. Fixed. https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:4346: On 2015/06/16 23:23:10, Leaf wrote: > If I'm reading this correctly, neither the closurization rules nor the > application rules allow for partial applications of generic functions (e.g. var > intId = id<int>; where id is the polymorphic identity). Did I miss something? > If not, is this intentional? My sense was that allowing this would be useful > for a number of different reasons, and I don't think it substantially adds to > the implementation complexity. Yes, that is correct. We should discuss where you find this useful. https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:7442: \rationale{ On 2015/06/16 23:23:10, Leaf wrote: > Just as an aside, I think this is a fairly natural rule from a technical > perspective as well. If you take the view that subtyping is entailment, then > the \forall t.\tau is naturally a subtype of \tau with \sigma substituted for t > (that is, a universal entails any of its instantiations). I believe that the > substitution of dynamic for the T_i essentially implements this: rather than > search for the exact instantiation, we simply check that the instantiation with > dynamic is a subtype. If it is, then there is * some* instantiation and we're > happy. If it's not, I believe that the Dart type system is structured such that > no instantiation would work. That's an interesting point. AFIK, most type systems with universal quantification and subtyping don't take this path though. Not that it matters, but do you know of counter examples? I haven't looked at this since the Java generics days. https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:7445: Even if we did not insist on the former point on principle,, there are many functions in the Dart libraries that would benefit from the use of type parameters. If these are to be changed, it is also crucial for compatibility that their callers may continue to use them without type arguments. On 2015/06/16 23:23:10, Leaf wrote: > Double comma after "principle". Done. https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:7456: It would be extremely attractive to have this rule, allowing ordinary functions to be used where generic functions are expected. The motivation here would also be compatibility. If an existing method were converted to be generic, subclasses and implementors would no longer be valid. At the very least, their declarations would now provoke warnings. Worse, if existing uses of such APIs evolved to pass actual type arguments, the code would crash. On 2015/06/16 23:23:10, Leaf wrote: > I agree with the motivation for wanting this, but i seems to me that this is > solving a short term problem (transitioning libraries to use generic method) at > a long term cost to the language (surprising behavior, implementation > complexity). > > Essentially, this rule makes the "dynamic" type definable: for any type S, > > \forall(T).() => T <: () => S // since S <==> dynamic (or Object) for any S > () => S <: \forall(T).() => T // since S <==> Object for any S > > Put another way, you essentially lose all typechecking with universal types: any > function type of the right arity is going to be assignable to a universal type > with Object bounds. Universal types with concrete bounds will be a little more > restricted. > > This also means that every method must be prepared to accept any number of type > parameters and silently ignore them, since every method can be called as a > generic method. > > Overall, this seems like a large cost to pay for a small benefit. It's true > that it allows implementors of genericized interfaces to ignore the change > (though they may still break in checked mode), but a small extra burden on the > subset of library writers who don't want to use generics seems small compared to > the cost of making universal types fairly meaningless as types. Yes, I realize it's rather costly. The choice is however, rather stark. A significant incompatibility vs. an expensive and somewhat lobotomized type system. If you view the benefit of generics as a error checking, you may find this especially disturbing. I am hardly interested in that, and much more in benefits to name completion etc. If *I* were to do generic methods, I'd go for compatibility. But I agree this is very disturbing. https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:7648: \item If On 2015/06/16 23:23:10, Leaf wrote: > I think this is wrong. It's not symmetric, and I think it gives the wrong > answers. Consider finding the LUB of: > > \forall T <: int . int => int > \forall S <: String . S => S > > LUB[int, String] is Object > > LUB[int => int, T => T] where T <: int is int => int > > so the LUB we compute is \forall T <: Object. int => int. > > But if we switch the order of the inputs, we end up using S <: String for the > variable, and computing > > \forall S <: Object. Object => Object > > Unless I'm misconstruing something? I think each successive recursive LUB needs > to use the LUB computed for the previously encountered bounds, rather than the > original bounds. Then we have: > > LUB[int => int, Q => Q] where Q <: Object is Object => Object > > and we get a LUB which has the presumably desired property that each of the > inputs is a subtype of the output, and which (at least for this example) seems > to be symmetric. Yes, the asymmetry is a problem.
brianwilkerson@google.com changed reviewers: + brianwilkerson@google.com
Initial thoughts on the grammar. I'll try implementing it soon to see whether there are any practical problems, but I don't see anything obvious. https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... File docs/language/dartLangSpec.tex (right): https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:664: {\bf formalParameterList:} It's a little hard to tell in the review tool, but it looks like there would be fewer changes to the grammar if formalParameterList stayed the same and we introduced a new genericParameterList production: genericParameterList: typeParameters? formalParameterList ; I'd also find it (a) easier to see what's changing as a result of this DEP (everything that's changed in the doc rather than everything that isn't changed in the doc) and (b) easier to read the new spec after the changes are applied (but that's just my preference and ymmv). Also, if it stays the way it is now, I think functionTypeAlias needs to be fixed to not allow two sets of type parameters. https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:3632: {\bf valueArguments:} I think the same is true here, that it would result in fewer changes that are easier to proof-read if 'arguments' stayed the same and we introduced a new genericArguments production. (In fact, if I'm counting correctly, there might only be one or two references to the new production and you might want to just inline it. But I could easily be off in my counts.)
A few more comments, thanks! https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... File docs/language/dartLangSpec.tex (right): https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:3677: 2. If there are no type parameters ($r = 0$), any type arguments are ignored. Otherwise the number of type arguments must match the number of formal type parameters ($r = s$). On 2015/06/18 20:05:58, gbracha wrote: > On 2015/06/16 23:23:10, Leaf wrote: > > s.b. ($s = 0$) ? > > No, why? This specifically describes the semantics where any number of type > arguments may be passed. I think the ($r = 0$) should be ($s = 0) because r is the number of type arguments (not the number of type parameters), and the text is referring to the number of type parameters. That is, if there are no type parameters (s = 0) then any number (r) of type arguments are allowed. No? https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:3909: On 2015/06/18 20:05:59, gbracha wrote: > On 2015/06/16 23:23:10, Leaf wrote: > > I think there's a small issue with expressing this in terms of Function.apply > > here since not all types are allowed to appear in expressions contexts (e.g. > if > > A_1 is List<int>). This applies in the NSM case and the corresponding super > > call cases below as well. > > Yes and no. I'm not saying this is the call Function.apply(v_g, ... [A1, ..., > Ar]). I'm saying the function got invoked with those values. They do exist > (e.g., new List<int>().runtimeType). You can argue that the list [A1, .., Ar] > isn't really valid, and I should say something like a list with the elements A1, > ..., Ar in that order. > > But section 5 already gives license to such abuse of notation. So I think I'm in > the clear. Ok. https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:4334: \} On 2015/06/18 20:05:59, gbracha wrote: > On 2015/06/16 23:23:10, Leaf wrote: > > Is it intentional that the type parameters are dropped here? This seems wrong > > > - why allow closurization if the types just get dropped? > > No, it's not intentional. It's called a bug. Fixed. Well you know, one man's bug is another man's feature... :) https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:4346: On 2015/06/18 20:05:58, gbracha wrote: > On 2015/06/16 23:23:10, Leaf wrote: > > If I'm reading this correctly, neither the closurization rules nor the > > application rules allow for partial applications of generic functions (e.g. > var > > intId = id<int>; where id is the polymorphic identity). Did I miss something? > > > If not, is this intentional? My sense was that allowing this would be useful > > for a number of different reasons, and I don't think it substantially adds to > > the implementation complexity. > > Yes, that is correct. We should discuss where you find this useful. My original DEP proposal used this a fair bit in the examples. Basically, I think it gives a way to reduce the syntactic noise in the absence of inference. Any place that you need to instantiate something more than once, you can easily bind the instantiation so you don't have to repeat it. It's a small thing, but the implementation cost should be very low (it's just another form of closurization) and I think it provides some nice expressiveness. https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:7442: \rationale{ On 2015/06/18 20:05:58, gbracha wrote: > On 2015/06/16 23:23:10, Leaf wrote: > > Just as an aside, I think this is a fairly natural rule from a technical > > perspective as well. If you take the view that subtyping is entailment, then > > the \forall t.\tau is naturally a subtype of \tau with \sigma substituted for > t > > (that is, a universal entails any of its instantiations). I believe that the > > substitution of dynamic for the T_i essentially implements this: rather than > > search for the exact instantiation, we simply check that the instantiation > with > > dynamic is a subtype. If it is, then there is * some* instantiation and we're > > happy. If it's not, I believe that the Dart type system is structured such > that > > no instantiation would work. > > That's an interesting point. AFIK, most type systems with universal > quantification and subtyping don't take this path though. Not that it matters, > but do you know of counter examples? I haven't looked at this since the Java > generics days. I don't know specifically with object subtyping. I think I first got this interpretation from Frank Pfenning and Rowan Davies. They were working on intersection types, and hence had a notion of subtyping and as I recall this kind of fit naturally into what they were doing. I could ping Frank about it, see if he knows anything interested and related. It's not all that different from the more standard type inference driven instantiation in practice, except that you don't need to actually produce the instantiation type - just show that there is one. The difference isn't very relevant in languages without reified types though. Of course, in languages like ML with HM type inference, you can just use a generic in a monomorphic context and it will be implicitly instantiated, so it feels awfully similar to the programmer. ML signature matching also has this property - you can ascribe a signature with a monomorphic type for a function to a structure containing a polymorphic function if it can be instantiated appropriately. The whole signature matching thing always smelled very subtyping-ish to me - not sure if there are any really good reasons it wasn't expressed that way. https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:7456: It would be extremely attractive to have this rule, allowing ordinary functions to be used where generic functions are expected. The motivation here would also be compatibility. If an existing method were converted to be generic, subclasses and implementors would no longer be valid. At the very least, their declarations would now provoke warnings. Worse, if existing uses of such APIs evolved to pass actual type arguments, the code would crash. On 2015/06/18 20:05:58, gbracha wrote: > On 2015/06/16 23:23:10, Leaf wrote: > > I agree with the motivation for wanting this, but i seems to me that this is > > solving a short term problem (transitioning libraries to use generic method) > at > > a long term cost to the language (surprising behavior, implementation > > complexity). > > > > Essentially, this rule makes the "dynamic" type definable: for any type S, > > > > \forall(T).() => T <: () => S // since S <==> dynamic (or Object) for any > S > > () => S <: \forall(T).() => T // since S <==> Object for any S > > > > Put another way, you essentially lose all typechecking with universal types: > any > > function type of the right arity is going to be assignable to a universal type > > with Object bounds. Universal types with concrete bounds will be a little > more > > restricted. > > > > This also means that every method must be prepared to accept any number of > type > > parameters and silently ignore them, since every method can be called as a > > generic method. > > > > Overall, this seems like a large cost to pay for a small benefit. It's true > > that it allows implementors of genericized interfaces to ignore the change > > (though they may still break in checked mode), but a small extra burden on the > > subset of library writers who don't want to use generics seems small compared > to > > the cost of making universal types fairly meaningless as types. > > > Yes, I realize it's rather costly. The choice is however, rather stark. A > significant incompatibility vs. an expensive and somewhat lobotomized type > system. If you view the benefit of generics as a error checking, you may find > this especially disturbing. I am hardly interested in that, and much more in > benefits to name completion etc. If *I* were to do generic methods, I'd go for > compatibility. But I agree this is very disturbing. Fair enough. I obviously fall in the error checking camp, and it does blow a pretty big hole in the system. A possible compromise would be to only allow this in method overriding (where most of the incompatibility is), but that feels kind of ad hoc. https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:7648: \item If On 2015/06/18 20:05:59, gbracha wrote: > On 2015/06/16 23:23:10, Leaf wrote: > > I think this is wrong. It's not symmetric, and I think it gives the wrong > > answers. Consider finding the LUB of: > > > > \forall T <: int . int => int > > \forall S <: String . S => S > > > > LUB[int, String] is Object > > > > LUB[int => int, T => T] where T <: int is int => int > > > > so the LUB we compute is \forall T <: Object. int => int. > > > > But if we switch the order of the inputs, we end up using S <: String for the > > variable, and computing > > > > \forall S <: Object. Object => Object > > > > Unless I'm misconstruing something? I think each successive recursive LUB > needs > > to use the LUB computed for the previously encountered bounds, rather than the > > original bounds. Then we have: > > > > LUB[int => int, Q => Q] where Q <: Object is Object => Object > > > > and we get a LUB which has the presumably desired property that each of the > > inputs is a subtype of the output, and which (at least for this example) seems > > to be symmetric. > > Yes, the asymmetry is a problem. I think a reasonable definition might be to define it inductively: If $F = \forall P_1 <: B_1, \ldots, P_n <: B_m. fsig$ $G = \forall Q_1 <: C_1, \ldots, Q_n <: C_m. gsig$ then the least upper bound of $F$ and $G$ is the least upper bound of $F = \forall P_2 <: B_2, \ldots, P_n <: B_m. fsig$ and $[P_1/Q_1]\forall Q_2 <: C_2, \ldots, Q_n <: C_m. gsig$ with the bound of $P_1$ set to $L_1$ where $L_1$ is the least upper bound of $B_1$ and $[P_1/Q_1]C_1$ with the obvious base case when $n=0$. WDYT?
Looks like my previous batch of changes wasn't uploaded before. It now matches the PDF I sent Leaf. Let's plan on a meeting this week, and a meeting with Lars next week. https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... File docs/language/dartLangSpec.tex (right): https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:664: {\bf formalParameterList:} On 2015/06/21 23:32:02, Brian Wilkerson wrote: > It's a little hard to tell in the review tool, but it looks like there would be > fewer changes to the grammar if formalParameterList stayed the same and we > introduced a new genericParameterList production: > > genericParameterList: > typeParameters? formalParameterList > ; > > I'd also find it (a) easier to see what's changing as a result of this DEP > (everything that's changed in the doc rather than everything that isn't changed > in the doc) and (b) easier to read the new spec after the changes are applied > (but that's just my preference and ymmv). > > Also, if it stays the way it is now, I think functionTypeAlias needs to be fixed > to not allow two sets of type parameters. We can certainly do that. I don't want to worry about that too much right now, because we need to fix the basics of the proposal and get a go/nogo decision very soon. https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:3677: 2. If there are no type parameters ($r = 0$), any type arguments are ignored. Otherwise the number of type arguments must match the number of formal type parameters ($r = s$). On 2015/06/23 01:59:59, Leaf wrote: > On 2015/06/18 20:05:58, gbracha wrote: > > On 2015/06/16 23:23:10, Leaf wrote: > > > s.b. ($s = 0$) ? > > > > No, why? This specifically describes the semantics where any number of type > > arguments may be passed. > > I think the ($r = 0$) should be ($s = 0) because r is the number of type > arguments (not the number of type parameters), and the text is referring to the > number of type parameters. That is, if there are no type parameters (s = 0) > then any number (r) of type arguments are allowed. No? Yes. I thought r = 0 was supposed to replace r = s and was puzzled. Should have looked higher up. https://codereview.chromium.org/1177073002/diff/20001/docs/language/dartLangS... docs/language/dartLangSpec.tex:4346: On 2015/06/23 02:00:00, Leaf wrote: > On 2015/06/18 20:05:58, gbracha wrote: > > On 2015/06/16 23:23:10, Leaf wrote: > > > If I'm reading this correctly, neither the closurization rules nor the > > > application rules allow for partial applications of generic functions (e.g. > > var > > > intId = id<int>; where id is the polymorphic identity). Did I miss > something? > > > > > If not, is this intentional? My sense was that allowing this would be > useful > > > for a number of different reasons, and I don't think it substantially adds > to > > > the implementation complexity. > > > > Yes, that is correct. We should discuss where you find this useful. > > My original DEP proposal used this a fair bit in the examples. Basically, I > think it gives a way to reduce the syntactic noise in the absence of inference. > Any place that you need to instantiate something more than once, you can easily > bind the instantiation so you don't have to repeat it. It's a small thing, but > the implementation cost should be very low (it's just another form of > closurization) and I think it provides some nice expressiveness. Ok, we can discuss.
A couple more comments based on another read through of the latest. https://codereview.chromium.org/1177073002/diff/80001/docs/language/dartLangS... File docs/language/dartLangSpec.tex (right): https://codereview.chromium.org/1177073002/diff/80001/docs/language/dartLangS... docs/language/dartLangSpec.tex:650: A function may be generic, in which case it also has formal type parameters \ref{generics}. The scope of these includes the formal parameter scope and the body scope of the function, as described in section \ref{generics}. Scope includes the return type too. https://codereview.chromium.org/1177073002/diff/80001/docs/language/dartLangS... docs/language/dartLangSpec.tex:3886: One in which parametrically polymorphic function types are subtypes of non-parametrically polymorphic ones, and one in which they are not. The commentary reflects the former, as it is more compatible, though harder to implement. " One in which parametrically polymorphic function types are subtypes of non-parametrically polymorphic ones, and one in which they are not. " I think this is backwards - we always allow universals to subtype non-universals. The question is whether we allow non-universals to subtype universals. https://codereview.chromium.org/1177073002/diff/80001/docs/language/dartLangS... docs/language/dartLangSpec.tex:7657: $L_i$ is the least upper bound of $[R_j/P_j]_{j=1}^{i}B_i$ and $[R_j/Q_j]_{j=1}^{i}C_i, i \in 1..n$ and $lsig$ is the least upper bound of $[R_i/P_i]fsig$ and $[R_i/Q_i]gsig$. I think there's still a small problem here at the boundary: in computing the LUB for B_i and C_i, what is the bound for R_i? This formulation either implies some sort of horrible fixed point (finding L_i uses L_i as the bound on R_i while computing L_i), or else uses no bound? I think that while computing L_i, the bound to use should be B_i, given the covariant rule. So this would suggest: the least upper bound of $F$ and $G$ is $\forall R_1 <: [R_1/P_1]L_1, \ldots, R_n <: [R_n/P_n]L_n. lsig$ where $L_i$ is the least upper bound of $[R_j/P_j]_{j=1}^{i-1}B_i$ and $[R_j/Q_j]_{j=1}^{i-1}[P_i/Q_i]C_i, i \in 1..n$ and $lsig$ is the least upper bound of $[R_i/P_i]fsig$ and $[R_i/Q_i]gsig$. Or perhaps better: the least upper bound of $F$ and $G$ is $\forall R_1 <: L_1, \ldots, R_n <: L_n. lsig$ where $L_i$ is $[R_i/P_i]M_i$ and $M_i$ is the least upper bound of $[R_j/P_j]_{j=1}^{i-1}B_i$ and $[R_j/Q_j]_{j=1}^{i-1}[P_i/Q_i]C_i, i \in 1..n$ and $lsig$ is the least upper bound of $[R_i/P_i]fsig$ and $[R_i/Q_i]gsig$.
Some suggestions about where to put the restrictions on type arguments to stop universal types from being instantiated with other universal types. Not sure if I caught all of them, or if there might not be a more central location to unify them in? https://codereview.chromium.org/1177073002/diff/80001/docs/language/dartLangS... File docs/language/dartLangSpec.tex (right): https://codereview.chromium.org/1177073002/diff/80001/docs/language/dartLangS... docs/language/dartLangSpec.tex:2193: A type parameter $T$ may be suffixed with an \EXTENDS{} clause that specifies the {\em upper bound} for $T$. If no \EXTENDS{} clause is present, the upper bound is \code{Object}. It is a static type warning if a type parameter is a supertype of its upper bound. The bounds of type variables are a form of type annotation and have no effect on execution in production mode. It is a static warning if the bound of a type parameter is a universal type. https://codereview.chromium.org/1177073002/diff/80001/docs/language/dartLangS... docs/language/dartLangSpec.tex:3683: Otherwise, $r = s$, then each formal type parameter is bound to the corresponding type argument. Generic restriction: If A_i is a universal type, then it is replaced with \DYNAMIC. https://codereview.chromium.org/1177073002/diff/80001/docs/language/dartLangS... docs/language/dartLangSpec.tex:3897: Generic restriction: If A_i is a universal type, then it is replaced with \DYNAMIC. https://codereview.chromium.org/1177073002/diff/80001/docs/language/dartLangS... docs/language/dartLangSpec.tex:4009: Generic restriction: If A_i is a universal type, then it is replaced with \DYNAMIC. https://codereview.chromium.org/1177073002/diff/80001/docs/language/dartLangS... docs/language/dartLangSpec.tex:7549: Let $T$ be a parameterized type $G<S_1, \ldots, S_n>$. If $G$ is not a generic type, the type arguments $S_i$, $1 \le i \le n$ are discarded. If $G$ has $m \ne n$ type parameters, $T$ is treated as as a parameterized type with $m$ arguments, all of which are \DYNAMIC{}. Restriction on generic parameters: If S_i is a universal type, then it is treated as if it were dynamic (and a static warning is issued). |
