Author: Brian Wilkerson
Language team shepherd: Bob Nystrom
The Dart language features type promotion. This lets you avoid pointless explicit casts in some cases where it's obvious that a variable has a more specific type than its declared (or originally inferred) type. For example:
int stringLength(Object o) { if (o is String) { return o.length; // OK! } else { throw "Not a string."; } }
Without type promotion, the marked line would have a static error since Object does not have a .length getter. Type promotion notes that an is String test was applied to o, and promotes or “re-types” o to have type String inside the then clause of the if statement.
The type promotion rules in Dart are useful, but very restricted. Some restriction is necessary because dataflow based type inference can get quite complex in some cases. But, in practice, the current rules are too restrictive. For example, this does not work:
int stringLength(Object o) { if (o is! String) { throw "Not a string."; } else { return o.length; // Error: Object does not have a "length" getter. } }
The type promotion rules don‘t handle negated is checks and else clauses. This doesn’t work either:
int stringLength(Object o) { if (o is! String) throw "Not a string."; return o.length; // Error: Object does not have a "length" getter. }
Since the first line will definitely throw if o is not a String, the only way the second line could execute is if o is a string. But type promotion fails to understand that.
To get around these limitations, the analyzer used by IntelliJ and others also has “type propagation”. This is more sophisticated than type promotion. But, since the language spec controls what errors and warnings are shown, type propagation is limited to be using for things like auto-complete suggestions.
Maintaining two similar but different flow typing systems adds complexity to our tools and confuses users. (“Why are you showing me an error that a variable isn‘t a Foo, when auto-complete on that same variable shows me all of Foo’s methods?”)
To remedy that, this proposal augments type promotion with smarter rules when variables can be promoted. That should avoid requiring annoying redundant casts in more places, and let us unify type promotion and propagation into a single coherent system. This proposal doesn't cover all possible extensions to type propagation, but it handles the simplest, most common cases.
The language specifies type promotion out of four components:
Certain expressions cause a fact to be known about a variable. For example, o is String deduces the fact “o must be a String”.
The scope where a fact is known to be true. For example in:
if (o is String) { return o.length; } else { throw "Not a string."; }
The fact “o is a String” is known to be true inside the then clause of the if statement, but not the else clause, and not after the end of the if statement.
Which variables can have their types promoted. Some code may cause a fact to not be soundly reliable. In that case, we shouldn't promote. For example:
test(Object o, bool callClosure) { closure() { o = 123; } if (o is String) { if (callClosure) closure(); print(o.length); } }
At the point where .length is accessed, o may be a String, or it may be an int if callClosure was true. To avoid cases like this, the spec defines certain variables to be off limits for type promotion.
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.
This proposal keeps the same general pieces, but refines the first two of them. The third and forth are unchanged.
The specification defines a single fact that can be deduced: that a variable v has some type T. It says some expressions “show that a variable has some type”. There are two places this can happen:
Section 16.34 says that an “is-test” expression v is T shows that v has type T.
Section 16.22 propagates facts through logical expressions. It says (roughly) that an and expression like e1 && e2 shows v has type T if either e1 or e2 does.
In both cases there is an unstated assumption that the fact is deduced when the expression evaluates to true. We extend this to include information that can be deduced when an expression evaluates to false. As with the true case, there are two places that we can do this.
An is-expression e of the form v is! T, shows that v has type T when e is false.
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 the entire || expression evaluated to false.
The specification defines three scopes where promotion can apply:
The “then” clause of a conditional expression (16.20):
o is String ? oPromotedToStringHere : notHere
The right operand of a logical && expression (16.22):
o is String && oPromotedToStringHere
This is because short-circuiting means the right operand is only evaluated when the left is true.
The “then” clause of an if statement (17.5):
if (o is String) oPromotedToStringHere;
All of these correspond to code that is only reached if a condition expression evaluates to true. We extend this to cover facts that are known when an expression evaluates to false.
In a conditional expression of the form e1 ? e2 : e3, we know that if e1 shows that v has type T when e1 is false, then v is known to be of type T in e3:
o is! String ? notHere : oPromotedToStringHere
In a logical boolean expression of the form e1 || e2, if e1 shows v has type T when e1 is false, then v is known to be of type T in e2:
o is! String || oPromotedToStringHere
This is because short-circuiting means the right operand is only evaluated when the left is false.
In an if statement, if the condition shows that v has type T when the condition is false, then v is known to be of type T in the else clause.
if (o is! String) notHere; else oPromotedToStringHere;
Much like if statements, we extend C-style for and while loops to promote inside their bodies when the condition is true and the condition expression shows a v has type T:
while (o is String) oPromotedToStringHere; for (; o is String;) oPromotedToStringHere;
The last common case where users expect type promotion to work but currently doesn't is in code that can only be reached if a type test succeeds because earlier code will cause the code to exit, as in:
int stringLength(Object o) { if (o is! String) throw "Not a string."; return o.length; // Should be promoted here. }
We say a statement “cannot complete normally” if the statement is one of:
A return statement.
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 that directly contains a statement that cannot complete normally.
We do not allow labeled statements of the above form. Fortunately, labels are so vanishingly rare that this is unlikely to affect users in practice.
Then, given an if statement of the form if (b) s1 else s2 that is contained in some block:
If b shows that v has type T when b is true, and s2 cannot complete normally, then v has the type T in the statements after the if statement in the immediately enclosing block. As in:
int stringLength(Object o) { if (o is String) /* whatever */; else throw "Not a string."; return o.length; // Promoted here. }
If b shows that v has type T when b is false, and v can be promoted, and s1 cannot complete normally, then v has the type T in the statements after the if statement in the immediately enclosing block.
This is also allowed if the if statement has no else clause at all.
One frequent annoyance of the current type promotion rules is that assigning to the promoted variable anywhere inside the scope where the variable is promoted kills the promotion, even before the assignment. For example:
Object trimIfString(Object o) { if (o is String) o = o.trim(); return o; }
This code is dynamically correct and intuitively should work. But because o is assigned to inside the then body, no promotion occurs. Since Object doesn't define trim(), you get a static error.
This restriction does help avoid some patently wrong code:
test(Object o) { if (o is String) { o = 123; // No longer a String. print(o.length); // Error! } }
But it's too pessimistic since it also disallows valid code like the trimIfString() example. We considered two middle grounds. The first is to allow assignment as long as the type of the assigned value is a subtype of the promoted type. That means the first example would promote because the type of o.trim(), String, is a subtype of the promoted type, also String.
The problem is that when we are calculating promotion, we don't know the types of the right-hand sides. The two features can interact with type inference in complex ways. Consider:
if (o is String) { o = f(o); }
Is this promotion valid? It depends on the type of f(o). If f is a generic function, we need to infer its type parameter, which requires knowing the type of o. But o‘s type depends on whether or not it is promote, which is what we’re trying to calculate. We're stuck in a loop.
An even nastier example is:
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()); } } }
(Determining whether x and/or y should promote is left as an exercise for the reader.)
A simpler alternative approach suggested by Leaf is to simply always allow assignment inside the promoted scope and then type check it against the promoted type. If you assign a value whose type is not a subtype of the promoted type, you get a type error but it doesn't nullify the promotion:
test(Object o) { if (o is String) { o = 123; // Error: 123 is not a String. o.trim(); // OK. } }
Unfortunately, there are times when you still want to assign using the original declared typed. Consider:
class Node {} class Tree extends Node { final Node left, right; } Node leftmostLeaf(Node node) { while (node is Tree) { node = node.left; } return node; }
Promoting node to Tree inside the while body lets the node.left expression work, which is good. But it breaks the assignment. The assignment becomes an implicit downcast from Node (the type of node.left) to Tree (the promoted type of node). That downcast is checked at runtime in strong mode and may fail.
But the whole point of this code is to allow assigning a non-Tree to node. That's how you exit the loop. This program would throw a cast exception from otherwise correct code.
Worse, there‘s no easy workaround. You can’t “unpromote” a variable or “upcast” an lvalue like:
Node leftmostLeaf(Node node) { while (node is Tree) { node as Node = node.left; } return node; }
The most promising approach is to change the type of the promoted variable at the assignment. So, in this case, node would have the promoted type when evaluating node.left. And then immediately after the assignment, its type switches to Node, the resulting type of the assignment.
But this requires control flow analysis. Consider examples like:
test(Object o) { if (o is String) { o = "String"; } else { o = 1; // Change type to int. o = o + 1; // OK. int + int. o = "Not String"; // Now change to String. o = o.trim(); // OK. String.trim(). } return o.toLowerCase(); // OK? }
Here, since both paths definitely assign a String to o, ideally it would allow the toLowerCase() call on the result. That requires doing a join on the two control paths. This kind of analysis isn't bad, but it would make this proposal much more complex. We may go there, but we want something simpler we can implement soon to remove the ad hoc type propagation code in analyzer.
Putting together all of the changes above, the following are examples of how the specification might read when this proposal is integrated. There is no assumption here that this would be the final wording in the specification (I'm sure others are more skilled at crafting specifications than I am). There is also no attempt to highlight the differences from the existing specification because that was found to be confusing.
Given a conditional expression c of the form e1 ? e2 : e3, if
v is promotable in e2, ande1 shows that a variable v has type T when e1 is true.then the type of v is known to be T in e2.
Given a conditional expression c of the form e1 ? e2 : e3, if
v is promotable in e3, ande1 shows that a variable v has type T when e1 is false,then the type of v is known to be T in e3.
A logical boolean expression b of the form e1 || e2 shows that a variable v has type T when b is false if either e1 shows that v has type T when e1 is false or e2 shows that v has type T when e2 is false.
Given a logical boolean expression b of the form e1 || e2, if:
v is promotable in e2, ande1 shows that v has type T when e1 is false,then the type of v is known to be T in e2.
A logical boolean expression b of the form e1 && e2 shows that a variable v has type T when b is true if either e1 shows that v has type T when e1 is true or e2 shows that v has type T when e2 is true.
Given a logical boolean expression b of the form e1 && e2, if:
v is promotable in e2, ande1 shows that v has type T when e1 is true.then the type of v is known to be T in e2.
A unary expression b of the form !e shows that a variable v has type T when b is true if e shows that the variable v has type T when e is false. A unary expression b of the form !e shows that a variable v has type T when b is false if e shows that the variable v has type T when e is true.
Dart 1.0: Let v be a local variable or a formal parameter. An is-expression e of the form v is T shows that v has type T when e is true iff T is more specific than the type S of the expression v and both T != dynamic and S != dynamic. An is-expression e of the form v is! T shows that v has type T when e is false iff T is more specific than the type S of the expression v and both T != dynamic and S != dynamic.
Dart 2.0: Let v be a local variable or a formal parameter. An is-expression e of the form v is T shows that v has type T when e is true iff T is a subtype of the type S of the expression v, or, if S is a type variable with bound B, if T is a subtype of B. An is-expression e of the form v is! T shows that v has type T when e is false iff T is a subtype of the type S of the expression v, or, if S is a type variable with bound B, if T is a subtype of B.
Given an if statement of the form if (b) s1 else s2, if:
v is promotable in s1, andb shows that a variable v has type T when b is true.then the type of v is known to be T in s1. If the if-statement is enclosed in a block and if s2 cannot complete normally, and v is promotable in the statements (S) in the immediately enclosing block that follow the if statement, then v is known to have type T in S.
Given an if statement of the form if (b) s1 else s2, if:
v is promotable in s2, andb shows that a variable v has type T when b is false,then the type of v is known to be T in s2. If the if-statement in enclosed in a block and if s1 cannot complete normally, and v is promotable in the statements (S) in the immediately enclosing block that follow the if statement, then v is known to have type T in S.
Given a for statement of the form for (...; c; ...) s, if
v is promotable in s, andc shows that v has the type T when true,then v is known to have type T in s.
Given a for statement of the form for (...; c; u) s, if
v is promotable in u, andc shows that v has the type T when true,then v is known to have type T in u.
Given a for statement of the form for (...; c; u) s, if
v is promotable in the statements (S) in the immediately enclosing block that follow the for statement,c shows that v has the type T when false, ands is neither a break statement, nor a block containing, directly or indirectly, a break statement,then v is known to have type T in S.
Given a while statement of the form while (e) s, if
v is promotable in s, ande shows that v has the type T when true,then v is known to have type T in s.
Given a while statement of the form while (e) s, if
v is promotable in the statements (S) in the immediately enclosing block that follow the while statement,e shows that v has the type T when false, ands is neither a break statement, nor a block containing, directly or indirectly, a break statement,then v is known to have type T in S.
Given a do statement of the form do s while (e);, if
v is promotable in the statements (S) in the immediately enclosing block that follow the do statement,e shows that v has the type T when false, ands is neither a break statement, nor a block containing, directly or indirectly, a break statement,then v is known to have type T in S.
The static type system ascribes a static type to every expression. In some cases, the types of local variables and formal parameters may be promoted from their declared types based on control flow.
We say that a variable v is known to have type T whenever we allow the type of v to be promoted. The exact circumstances when type promotion is allowed are given in the relevant sections of the specification (16.20, 16.22, 16.29, 17.5, 17.6.1, and 17.7). Each of these sections defines the scope (range of code) in which the variable's type is to be promoted.
Type promotion for a variable v is allowed only when we can deduce that such promotion is valid based on an analysis of certain boolean expressions. In such cases, we either say that the boolean expression b shows that v has type T when b is true, or that the boolean expression b shows that v has type T when b is false. As a rule, for all variables v and types T, a boolean expression does not show that v has type T. Those situations where an expression does show that a variable has a type are mentioned explicitly in the relevant sections of this specification (16.34 and 16.22).
Dart 1.0: Type promotion for a variable v is also allowed only for a subset of variables and is dependent on the use of the variable in the scope in which the promotion would occur. If a variable is one for which type promotion is allowed, we say that the variable is promotable in some scope. A variable v is promotable in the scope S if all of the following conditions are met:
v is either a local variable or a parameter,
v cannot be potentially mutated within any closure, and
if v is accessed by a closure in S then v cannot be potentially mutated anywhere.
Dart 2.0: Type promotion for a variable v is also allowed only for a subset of variables and is dependent on the use of the variable in the scope in which the promotion would occur. If a variable is one for which type promotion is allowed, we say that the variable is promotable in some scope. A variable v is promotable in the scope S if all of the following conditions are met:
v is either a local variable or a parameter,
v cannot be potentially mutated within any closure, and
if v is accessed by a closure in S then v cannot be potentially mutated anywhere.
For the purposes of type promotion, a statement cannot complete normally if the statement is either
if (b) s1 else s2 where neither s1 nor s2 can complete normally, or