"Enhanced Type Promotion" informal proposal. #29624

munificent · 2017-05-16T00:07:58Z

This is the proposal and tracking issue to improve the language's type promotion rules to allow promotion to apply in more places.

@bwilkerson

floitschG · 2017-05-18T09:25:20Z

docs/language/informal/enhanced-type-promotion.md

+
+*   A logical or expression `e` like `e1 || e2` shows that `v` has type T if
+    either `e1` or `e2` shows that when they are false if `e` itself is false.
+    For example, in `o is String || itsMonday`, we know `o` must be a String if


o is! String
@johnniwinther

floitschG · 2017-05-18T09:27:51Z

docs/language/informal/enhanced-type-promotion.md

+
+*Optional: We could expand the definition of complete normally for a block to
+allow for returns or throws before the last statement as long as they are
+unconditionally executed.*


We should. The following statements should not be treated differently, just because I had to add a block to make the code fit into 80 chars.

if (e) return foo; if (e) { return foo; }

Adding curly braces is a style issue.

@johnniwinther

Those two are actually equivalent with the wording above because the return is the last statement of the block.

floitschG · 2017-05-18T09:29:22Z

docs/language/informal/enhanced-type-promotion.md

+  v = someNonTValue;
+  // v has the non-promoted type here
+}
+```


Would be good to have.

A common pattern is:

Value v = ... if (v is ProxyValue) { v = v.value; }

@johnniwinther

one of the "stupidities" of the current system is that it blows up if you have any assignment, even if the assignment is after the use-point.
I know that evaluation-order may be tricky (which is a good reason to fix the evaluation order as we are discussing elsewhere), and it basically amounts to abstract interpretation, but it would also be very useful.

Yeah, I think this is super important. The pattern you note Florian is really common, especially with parameters.

If we all think that this is important, we should not make it optional.

I believe the current proposal already covers this case. The wording ("same type") in the beginning wasn't clear, but the example was analogous to this one. The proposed spec language was precise on this already.

I updated the wording to be clear that "same type" means the same as the promoted type.

This doesn't, I think, require abstract interpretation or changing the type of a variable after the assignment.

floitschG · 2017-05-18T09:32:44Z

docs/language/informal/enhanced-type-promotion.md

+    It depends on whether the function passed to `stringLength()` calls the
+    closure that is passed to it. To avoid cases like this, the spec defines
+    certain variables to be off limits for type promotion.
+


There is the 4th dimension: what type can be promoted (and how).

For example:

Iterable<String> x = ...; if (x is List) { ... }

If we reduce the promotion to simple cases with only one constraint, then almost all cases are covered, and most users would be much happier. Dart2js seems to have some work in it.

@johnniwinther

I didn't follow this. What do you mean by "constraint"?

In this case, it's pretty clear, that we want to promote the Iterable<String> to a List<String>. However, the type promotion doesn't even try to.
The following example is currently invalid:

Iterable<int> foo() { return [1, 2]; } main() { Iterable<int> x = foo(); if (x is List) { print(x[0] + 3); } }

@johnniwinther (correctly) stated that this is a 4th dimension in this list.

OK, added some verbiage around this.

lrhn · 2017-05-18T10:21:35Z

docs/language/informal/enhanced-type-promotion.md

+*   A rethrow statement
+*   An expression statement whose expression is a throw expression
+*   An if statement with an else where neither statement can complete normally
+*   A block whose last statement cannot complete normally


We might want to emphasize that a labeled block statement is not a block statement (it's a labeled statement, and might contain a break to the label - we can also statically determine if it does contain a break to the label, but there is no other reason to have a labeled block, so let's just assume that it does.

lrhn · 2017-05-18T10:25:07Z

docs/language/informal/enhanced-type-promotion.md

+*   A rethrow statement
+*   An expression statement whose expression is a throw expression
+*   An if statement with an else where neither statement can complete normally
+*   A block whose last statement cannot complete normally


No break or continue?
I know they are delimited, but so are throws (by try/catch), and the limit can always be found statically for break and continue.

I guess I'm angling for a proper (function-local) control flow analysis, and not more ad hocery.

I would like full control flow analysis too, eventually. But I'd like to not go there yet because that's going to be a lot of work. Can we stick with a smaller subset that covers the common cases in this proposal and then refine it later?

I think we will end up revisiting promotion anyway to handle non-nullable types and possible intersection and union types. That would be a good time to do the full flow analysis.

lrhn · 2017-05-18T10:32:28Z

docs/language/informal/enhanced-type-promotion.md

+
+*Optional: We could expand the definition of complete normally for a block to
+allow for returns or throws before the last statement as long as they are
+unconditionally executed.*


Agree, we should say: A block statement where any of its statements cannot complete normally. The remaining statements would be dead code, but there is no reason to be more stupid than necessary in the presence of dead code.

Agreed. Done.

lrhn · 2017-05-18T10:33:27Z

docs/language/informal/enhanced-type-promotion.md

+
+*Optional: We could expand the definition of complete normally for a block to
+allow for returns or throws before the last statement as long as they are
+unconditionally executed.*


Those two are actually equivalent with the wording above because the return is the last statement of the block.

lrhn · 2017-05-18T10:35:49Z

docs/language/informal/enhanced-type-promotion.md

+```
+
+Here, since `trim()` returns a String, the assignment of `o` to its result does
+not disable its promotion.


Allowing promotion precisely in the case where you assign the same type again feels ad-hoc.
It's basically saying that we trust the assignment, but we only allow it to promote to something we know already.

How about trusting assignments enough to actually let them promote
the variable in all cases, to the type actually being assigned?

Consider:

foo(Object o) { o.length; // Should have error! o = "string now"; o.length; // This would be OK. }

If we allow assignment promoting to other types, then we need to split the scope at each assignment so that we don't promote until after the assignment. That's reasonable, but I think it would make this proposal quite a bit more complex.

I do think we want to get there eventually, but I'm hoping to not do so yet. I'd rather defer the interesting flow-sensitive analysis later and try to do it holistically. This proposal is more about what's the minimal amount we can do shortly so that we can eliminate the ad-hoc type propagation that analyzer is doing?

Is that OK?

Analyzer's type propagation currently re-assigns the type on assignment (though without the limitations used by promotion). It appears (based on issues opened) to be one of the most confusing aspects of promotion for most users. Perhaps the extra limitations would negate the confusion, but be aware that we've previously run into issues related to this.

Thanks, that's useful to keep in mind.

lrhn · 2017-05-18T10:38:50Z

docs/language/informal/enhanced-type-promotion.md

+  v = someNonTValue;
+  // v has the non-promoted type here
+}
+```


one of the "stupidities" of the current system is that it blows up if you have any assignment, even if the assignment is after the use-point.
I know that evaluation-order may be tricky (which is a good reason to fix the evaluation order as we are discussing elsewhere), and it basically amounts to abstract interpretation, but it would also be very useful.

lrhn · 2017-05-18T10:43:59Z

docs/language/informal/enhanced-type-promotion.md

+    after the if statement in the immediately enclosing block.
+
+    This is also allowed if the if statement has no else clause at all.
+


I would really like the statement x as T; to promote x to T.
It's basically equivalent to (x is T) ? x : throw new CastError() which:

promotes x to T in the true branch, and

cannot complete normally in the false branch.
Any expression or statement that is down-flow from this can trust that x is T.

I'm not opposed to that, but we're trying to keep this proposal small and incremental so that we can get it done in a reasonable amount of time. We'd like to get rid of analyzer's special type propagation code as soon as possible.

Do you think the as case comes up enough to warrant adding it now? I can't recall running into it.

It doesn't come up because it doesn't help you right now, but I expect that it would be useful if it causes type promotion, as an assertion-like promotion syntax.

Compare:

_foo(Object x) { assert(x is Foo); // no promotion ... } _bar(Object x) { Foo fooX = x; // unnecessary new name ... } _baz(Object x) { if (x is! Foo) throw ... something; // Long an cumbersome ... } _qux(Object x) { x as Foo; ...; // Type promotion of x, short and convenient. }

We could even say that covariant desugars into an initial x as Type; statement.

So, not necessary, but I think it will be very convenient, so at least keep it in mind.

I'll definitely keep it in mind.

I also think x as Type would cover a very practical set of situations concisely. However, it is an example of the "after" semantics that I'd like to push a little bit further into the future, such that we can get the simple cases done now.

lrhn · 2017-05-18T10:47:34Z

docs/language/informal/enhanced-type-promotion.md

+*   an expression statement whose expression is a throw expression,
+*   an if statement of the form if (b) s1 else s2 where neither s1 nor s2 can
+    complete normally, or
+*   a block whose last statement cannot complete normally.


(Or a do-while statement where the body cannot complete normally, but it's probably ridiculous enough that we shouldn't care).

lrhn · 2017-05-18T10:48:05Z

docs/language/informal/enhanced-type-promotion.md

+*   an expression statement whose expression is a throw expression,
+*   an if statement of the form if (b) s1 else s2 where neither s1 nor s2 can
+    complete normally, or
+*   a block whose last statement cannot complete normally.


Again, I'd add a break or continue statement.

I'm up for that, though I worry about how break/continue to a label interferes with this. @bwilkerson, do you think we should add this?

I chose not to add it to the original proposal because (a) I wanted to keep this as simple as possible, (b) I don't think that case occurs frequently, and (c) it isn't necessary to add all possible enhancements at this point.

I'd leave it out for now, unless adding it will allow us to get this approved more quickly :-)

If we just go for break, it should be safe, as long as we never consider labeled statements to not complete normally.

The only complication I can see is that a block-statement that is the body of a loop can complete normally if it contains a continue. We need to handle that anyway, because that applies even if the last statement of the block is a return:

while (x is! T) { if (test) continue; if (otherTest) break; return 42; } // x is T?

(I don't remember if we do the contra-indicated promotion on while loops the same way as on if statements, but if we do, this is a problem. It's also a problem that can be easily solved by statically checking if the loop contains a break or continue targeting it).

Apart from loop bodies, there is not problem. A break or continue always terminate the current block, just like a throw. If a loop, switch or try statement is never considered not completing normally, then having control flow going to them from unpredictable places is not a problem.

I don't remember if we do the contra-indicated promotion on while loops the same way as on if statements, but if we do, this is a problem.

The proposal doesn't go for that and, anecdotally, I don't think it comes up too often in practice.

- Fix typo in example. - Clarify that labeled statements are not supported. - Allow statements that cannot complete normally anywhere in the block.

leafpetersen · 2017-05-24T20:25:54Z

docs/language/informal/enhanced-type-promotion.md

+
+    ```dart
+    if (o is String) {
+      o = 123; // Not a string anymore!


Just a thought, but should we really not promote o here? I suspect that the original argument was that promotion should not introduce errors, only eliminate them. But we're already changing that by allowing promotion from dynamic. So maybe we should just allow in scope re-assignments, and let the chips fall where they may. The code above becomes an error.

See my comment above. I'd like to go here eventually, but probably not in this proposal.

Sure. Note though that I'm not really suggesting the same thing that you addressed in your comment above: I'm not suggesting promoting based on the assignment, I'm suggesting just allowing promotion (from the is test) even if there is an assignment, and then allowing the assignment to become an error if it changes the type.

I think that's a much easier semantic to explain to users than either (a) allowing the type to change after an assignment (the current analyzer propagation model) or (b) splitting the scope so that it has a promoted type in some of the code but not in other code. It would be interesting to run an analysis to figure out how much code would be effected by that change in semantics.

lrhn · 2017-05-31T07:43:09Z

docs/language/informal/enhanced-type-promotion.md

+
+*   A block that directly contains a statement that cannot complete normally.
+
+We do not allowed *labeled* statements of the above form. Fortunately, labels


"do not allowed" -> "do not allow"
... but I'm still not sure what that means. Who allows what to do what?
Maybe:
"Notice that this does not include a labeled block statement, or a loop statement with a block body, only the block statement itself."

I really think we should include break/continue as well:

for (var object in objects) { if (object is! Future) { print(object); continue; } object.then(print); }

How do we explain that this doesn't work but replacing continue with return does. That is an inconsistency that we have to explain, where "if execution of the positive-test branch will definitely not reach the end of the after the i, then the following code is considered to be on the negative test-branch."

stereotype441 · 2017-06-02T20:36:26Z

docs/language/informal/enhanced-type-promotion.md

+```dart
+while (o is String) oPromotedToStringHere;
+
+for (; o is String;;) oPromotedToStringHere;


Nit: extra ;.

Question: should o be promoted within the increment part of the for-loop? E.g.:

for (; o is String; oPromotedToStringHere) ...;

If an assignment in the loop body doesn't nullify the promotion then, yes, it seems to me like it should.

@bwilkerson?

I don't have any problem with promoting o in the update. I'm not sure whether this pattern occurs much (I don't recall seeing it before), but it won't hurt anything to add it. But again, I'm less concerned with covering every possible case than with covering the most common cases.

stereotype441 · 2017-06-02T20:47:37Z

docs/language/informal/enhanced-type-promotion.md

+*   An if statement with an else where neither statement can complete normally.
+
+*   A block that directly contains a statement that cannot complete normally.
+


The prototype I experimented with actually covers more cases than this, kind of by accident, e.g. it can tell that the following contrived statement does not complete normally:

if (x is int && throw ...) { print('hello'); } else { return; }

The reason is because it treats "cannot complete normally" another kind of fact, tracked in the same way as the facts indicating that a variable has a certain type (I use the term "unreachable" in my prototype code). Specifically, the reasoning looks like this:

Before x is int, nothing is known.

After x is int, if x is int evaluated to true, x is known to have type int. Otherwise nothing is known.

Before throw, x is known to have type int.

After throw ..., x is known to have type int, and this code path is unreachable.

After x is int && throw ..., if x is int && throw ... evaluated to true, x is known to have type int, and this code path is unreachable. Otherwise nothing is known.

Before the evaluation of print('hello');, x is known to have type int, and this code path is unreachable.

After the evaluation of print('hello');, x is known to have type int, and this code path is unreachable.

Before the evaluation of return;, nothing is known.

After the evaluation of return;, the code path is unreachable.

Therefore, since both branches of the if statement result in an unreachable code path, the code is unreachable after the if statement.

Would you consider the implementation to conform to the spec if its flow control analysis is more sophisticated than what's above, or does it need to match it exactly?

My personal opinion is that the specification and the implementation need to agree, because without that I believe that it becomes confusing to users. That could mean updating the spec to match the implementation, or vice versa.

Yeah, I think it should match.

I would be up for updating the proposal to match what you describe here. I like the idea of having a unified fact formalism that covers both flavors of facts, and I think tracking reachability at the expression level will end up being useful.

What do you think, @bwilkerson? I'll have to do some homework first, but I could try to sketch out some informal prose to define reachability like @stereotype441 describes.

Incidentally, my prototype was inspired by definite assignment analysis, so if you're going to sketch out an informal proposal I'd recommend using definite assignment analysis as a starting point. I took some shortcuts in the presence of loops to avoid the need to compute a fixed point.

Note that the current (Dart 1.0) type promotion rules can all be re-cast into a definite assignment style framework without changing the current semantics, so if we updated the spec to use a definite assignment style framework we would be able to start adding type promotion features by making parallel incremental changes both in the spec and in the front end implementation.
I think that would be really desirable.

I can give you more details about my prototype algorithm any time--let me know if you want to set up a meeting.

IIRC, Lasse was advocating the same thing in the original doc. My only concern then, as now, is the complexity that might add. My primary concern is that this needs to be comprehensible to users (who are not language designers). That said, if you want to take a stab at writing something up that will give us a concrete example to look at to judge the comprehensibility of what it would require.

(IIRC, the original proposal was that every statement and expression have text added of the form: "This construct completes normally if ...", thus defining the notion recursively. Not sure whether that's the most readable form. I think the Java spec has a separate chapter on the subject just to bring all of the parts of the definition closer together.)

Just to clarify, "same thing" did not mean "definite assignment analysis" when I typed it; it meant "reachability analysis".

Paul, I think your approach is very promising! Also, it would be very helpful to have an analysis which is at this (high) level of detail. That'll take care of a large and meaningful portion of all those situations where developers could go "but it obviously has that type, so why can't my IDE understand that?!".

In general, we can express the analysis in many ways. But in the end it must be some sound approximation of an explicit control flow analysis:

The code is organized into basic blocks connected by edges (corresponding to the different kinds of completion), and any particular property (such as "v has type T") is known to hold in a given node N if all paths to N pass through a node or edge where that property is established, and the property isn't destroyed in any node on the path up to N.

I believe that your analysis, Paul, essentially gathers information about all known valid properties of interest, e.g., things like "v is T was true" & "v is T was false, but no path exists from that situation to the current point". That may be a little twisted (why not just forget about things happening on non-existing paths?), but it sounds like it would work.

However, we should consider taking one step dealing with simple scopes (whenever something is known to hold in a complete {} delimited block), and then in a later step (both for implementation and specification) to add the complex scopes (whenever something is known to hold in a different subset of the code, e.g., it holds "after" a specific point, because all other paths to that area do not exist).

stereotype441 · 2017-06-02T20:58:58Z

docs/language/informal/enhanced-type-promotion.md

+*   the variable v is promotable in u, and
+*   c shows that v has the type T when true,
+
+then v is known to have type T in u.


Note that depending on how we handle assignments, this might get tricky since u executes after s. For example, if we allow an assignment to un-do a promotion, then an assignment to v somewhere in s will also need to un-do the promotion in u. For example, we need to ensure that an error is reported for:

for (var x = 0; x is int; x++) { x = 'whoops'; }

stereotype441 · 2017-06-02T20:59:12Z

docs/language/informal/enhanced-type-promotion.md

+
+### 17.6.1 For Loop
+
+Given a for statement of the form for (..., c, ...) s, if


Nit: these commas should be semicolons.

stereotype441 · 2017-06-02T21:55:42Z

docs/language/informal/enhanced-type-promotion.md

+
+*   v cannot be potentially mutated within S unless all of the types of the
+    values that would be assigned to v within S are a subtype of the promoted
+    type of v,


I think this is undecidable in general. For instance, consider:

if (x is T) { x = f(x); }

Is x promoted within the block? To answer that we need to know whether f(x) evaluates to a subtype of T. If f is a generic function, then to answer that question we need to perform type inference on f(x), which requires knowing the type of x. To know the type of x, we need to know whether it is promoted within the block. So we are at an impasse.

The two bullet points that follow this one have similar problems.

😧

You're exactly right. Digging into it, I managed to come up with this fun one:

T fn<T, T>(T t, T t) => t; class A { D v; } class B extends A { E2 v; } class C extends B {} class D { A a; } class E1 extends D { C a; } class E2 extends D {} foo(A x) { if (x is B) { var y = x.v; if (y is E1) { x = fn(y.a, new B()); } } }

Here, if we allow the promotion of x to B, then it kills the promotion of y to E1. If we allow the promotion of y to E1, it kills the promotion of x to B. So there's stable solutions where either x or y is promoted (but not both) and the choice is arbitrary. At least, I think that's how it works.

I'd hate for the perfect to be the enemy of the good and go back to making all assignments kill promotion when in most cases, the assignment is innocuous and doesn't depend on or affect inference. But I'm stumped as to how we can identify "safe" and "unsafe" assignments without using any type analysis on the RHS.

Any ideas?

@leafpetersen @bwilkerson

The basic problem is the definition of scope. In Guarded Type Promotion (see section 4, rule for assignment) the scope extends until the first assignment, and a 'reduced' promotion after the assignment.

This allows for continued promotion after assignment if the assignment upholds the promotion. For instance

if (x is String) { x = x.trim(); // promotion is continued since .trim() returns String x = x.length; // promotion is terminated since .length has type int }

In the example above x is promoted to B until the assignment - or even after the assignment if we solve the orthogonal question of which pairs of types that can be promoted (component 4); can we promote y to E1&E2 or to E1 since it was only inferred to be E2.

I worry (and I think Brian has evidence to support it) that changing (by demoting or refining) the type on assignment leads to a more confusing user experience, even if we sidestep intersection types.

For now, at least, I like Leaf's suggestion of having the assignment simply not change the type. Instead, we type check the assigned value against the variable's (now promoted) type and report an error as usual if that's not valid. So, in your example, you'd get an error on x = x.length because you're trying to assign an int to a variable of (promoted) type String.

I don't think having only one type for a variable is "good enough", we will need to have something similar to intersection types ("multiple independent known types") in order to not look too stupid.
If I do if (x is C) { x.methodFromC(); } it shouldn't fail. If we can only promote to subtypes of the previously known type, then it can fail if C is an unrelated type.

I know that it's tempting to go for "the simplest thing that could work", but that's what got us where we are now (a promotion system that users rightly find mindbogglingly stupid).
The rules are pretty simple, it's the exceptions that hurt, so I want to remove exceptions. An is-test should always promote a local variable, without exception. (I'd even argue that it should promote other things than local variables, but that's more tricky).
That means promoting even if the type is unrelated to the static type or other currently known types, because that's easier than explaining to the user when it works and when it doesn't.
For the same reason, I want to be able to know multiple independent types, because there is no good unification of independent types, but the user is able to "know" that x is both B and C.
If one of B and C is more specific than the other, we can unify them, but we should be able to handle the case where we can't.

- Add a section on which pairs of types allow promotion. - Clarify that assignment is allowed if the RHS is the same as the *promoted* type. - Fix some typos. - Go ahead and code format the proposed spec language. This doesn't address the problem Paul raised about assignment. Not sure what to do with that yet.

johnniwinther · 2017-06-07T10:44:41Z

docs/language/informal/enhanced-type-promotion.md

+4.  **Which pairs of types -- declared and promoted -- are allowed for
+    promotion.** The spec says that promotion only applies if the promoted type
+    is a subtype of the declared type.
+


The spec says more specific, not subtype. This is why you cannot promote Iterable<String> to List. In simple cases, like this one, there is only one way for a List to be an Iterable<String>, namely a List<String> thus promoting to List<String> would avoid the need for an intersection type (Iterable<String>&List) in this case.

The spec says more specific, not subtype.

I think that's the 1.0 spec, but for strong mode / 2.0, I believe the intent is to change it to subtype. Is that right, @leafpetersen?

Clarify that when that happens, the assignment is checked (statically and dynamically for implicit downcasts) against the promoted type.

eernstg

We discussed this a long time ago, but I promised to take a fresh look at the document.

In general, I think it looks fine. The main issue I can see is that the notion of being "after" some piece of code is complex and somewhat ad-hoc. I really like Paul's approach, but we need to specify it, and I'd recommend that we consider enhancing promotion in two steps: (1) specify and implement simple scopes of promotion ({.. "x promoted here" ..}) and (2) specify and implement irregular scopes of promotion (where propotion takes place "after" some point where it is guaranteed that v is T because all other situations would force a non-normal completion).

eernstg · 2017-07-04T16:49:10Z

docs/language/informal/enhanced-type-promotion.md

+}
+```
+
+Without type promotion, the marked line would have a static error since Object


'error': In strong mode, otherwise a static warning (that distinction is made explicit later on).

eernstg · 2017-07-04T17:27:35Z

docs/language/informal/enhanced-type-promotion.md

+*   An if statement with an else where neither statement can complete normally.
+
+*   A block that directly contains a statement that cannot complete normally.
+


Paul, I think your approach is very promising! Also, it would be very helpful to have an analysis which is at this (high) level of detail. That'll take care of a large and meaningful portion of all those situations where developers could go "but it obviously has that type, so why can't my IDE understand that?!".

In general, we can express the analysis in many ways. But in the end it must be some sound approximation of an explicit control flow analysis:

The code is organized into basic blocks connected by edges (corresponding to the different kinds of completion), and any particular property (such as "v has type T") is known to hold in a given node N if all paths to N pass through a node or edge where that property is established, and the property isn't destroyed in any node on the path up to N.

I believe that your analysis, Paul, essentially gathers information about all known valid properties of interest, e.g., things like "v is T was true" & "v is T was false, but no path exists from that situation to the current point". That may be a little twisted (why not just forget about things happening on non-existing paths?), but it sounds like it would work.

However, we should consider taking one step dealing with simple scopes (whenever something is known to hold in a complete {} delimited block), and then in a later step (both for implementation and specification) to add the complex scopes (whenever something is known to hold in a different subset of the code, e.g., it holds "after" a specific point, because all other paths to that area do not exist).

eernstg · 2017-07-04T17:30:51Z

docs/language/informal/enhanced-type-promotion.md

+    after the if statement in the immediately enclosing block.
+
+    This is also allowed if the if statement has no else clause at all.
+


I also think x as Type would cover a very practical set of situations concisely. However, it is an example of the "after" semantics that I'd like to push a little bit further into the future, such that we can get the simple cases done now.

eernstg · 2017-07-04T17:32:18Z

docs/language/informal/enhanced-type-promotion.md

+An even nastier example is:
+
+```dart
+T fn<T, T>(T t, T t) => t;


This one certainly won't work (the two type variables have clashing names, and so do the two value parameters). It's not quite obvious to me what was intended, but I'll assume T fn<T>(T t1, T t2) => random ? t1 : t2.

eernstg · 2017-07-04T17:33:50Z

docs/language/informal/enhanced-type-promotion.md

+class C extends B {}
+
+class D            { A a; }
+class E1 extends D { C a; }


In strong mode we would need to have covariant C a;.

eernstg · 2017-07-04T17:35:43Z

docs/language/informal/enhanced-type-promotion.md

+
+foo(A x) {
+  if (x is B) {
+    var y = x.v;


If we promote x it has type B here, so y has type E2 ..

eernstg · 2017-07-04T17:41:43Z

docs/language/informal/enhanced-type-promotion.md

+  if (x is B) {
+    var y = x.v;
+    if (y is E1) {
+      x = fn(y.a, new B());


y isn't promoted (wasn't a supertype of E1), so y.a has type C. The invocation of fn receives arguments of type (C, B), depending on the meaning of fn we might infer a type argument B and it might return B, which is OK for x (assuming that we allow assignments to a promoted variable as long as it preserves the promotion).

I wouldn't claim that there can't be any cycles involving type inference, but I couldn't see them in the given example. But I suspect that the cycles could be eliminated by introducing demotion of variables (such that the promotion doesn't apply "after" the assignment which could violate the promotion).

lrhn · 2017-07-05T10:28:37Z

Erik's comment on the "comes after" specification is correct.

I like to think of it as "a test/branch dominates another expression/statement" when all routes of execution from the test to the expression requires the test to have the same value. That is, when reaching the expression/statement implies the result of the test.

Maybe that's a way to specify it. Needs more thinking obviously :)

(Or am I just going down the dark and quirky path of abstract interpretation here :)

mit-mit · 2018-11-02T08:53:27Z

@munificent @lrhn what is the status of this?

bwilkerson · 2018-11-02T13:26:37Z

Is there a language issue to track this?

munificent · 2018-11-02T21:08:45Z

Back when the final feature list for Dart 2.0 was put together, this didn't make the cut. It's been inactive since then.

leafpetersen · 2018-11-02T23:23:57Z

I'm hoping we can land this (or a superset of this) at some point in the next year or two as an opt in feature. How about we:

open an issue in the language repo for improved type promotion (but don't make it active yet)
land this PR in the language repo working directory as a strawman
link the strawman from the issue to track it

Was originally at: dart-lang/sdk#29624

munificent · 2018-11-03T00:20:23Z

open an issue in the language repo for improved type promotion (but don't make it active yet)

dart-lang/language#80

land this PR in the language repo working directory as a strawman

dart-lang/language#79

link the strawman from the issue to track it

Done.

Was originally at: dart-lang/sdk#29624

"Enhanced Type Promotion" informal proposal.

49b5c1e

munificent added the area-language Dart language related items (some items might be better tracked at github.com/dart-lang/language). label May 16, 2017

googlebot added the cla: yes label May 16, 2017

bwilkerson approved these changes May 16, 2017

View reviewed changes

munificent mentioned this pull request May 17, 2017

Type propagation/inference not symmetric for ?: #26086

Closed

floitschG reviewed May 18, 2017

View reviewed changes

lrhn reviewed May 18, 2017

View reviewed changes

Tweak proposal.

b6fd44f

- Fix typo in example. - Clarify that labeled statements are not supported. - Allow statements that cannot complete normally anywhere in the block.

leafpetersen reviewed May 24, 2017

View reviewed changes

lrhn reviewed May 31, 2017

View reviewed changes

stereotype441 reviewed Jun 2, 2017

View reviewed changes

johnniwinther reviewed Jun 7, 2017

View reviewed changes

Allow assignment inside the promoted scope.

6c174d4

Clarify that when that happens, the assignment is checked (statically and dynamically for implicit downcasts) against the promoted type.

munificent mentioned this pull request Jun 13, 2017

Make type rules more flow sensitive. #18921

Closed

Remove assignment from proposal and explain in "Alternatives" section.

30acbdc

eernstg reviewed Jul 5, 2017

View reviewed changes

natebosch mentioned this pull request Jul 26, 2018

improve type promotion in strong mode #25565

Open

8 tasks

matanlurey mentioned this pull request Nov 1, 2018

No type inference from is! #35019

Closed

munificent added a commit to dart-lang/language that referenced this pull request Nov 3, 2018

Move over "Enhanced Type Promotion" proposal.

192e026

Was originally at: dart-lang/sdk#29624

munificent mentioned this pull request Nov 3, 2018

Move over "Enhanced Type Promotion" proposal. dart-lang/language#79

Merged

munificent closed this Nov 3, 2018

munificent deleted the enhanced-type-promotion branch November 3, 2018 00:20

lrhn pushed a commit to dart-lang/language that referenced this pull request Nov 7, 2018

Move over "Enhanced Type Promotion" proposal. (#79)

981b6f8

Was originally at: dart-lang/sdk#29624

		after the if statement in the immediately enclosing block.

		This is also allowed if the if statement has no else clause at all.


		* A block that directly contains a statement that cannot complete normally.

		We do not allowed labeled statements of the above form. Fortunately, labels

		* An if statement with an else where neither statement can complete normally.

		* A block that directly contains a statement that cannot complete normally.


		### 17.6.1 For Loop

		Given a for statement of the form for (..., c, ...) s, if

"Enhanced Type Promotion" informal proposal. #29624

"Enhanced Type Promotion" informal proposal. #29624

Conversation

munificent commented May 16, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

munificent Jun 6, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lrhn May 31, 2017 • edited by munificent Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

munificent Jun 6, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

munificent Jun 6, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eernstg left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

munificent commented May 16, 2017 •

edited

Loading

munificent Jun 6, 2017 •

edited

Loading

lrhn May 31, 2017 •

edited by munificent

Loading

munificent Jun 6, 2017 •

edited

Loading

munificent Jun 6, 2017 •

edited

Loading