Several related proposals for definite assignment and type promotion with NNBD

[stereotype441]

This issue captures some in-person discussion @lrhn and I had yesterday and today. A number of proposals were floated, and I'd like to hear others' opinions. Lasse, please let me know if I get some details wrong.

Proposal: promotions are recorded as a chain.

It would be nice to be able to write the following code:

// Example 1
void f(Object x) {
  if (x is! num) throw ...; // Promotes `x` to `num`
  if (x is int) { // Promotes `x` to `int`
    ...
  } else {
    if (x is! double) throw ...; // Promotes `x` to `double`.
  }
  x + 1; // Ok because `x` is known to be `num`.
}

(Note that all these examples assume the code has been "opted in", so that types are non-nullable by default, and enhanced type promotion and definite assignment analysis are enabled).

Consider what happens when type promotion analysis reaches the end of the second if statement. It has to join a control flow path in which x is promoted to int with a control flow path in which x is promoted to double. We would like it to remember the promotion to num.

The proposed way to do this is for the promotion process to record each promotion as a chain of types, where each type in the chain is a subtype of the next link in the chain. So if (x is! num) throw ...; promotes x from Object to num <: Object; if (x is int) promotes to int <: num <: Object; and if (x is! double) throw ...; promotes to double <: num <: Object. Joining two control flow paths is now a simple* matter of rewinding mismatched parts of the two chains until a matching type is found.

(*Ok, maybe it's not actually that simple. How do we join, for example, int <: Object with int <: num <: Object? What if the two chains form a diamond, e.g. List<int> <: List<num> <: Iterable<num> and List<int> <: Iterable<int> <: Iterable<num>?)

Proposal: some assignments promote.

It would be nice for type promotion to account for assignments, so e.g. one can do something like this:

// Example 2
void f(Object o) {
  if (o is! String) o = o.toString();
  o.length; // Ok because `o` has promoted type `String`
}

However, not every assignment should promote. Sometimes the user wants to explicitly declare a variable to have a more general type in order to avoid accidentally making use of more specific methods, and we want to preserve that ability. For example:

// Example 3
void f() {
  Iterable<int> x = ...;
  x = <int>[1, 2, 3];
  x[0] = 4; // Compile-time error: `Iterable<int>` does not support `operator[]`.
}

The proposed rule is that part of the state carried by the type promotion engine is a set* of "types of interest" for each variable, and an assignment will only promote if the type of the RHS is a subtype of one of the types of interest. So in example 1, if (o is! String) causes o to be promoted to String in the "else" branch, and to be "interested in" String in the "then" branch.
Then o = o.toString(); successfully promotes it, since it the type String is of interest. Then, at the end of the if statement, when the two control flow paths are joined, the promotion is preserved because it occurs along both control flow paths. However, in example 2, x = <int>[1, 2, 3]; causes no promotion because there are no types of interest to promote to.

(*Representing the types of interest as a set carries the disadvantage that if the RHS is a subtype of multiple types of interest it might not be clear which type to promote to; perhaps we should use a chain here too.)

Proposal: allow uninitialized non-nullable final variables.

In the area of definite assignment, it would be nice to be able to write final without an initializer, provided that definite assignment analysis can prove that the variable is definitely assigned before it is used. For example:

// Example 4
void f() {
  final int x;
  if (...) {
    x = 1;
  } else {
    x = 2;
  }
  print(x); // Ok because `x` is definitely assigned before it's used.
}

The current NNBD spec says that this works if final is dropped (it's ok to not initialize a potentially non-nullable variable provided that it is also marked late, or definite assignment analysis can prove that it is definitely assigned before it is read). Intuitively, the proposal is to have that the same rule apply for final variables.

However, the analysis is somewhat more complex because we need to verify that final variables aren't assigned twice. So this would be an error:

// Example 5
void f() {
  final int x;
  if (...) {
    x = 1;
  }
  x = 2; // Compile-time error: `x` might be assigned more than once.
}

So the definite assignment algorithm would need to track three possible states for each final variable: definitely not assigned, possibly assigned, and definitely assigned. Note that the "possibly assigned" state is a little weird for final variables because it renders them useles: you can neither assign the variable nor use it once it gets in this state.

A further complication is that as the spec is currently written, it is permissible (though useless) to have a final variable with no initializer whose type is nullable. (Such a variable receives the value null and cannot be changed). If we want to permit the pattern in example 4, it seems like we should prohibit the "useless null final" pattern, e.g.:

// Example 6
void f() {
  final int? x;
  print(x); // Compile-time error: `x` not assigned
}

Proposal: assignments to definitely unassigned final variables trigger promotion

The two previous proposals above have an unfortunate interaction: if you drop the type of the final variable, it is not promoted. For example:

// Example 7
void f() {
  final x; // Type is implicitly dynamic
  if (...) {
    x = 1; // Promotes to `int`
  } else {
    x = 2; // Promotes to `int`
  }
  x.length; // Compile-time error: `int` does not support `.length`.
}

It would be nice for type promotion to catch the bug in this case, and the previous argument that "we should only promote to types of interest" doesn't really seem as strong in this case, because the user didn't specify an explicit type.

So a further proposal is to waive the "types of interest" requirement when assigning to a definitely unassigned final variable with an implicit type. So in the above example, x.length would be caught as a compile-time error.

Proposal: assignments to definitely unassigned non-final variables also trigger promotion

It would be nice to have the invariant that changing "final" to "var" doesn't reduce the strength of type promotion. So for example, if we accept the proposal above, it would be nice for this to work too:

// Example 8
void f() {
  var x; // No longer `final`
  if (...) {
    x = 1; // Promotes to `int`
  } else {
    x = 2; // Promotes to `int`
  }
  x.length; // Compile-time error: `int` does not support `.length`.
}

When we discussed this today, we thought this would force us to have a new kind of state to represent the state of x after var x;. But on further reflection, we don't; this is the "definitely not assigned" state.

Proposal: use definite assignment analysis to flag compile time errors for obviously wrong code using "late"

The late keyword silences most of the errors we've been discussing here, causing runtime checks to occur instead. The idea is that the user doesn't want to be hindered when they know their code will work at runtime, but the compiler can't prove it. But we could consider still flagging it as an error if the compiler can prove that the code won't work at runtime. For example:

// Example 9
void f() {
  late final x;
  x = 1;
  x = 2; // Compile-time error: `x` already definitely assigned
}
void g() {
  late final x;
  print(x); // Compile-time error: `x` definitely not assigned 
}

After some discussion, we agreed that this probably isn't a good idea, for two reasons:

• It's a lot easier to explain the behavior of late as "enforces finality and definite assignment at runtime rather than compile time" rather than "enforces finality and definite assignment at runtime rather than compile time, unless definite assignment analysis can prove that a runtime error would occur in a certain code path"
• We don't want the user to get into the habit of seeing a compile-time error with a variable, adding late as an experiment to see if the error goes away, and taking that as a signal that the error wasn't legitimate.

[stereotype441]

@leafpetersen FYI

[lrhn]

Re.

Proposal: promotions are recorded as a chain.

...
(*Ok, maybe it's not actually that simple. How do we join, for example, int <: Object with int <: num <: Object? What if the two chains form a diamond, e.g. List<int> <: List<num> <: Iterable<num> and List<int> <: Iterable<int> <: Iterable<num>?)

Treating the chain as a set, which just happens to be totally ordered too, means that you can do an intersection and the result is still a chain. In that cast, you'd get List<int> <: Iterable<num> as the only types the two branches agree on.

The big question is whether a user will ever be able to understand that. They might - if they think of things being promoted and re-promoted, then they might mentally have the chain too (I know I do, and then I have to forget it again because Dart currently only remembers one type).

Re.

Proposal: assignments to definitely unassigned final variables trigger promotion

...
When we discussed this today, we thought this would force us to have a new kind of state to represent the state of x after var x;. But on further reflection, we don't; this is the "definitely not assigned" state.

The reason I wanted an extra state is that I also want the initial-assignment promotion to apply to non-final variables. A non-final variable with no type and with no initializer (var x;) is initialized to null, but it's not really initialized yet if you intend to late-init it below. So, I'd like to recognize the pattern:

var x;
if (...) { 
  x = ...;
} else {
  x = ...;
}

as a late-init of a mutable variable and still promote to the initialized type (if there is one such type).

[stereotype441]

Re.

Proposal: promotions are recorded as a chain.

...
(*Ok, maybe it's not actually that simple. How do we join, for example, int <: Object with int <: num <: Object? What if the two chains form a diamond, e.g. List<int> <: List<num> <: Iterable<num> and List<int> <: Iterable<int> <: Iterable<num>?)

Treating the chain as a set, which just happens to be totally ordered too, means that you can do an intersection and the result is still a chain. In that cast, you'd get List<int> <: Iterable<num> as the only types the two branches agree on.

The big question is whether a user will ever be able to understand that. They might - if they think of things being promoted and re-promoted, then they might mentally have the chain too (I know I do, and then I have to forget it again because Dart currently only remembers one type).

Good point. I like this approach.

[stereotype441]

Re.

Proposal: assignments to definitely unassigned final variables trigger promotion

...
When we discussed this today, we thought this would force us to have a new kind of state to represent the state of x after var x;. But on further reflection, we don't; this is the "definitely not assigned" state.

The reason I wanted an extra state is that I also want the initial-assignment promotion to apply to non-final variables. A non-final variable with no type and with no initializer (var x;) is initialized to null, but it's not really initialized yet if you intend to late-init it below. So, I'd like to recognize the pattern:

var x;
if (...) { 
  x = ...;
} else {
  x = ...;
}

as a late-init of a mutable variable and still promote to the initialized type (if there is one such type).

Right, but this example works as long as we consider a variable declaration without an initializer (like var x;) to put the variable in the "definitely unassigned" state. If we further stipulate that the "types of interest" requirement is waived when assigning to any definitely unassigned variable with an implicit type (regardless of whether the variable is final), then the two x = ...; statements will promote x, as you wanted.

[eernstg]

tl;dr We must manage certain sources of rampant subtlety; 'admitting' promotions would help tl;dr

Proposal: promotions are recorded as a chain.

At a control flow join point, for a variable x, we know that the type of the value of x is in the union of the predecessors, so the obvious promotion of x would be to that union. We can't express that, but the nearest type that we can express is the least upper bound. This would be optimal in the sense that it preserves the information established by previous promotions as far as possible using mechanisms that the language already supports.

So the rationale for using a mechanism which is clearly less precise will have to be something like "we only want to promote to a type of interest".

But this relies on developers having a table of "types of interest" in mind when they read and modify code, and (with further proposals: promote at assignment) those types of interest may arise basically anywhere in the preceding code, and it might be a type which is based on declarations in other libraries that the developer has never touched (x = foo(...)), and it might involve type inference (making it x = foo<int, Widget>(...).

I do not think it's realistic to assume that developers will have such a precise table of "types of interest" of the previous 50 lines of code immediately available when they encounter a surprise type error that promotion might have prevented. Using the LUB of the immediate predecessors in the control flow will at least allow developers to reason about the situation in a way that is more local.

maybe it's not actually that simple

Exactly. ;-) But the examples (say List<int> <: List<num> <: Iterable<num> and Iterable<int> <: Iterable<num>) seem to indicate that we would not just find the first shared type of interest in the k chains available at the join (here: Iterable<num>). If we start computing anything which is not already a type of interest then, again, we might as well use the LUB: That's actually simpler.

Proposal: some assignments promote

Do we have any examples where an assignment promotion is desirable, and the control flow is not similar to the following?:

void f(Object o) {
  if (o is! String) o = o.toString();
  o.length; // Ok because `o` has promoted type `String`
}

The underlying structure here is that we have a control flow branch (if), a non-zero number of the branches have a type test based promotion (the 'else' branch is guarded by o is String), and the remaining branches ('then') admit that promotion, because the assignment + soundness provides the guarantee that o is String will evaluate to true.

One thing to note here is that we do not have access to any useful types of interest in the predecessors of the assignment itself, so there is no justification for promoting o unless we consider types of interest that are established somewhere else.

I don't think it's meaningful to use nodes that are strictly after the assignment to justify promotion (this would make it an even more twisted exercise for developers to understand why a certain promotion does/doesn't occur). It could also be strictly before:

main() {
  Object o = ...;
  if (o is String) print("Yes!");
  ... // .. two screens further down ..
  o = 42; // No promotion, nobody cares about `int`s.
  o = "Yes, indeed!"; // Promotion.
}

I think this kind of promotion would be too capricious for practical software development. For instance, we could add else if (o is int) print("Even better!!"); after the first if, and suddenly the promotion at o = 42; would take place, and (possibly) the promotion at o = "Yes, indeed!"; would be eliminated because promotion is supposed to make the type of a variable a subtype of its current type.

I think it would be less twisted and more manageable in practice if we do not introduce promotion at assignments at the same level as promotion based on explicit type tests. Instead, we could allow promotion of a variable x to take place at a control flow join point P when:

• At least one predecessor of P promotes x, and the resulting promotion based on all predecessors of P where x is promoted is a type T.
• Every predecessor of P admits promotion of x to T.

The concept of admits promotion would enable assignments to have an effect, they would not be able to promote anything on their own.

An assignment admits promoting x to a type T if the assigned value has a static type which is a subtype of T.

This helps us avoiding two of the issues that I mentioned above: (1) We never consider the type of the right hand side of an assignment as a type of interest, so we avoid getting a bunch of mysterious breakages in client code when some method/getter gets a slightly different return type (perhaps based on updates in some far-away library, or perhaps based on a slightly different argument passed to a generic function, followed by a change in the return type because different type arguments were inferred).

And (2) we avoid forcing developers to scan over all the code up to the point that they are currently working on, in order to find all those locations where some subtle effect on promotion may or may not occur. Ideally, developers would be able to trust type tests as being the sole source of promotion, and assignments would only be admitted as secondary evidence during promotion.

Proposal: allow uninitialized non-nullable final variables

Sounds good!

Proposal: assignments to definitely unassigned final variables trigger promotion

This proposal raises the same issues as the previous one about assignments in general.

But if we change promotion such that type tests can introduce types of interest and assignments can admit promotions that are already on the table based on type tests, then I think this step would be fine as well.

[lrhn]

Let me try to nail down the situation I want to handle with "uninitialized" variables and assignment based promotion:

Define a local variable to be "type un-initialized" if:

• It has no declared type (only final or var).
• It has no initializer (maybe even allow an initializer of = null for a mutable nullable variable).
• (So the variable's type is dynamic, but it was not explicitly declared as such).
• The variable has not previously been assigned
  • Same as definitiely unassigned for final, lazy or non-nullable variables,
  • just not assigned yet for mutable nullable variables (which are initialied to null).
  • This rules out parameters, because the are always considered assigned by the invocation.

Then an assignment to a type un-initialized variable considers all types interesting and promotes to the assigned type.
This is one extra flag on the analysis of a variable. It's set if the declaration matches the requirements above, and is removed on any assignment, and it is removed when joining analysis results if it has been removed from either of the joined branches. (Or at least if the variable has been given a type)

The underlying idea is that if you don't write a type, it's not because you mean dynamic. You just didn't write a type. A value of null doesn't really count towards initialization.

This should cover the cases of "late initializaton" where you don't want to write the type on the variable:

var subscription;
subscription = stream.listen(...);

or

var message;
if (input is String) {
  message = "Text: $input";
} else {
  message = "Object: $input";
}

and where the variable is likely never assigned again later.

(Sudden idea: Would it work to simply pre-promote these variables to Null for the mutable ones and Never for the non-mutable ones, and then say that we consider any assignment to a variable with promoted/static type Null or Never is "interesting"? That is, a declaration of var x; would have declared type dynamic and promoted type Null, so anybody trying to use it would be stopped, and we would also use that to trigger assignment promotion because Null is itself an uninteresting type, so any type is more interesting. We could even join var x; if (something) x = "abc"; to have promoted type String? after the if).

[eernstg]

I think promotions based on assignments is a source of complexity that we must take seriously. It will force developers to play elaborate games with their source code when the type checker doesn't give them the type they expect.

Granted, it would be possible to make a distinction between an assignment to a 'definitely unassigned' variable and other assignments, but that's just one more level of implicit computation that developers will have to perform in their heads when they try to understand which assignments are promoting and which ones are not. This means that time is wasted during development, and it could very well give rise to style guide-ish advice along the lines of "never use assignment-promotion, it makes your code harder to read and maintain". However, even that is not an option, because we aren't going to stop using assignments.

To avoid having too many problems of that nature, it would be really helpful to make a clear distinction between promoting assignments and regular assignments.

@lrhn, you suggested v := e for that, and that makes a lot of sense: : is a hint about the relationship with typing, and it's easy to see/grep/search the :=.

If we have such an explicit distinction between promotion and regular assignments then we can proceed to check whether any given promoting assignment is OK or not.

var message;
if (input is String) {
  message := "Text: $input";
} else {
  message := "Object: $input";
}
// `message` promoted to `String` here.
message = 24; // Error, `24` not assignable to `String`.
message := 24; // Error, promotions must go to a subtype.

but

var message;
if (input is String) {
  message := "Text: $input"; // Hint: Promotion has no effect.
} else {
  message = "Object: $input";
}
// `message` still has type `dynamic` here.
message = 24; // OK.
message := 24; // Maybe OK.

The last case (Maybe OK) may be an error because there's a predecessor in the control flow graph where message was promoted to String (and int is not a subtype of that), but it might also be considered OK because the actual status is that message is not promoted.

In any case, I think we must give developers control of the situation, so they must have a simple and effective way to discern what's going on in terms of promotion, and they must have a way to explicitly control promotion—both of which point in the direction of an explicit mechanism like :=, or not promoting at assignments at all.

[lrhn]

I do like the idea of explicit promoting assignment. (I would prefer := for something else, but it's definitely applicable here).

I don't think we'll disallow an assignment like message = 24;. The variable's type is still dynamic, its current value has just been promoted to String. You can assign anything to the variable, even an int, but you'll demote then. You can even do message := 24; which will then demote to dynamic and re-promote to int.

If we allow an explicit promoting assignment, then we should remove the concept of "type of interest", and rely entirely on the explicit promotions.

[eernstg]

But if we rely entirely on explicit promotions then, presumably, every is and as test is explicitly promoting, and any occurrence that doesn't promote should give rise to some diagnostic message?

[leafpetersen]

However, not every assignment should promote. Sometimes the user wants to explicitly declare a variable to have a more general type in order to avoid accidentally making use of more specific methods, and we want to preserve that ability. For example:

// Example 3
void f() {
  Iterable<int> x = ...;
  x = <int>[1, 2, 3];
  x[0] = 4; // Compile-time error: `Iterable<int>` does not support `operator[]`.
}

I'd like to push on this just a bit. Do we really think this provides a lot of value? I very much buy this reasoning for non-local things where there's a contract between disjointly written pieces of code. But within a method body, code is by definition tightly coupled. And it's hard to see what I'm really protecting the user from if I allow them to use a more specific type for a variable within the dominated scope of an assignment. In your example, what does it hurt to treat x as a List? It is a list. And outside the scope where it's guaranteed to be a list, it's demoted back to an Iterable. So in some ways this is a nice pattern: on one control flow path I can assign an actual iterable to x, on another control flow path I can initialize it with a list, do some mutation to initialize it, and then forget that it's a list when I move back into the broader scope.

I guess there's some kind of code maintenance argument, where I might say that I don't want to start relying on something "accidental". But this feels very weak to me.

Am I missing something? Counter-arguments?

[lrhn]

The danger of accidental promotion usually comes from type inference propagating the unexpected type into a contravariant position.

So, in this case:

void f() { 
  Iterable<int> x = ...;
  x = <int>[1, 2, 3];
  var xs = [x];
  // Fails because xs has static type List<List<int>>, not List<Iterable<int>>:
  xs.add(someList.whereType<int>());    
}

Here the user has explicitly asked for Iterable<int>, and the promotion introduces a compile-time error which means they have to write Iterable<int> one more time to undo the promotion.

That said, it is really convenient to be able to do:

foo() {
  Object o; 
  String s;
  if (o is String) {
    s = o;
  } else {
    s = "$o";
  }
  ...
}

(get promotion when both branches assigns the same type to a variable), or

var x; ...
var xlen; 
if (somethingSomethingString) {
  x = "foo";
  xlen = x.length;
} else {
  x = 42;
  xlen = x.bitLength;
}

(referring to the value you just assigned without having to cast it).

Those might be harder to achieve without promotion from arbitrary assignments.

[lrhn]

About my earlier idea:
Let's say we pre-promote variable without an initializer expression to Null (if nullable and readable) or Never (if not readable). That is: var x; and String? x are promoted to Null (which is its actual value) and final x; and String x are promoted to Never because they're definitely unassigned and reading them will definitely throw.

Further, any assignment which invalidates the current promoted type of the variable will demote to the assigned type.
An assignment which satisfies the current promoted type will not promote unless it's a "type of interest". (Or whatever, that case isn't what I'm interested in here).

That is, on an assignment we keep the current type if possible, otherwise we fall back on the assigned type. If the assignment is a "type of interest", we even promote.
Because an uninitialized variable is promoted to a bottom/nearly-bottom type, all assignments are likely to demote to the assigned type.

It would grant me what I want:

var x;
if (y is String) { 
 x = y;
} else {
 x = "$y";
}
// x *demoted* to string on both branches, merged to string.

[leafpetersen]

So, in this case:

void f() { 
  Iterable<int> x = ...;
  x = <int>[1, 2, 3];
  var xs = [x];
  // Fails because xs has static type List<List<int>>, not List<Iterable<int>>:
  xs.add(someList.whereType<int>());    
}

Here the user has explicitly asked for Iterable<int>, and the promotion introduces a compile-time error which means they have to write Iterable<int> one more time to undo the promotion.

I still don't really buy this. I mean, yes, this arguably doesn't do what the user wanted. But that's a property of our inference, not particular to this kind of promotion. Here's the same example, using just current Dart 2.0 type promotion:

void f() { 
   Iterable<int> x = null;
   if (x is List<int>) {
     var xs = [x];
     // Fails because xs has static type List<List<int>>, not List<Iterable<int>>:
     xs.add([1].whereType<int>());
   }
}

[leafpetersen]

About my earlier idea:
Let's say we pre-promote variable without an initializer expression to Null (if nullable and readable) or Never (if not readable). That is: var x; and String? x are promoted to Null (which is its actual value) and final x; and String x are promoted to Never because they're definitely unassigned and reading them will definitely throw.

Further, any assignment which invalidates the current promoted type of the variable will demote to the assigned type.
An assignment which satisfies the current promoted type will not promote unless it's a "type of interest". (Or whatever, that case isn't what I'm interested in here).

That is, on an assignment we keep the current type if possible, otherwise we fall back on the assigned type. If the assignment is a "type of interest", we even promote.

Do you really mean "demote to the assigned type" unconditionally? Surely you mean something like "demote to the assigned type if it is one of the types in the history of the variable"? That is, you don't want to allow:

String? x;
x = 3;  // We don't want to demote to int here, right?

I'm a little hinky about typing a variable as Never. I think it's ok as long as you can't do anything except assign to it, but it's weird. Is all we're doing is using that as a proxy for "not yet assigned"? If so, maybe we should just use that?

• On assignment, if assigned type is a subtype of current type:
  • if assigned type is a type of interest, promote
  • if variable has not yet been assigned, promote