o is! String
@johnniwinther

Fixed.

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.

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.

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"?

@floitschG

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.

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.

Done.

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.

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.

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

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.

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.

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.

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

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.

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.

"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."

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.

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).

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';
}

Aye.

Nit: these commas should be semicolons.

Fixed.

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.

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?

Yes.

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

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).

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.

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.

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

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

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).