make least upper bound more useful

[jmesserly]

consider:

void main() {
  var l = true ? [] : <int>[];
  l.add(42);
  print(l);
}

This l is inferred as EfficientLength

[vsmenon]

Note: we're using the analyzer's LUB computation, which follows the spec. It's not the ideal for generic types.

@stereotype441, @leafpetersen - do you know which section of the spec deals with LUB of generic types? 19.8.2 primarily deals with function types.

[stereotype441]

Section 19.8.2 is the complete definition of LUB. It only looks like it
primarily deals with function types because the definition is broken down
into cases and the case for function types is the longest. But if you look
at the first four paragraphs of 19.8.2 I believe they address all the cases
where one or both of the types is something other than a function type.

On Fri, 14 Aug 2015 at 11:02 vsmenon [email protected] wrote:

Note: we're using the analyzer's LUB computation, which follows the spec.
It's not the ideal for generic types.

@stereotype441 https://github.com/stereotype441, @leafpetersen
https://github.com/leafpetersen - do you know which section of the spec
deals with LUB of generic types? 19.8.2 primarily deals with function types.

—
Reply to this email directly or view it on GitHub
#288 (comment)
.

[leafpetersen]

I believe it's all basically section 19.8.2. The function type discussion is just the last part of that section - the first part deals with interface types (and hence implicitly generics). Consider:

class A<T> {}

What's the lub of A<int> and A<String>? The super-interfaces of A<int> are {Object}, and the super-interfaces of A<String> are {Object}. So per 19.8.2, we have that S = {Object}, and s_0 = {Object}, all of the s_i for i > 0 are empty, so the lub is Object.

It doesn't really have the expected properties of a least upper bound with respect to the subtyping relation, so it doesn't work very well for generics where the subtyping relation is richer than the super-interface relation (the set of super-types of A<int> includes A<Object>, as does the set of super-types of A<String>). It does have (by construction) nice properties like the lub being unique.

[stereotype441]

@leafpetersen the implementation in analyzer assumes that the statement "The least upper bound relation is symmetric and reflexive." (from the third paragraph of 19.8.2) takes precedence over the rest of 19.8.2. So analyzer would say that the lub of A and A is A.

I agree with your larger point, though (that it doesn't have the expected behavior when generics are involved, because it is defined in terms of super-interfaces rather than super-types).

[leafpetersen]

Edited my comment to add quotes around the generic parameters that otherwise disappear in markdown - @stereotype441 , I think that addresses your comment (please follow up again if not).

[stereotype441]

@leafpetersen Yes, that addresses my comment. Thanks.

[eernstg]

The terminology is somewhat confusing, given that it is not a least upper bound at all --- in case of a subtype graph where a least upper bound does not exist (A <: I,J and B <: I,J) we just proceed to the next level (if I <: K and J <: K it would be K) until there is no ambiguity. But it is an upper bound, and there is an algorithm, so we could call it "the standard upper bound". We could also argue that it is OK to take some upper bound which is not least, because the "leastness" is never crucial for the static analysis, nor for the runtime semantics.

However, the result is not pretty with cases like A<int> and A<String>. Since it's all about the conditional operator ?:, the need to compute this upper bound might be taken as a trigger for a hint about how the code could be adjusted such that the computation is trivial. ("Change [] to <int>[]" would do here).

[leafpetersen]

@eernstg Yes, there are two issues: one is that it is not a least upper bound, but the other is that it is not defined on the subtype graph at all, but rather on the super-interface graph (and hence doesn't consider candidates that are super-types but not super-interfaces). I actually think it is the latter issue that we are more concerned with here.

[eernstg]

OK. I think that the two topics are very tightly coupled, though, because
one main reason for not being a least upper bound is that the algorithm
jumps directly over all the supertypes which arise because of type argument
covariance.

On Fri, Aug 14, 2015 at 9:31 PM, Leaf Petersen [email protected]
wrote:

@eernstg https://github.com/eernstg Yes, there are two issues: one is
that it is not a least upper bound, but the other is that it is not defined
on the subtype graph at all, but rather on the super-interface graph (and
hence doesn't consider candidates that are super-types but not
super-interfaces). I actually think it is the latter issue that we are more
concerned with here.

—
Reply to this email directly or view it on GitHub
#288 (comment)
.

Erik Ernst - Google Danmark ApS
Skt Petri Passage 5, 2 sal, 1165 København K, Denmark
CVR no. 28866984

[leafpetersen]

Fair point. It seems to me that an equally significant issue with respect to the "leastness" though is that least upper bounds (in the usual sense) don't always exist absent the addition of intersection types for the reasons you mention above (e.g. class A and B both extend I and implement J, so both I and J are upper bounds for A and B, but neither dominates the other). I ^ J (the intersection of I and J) would be a least upper bound since I ^ J <: I and similarly for J, but neither I nor J is least.

@eernstg Do you know off the top of your head what other languages with similar subtype hierarchies do?

[eernstg]

It's not a perfect match, but
http://www.cis.upenn.edu/~bcpierce/papers/variance.pdf discusses some
decidability problems with Java, Scala, .Net and conclude that there is a
way to make them decidable. ;-)

On Mon, Aug 17, 2015 at 6:13 PM, Leaf Petersen [email protected]
wrote:

Fair point. It seems to me that an equally significant issue with respect
to the "leastness" though is that least upper bounds (in the usual sense)
don't always exist absent the addition of intersection types for the
reasons you mention above (e.g. class A and B both extend I and implement
J, so both I and J are upper bounds for A and B, but neither dominates the
other). I ^ J (the intersection of I and J) would be a least upper bound
since I ^ J <: I and similarly for J, but neither I nor J is least.

@eernstg https://github.com/eernstg Do you know off the top of your
head what other languages with similar subtype hierarchies do?

—
Reply to this email directly or view it on GitHub
#288 (comment)
.

Erik Ernst - Google Danmark ApS
Skt Petri Passage 5, 2 sal, 1165 København K, Denmark
CVR no. 28866984

[jmesserly]

moved to dart-lang/sdk#25248

[jmesserly]

actually merged into dart-lang/sdk#25821