Specify null safety: Sections 'Variables' and 'Local Variable Declarations'

[eernstg]

Leaf and Lasse, I believe you might discuss this PR and decide on whether one of you would give it a review. For now I'm just putting it on github such that reviewing can start whenever it fits (I guess it makes sense to wait for #2023).

This PR updates the sections 'Variables' and 'Local Variable Declarations' of the language specification to fit the language with null safety.

It is part of a larger PR, but provided in smaller pieces in order to make the reviewing task manageable. Because of this, the updated text contains a handful of undefined \ref{...} references. They refer to newly added sections which are included in #2023.

Apart from that, this PR changes dart.sty to a new version of the file which will work with all the null safety updates (so we don't have to update dart.sty again and again during this process). However, this causes a couple of changes outside the above mentioned sections: A couple of commands need to get an extra argument (it's an {r}, specifying the metasymbol which stands for either the empty string or required, which is now needed in some rules about functions and function types). Similarly, this PR also changes \Gamma to \Delta to denote type variable environments, because that's a more commonly used notation (and the new dart.sty has it in some commands already).

[github-actions]

Visit the preview URL for this PR (updated for commit 3285049):

https://dart-specification--pr2052-specify-null-safety-3qf0tqse.web.app

_{(expires Wed, 26 Jul 2023 11:48:21 GMT)}

_{🔥 via Firebase Hosting GitHub Action 🌎}

_{Sign: 6941ecd630c4f067ff3d02708a45ae0f0a42b88a}

[eernstg]

@lrhn, would you be able to take a look at this PR? I'm removing @leafpetersen as a reviewer, because it's obviously a good idea to broaden this effort a bit.

[eernstg]

@lrhn, when you're back from vacation, could you take a look at this one?

[eernstg]

Thanks, and PTAL!

[eernstg]

@lrhn, friendly ping.

[lrhn]

... is an immutable and non-late variable that has potentially been assigned, or if it is immutable and late and definitely assigned.

Should we have an abstraction?

A local variable may be assigned if it is not immutable,
or if it's immutable and definitely unassigned,
or it's immutable and late and not definitely assigned.

(Variables with initializer expressions are always definitely assigned, even if they are late and not initialized yet.)

Just so we don't have to remember every case every time.

The following are both valid and run today:

  final int x;  
  for (x in [1]) {print(x);}

  late final int x;  
  for (x in [1]) {}
  print(x);

[eernstg]

This section is concerned with asynchronous for-in statements, so we'd need to consider await for .... Again, I do get errors for this:

void main() async {
  final int x1;
  await for (x1 in Stream.fromIterable([1])) {
    print(x1);
  }

  late final int x2;
  await for (x2 in Stream.fromIterable([1])) {}
  print(x2);
}

line 3 * The final variable 'x1' can only be set once.
line 8 * The late final local variable is already assigned.

Error compiling to JavaScript:
lib/main.dart:3:14:
Error: Can't assign to the final variable 'x1'.
  await for (x1 in Stream.fromIterable([1])) {
             ^^
lib/main.dart:8:14:
Error: Can't assign to the final variable 'x2'.
  await for (x2 in Stream.fromIterable([1])) {}
             ^^
lib/main.dart:4:11:
Error: Final variable 'x1' must be assigned before it can be used.
    print(x1);
          ^^
lib/main.dart:9:9:
Error: Late variable 'x2' without initializer is definitely unassigned.
  print(x2);
        ^^
Error: Compilation failed.

[lrhn]

The

line 8 * The late final local variable is already assigned.

looks spurious. At the assignment to x2 in the loop, it's at most possibly assigned, and since it's late, that's OK.

The read afterwards is also OK, since it's possibly assigned, and again that's good enough.

That is, there is a possible execution sequence where the late variable doesn't throw when accessed, so it would be wrong to consider the program incorrect. (Non-late variable uses must be valid on all execution paths, late variable uses must be possibly valid on at least one.)

[eernstg]

The error message for line 8 is of course less than ideal: It does not include the name of the variable.

I don't think we can use ad-hoc reasoning and conclude that a given late variable is possibly assigned, etc, because the actual analysis will do something specific (for loops, and for any other construct), and the resulting data is used to determine where/why to emit compile-time errors. We just have to live with the outcome, even when it is "easy to see" that some other result would have been more precise and still sound.

For example, the assignment to x in for (x in ...) is presumably approximated to run at least twice (even though it might just run once or not at all). This implies that we have approximated and then concluded that there is an assignment to x at a time where it is definitely assigned. That is indeed true for any loop execution that iterates more than one time.

However, I do think we should take this opportunity to double check that the implementations are consistent with the specification.

So we should get an error for an x which is immutable, both when it is non-late and when it is late, and then both when it is definitely unassigned and when it is possibly assigned. We do get that:

void main() async {
  {
    // Immutable, non-late.
    final int x;
    await for (x in Stream.fromIterable([1])) {} // Error: can only set once.
    print(x); // Error: potentially unassigned: OK.
  }
  {
    // Immutable, late, definitely unassigned at `for`.
    late final int x;
    await for (x in Stream.fromIterable([1])) {} // Error: is already assigned.
    print(x);
  }
  {
    // Immutable, late, possibly assigned at `for`.
    late final int x;
    if (2 > 1) x = 1;
    await for (x in Stream.fromIterable([1])) {} // Error: is already assigned.
    print(x);
  }
}

I think we should just keep the spec as it is, given that this is also the implemented behavior.

[lrhn]

For example, the assignment to x in for (x in ...) is presumably approximated to run at least twice

It most certainly is not, because analysis must assume that the loop body runs zero times.
Flow analysis is not approximating, it's doing worst-case analysis, which means that in case of doubt, the result is "potentially assigned" (aka: "We don't know").

The only possible results of assignment analysis are:

• Definitely unassigned
• Definitely assigned
• Potentially assigned/unassigned (same thing, "we don't know")

The analysis must be sound.

int x;
await for (x in Stream<int>.empty()) {
  print("nope");
}
print(x); // Must be compile-time error, x potentially assigned.

Changing int x to final int x should be an error because any variable assigned in the for (<here> ...) assignment should
be considered potentially assigned after the loop, or in that assignment, and definitely assigned in the body. Because that's the only sound analysis.
Changing it to late int x; should not be an error, because it is at most potentially assigned in the loop-header assignment. (Because the first time we get there, it's unassigned.)

If we assume it's definitely assigned there, it should also be definitely assigned after the loop. Doing the same analysis for a non-late-final variable is unsound.

(But I agree we have weird behavior in the implementation.)

[eernstg]

The approach to type inference is tricky, and we are not going to resolve all issues with that topic in this PR. So I mainly changed the wording at the locations where "type inference is assumed to have taken place already" is obviously wrong. We should deal with that topic by actually specifying type inference in detail, but that won't be right now.

Next, lots of imprecise details have been fixed.

PTAL.

[eernstg]

Ah, two more updates needed; will be finished this with this hour.

[eernstg]

OK, latest updates have now been uploaded, PTAL.

[eernstg]

See also dart-lang/sdk#52704.

[eernstg]

@lrhn, friendly ping..

[eernstg]

@lrhn, friendly ping...

[lrhn]

(I worry that this phrasing will come back to haunt us. It's probably correct: A variable declaration and a formal parameter declaration are two distinct syntactic productions. But we haven't defined what a variable declaration is. There is no "A variable declaration is the result of one of the following productins: ...." and "A parameter declaration is the result of the production <normalFormalParameterNoMetadata>" ... or something. So as written, it's saying that two undefined concepts are distinct.)

[eernstg]

We do have a well-defined notion of the declarations considered as syntactic entities. The level which hasn't been defined particularly explicitly is the semantic entity which is introduced (into some other semantic entity like a compile-time scope or a run-time scope). We do say that a declaration "induces a local variable" or "introduces a local variable" into a given scope, which is arguably a reference to a semantic entity.

We are making this distinction already in some situations: An initializing formal introduces a local variable in two scopes.

So I think this will be OK after all.

[lrhn]

(That works too. But so would defining a non-local-late-final-no-initializer variable as mutable. I just fear we'll make a mistake somewhere and assume that "non-mutable" means "not having a setter" or "not being assignable").

[eernstg]

I can see the issue. However, I think it would create more confusion to talk about a final variable with a setter as 'mutable' because that seems to imply that (1) it is intended to support updates, and (2) it would be possible to read it twice and get two different values.

I think it makes sense to reserve the word mutable for the situation where mutation is actually intended. The fact that we need to have a "once" setter with some final variables is secondary: The intention and actual semantics of this variable is that it doesn't mutate.

[lrhn]

For example, the assignment to x in for (x in ...) is presumably approximated to run at least twice

It most certainly is not, because analysis must assume that the loop body runs zero times.
Flow analysis is not approximating, it's doing worst-case analysis, which means that in case of doubt, the result is "potentially assigned" (aka: "We don't know").

The only possible results of assignment analysis are:

• Definitely unassigned
• Definitely assigned
• Potentially assigned/unassigned (same thing, "we don't know")

The analysis must be sound.

int x;
await for (x in Stream<int>.empty()) {
  print("nope");
}
print(x); // Must be compile-time error, x potentially assigned.

Changing int x to final int x should be an error because any variable assigned in the for (<here> ...) assignment should
be considered potentially assigned after the loop, or in that assignment, and definitely assigned in the body. Because that's the only sound analysis.
Changing it to late int x; should not be an error, because it is at most potentially assigned in the loop-header assignment. (Because the first time we get there, it's unassigned.)

If we assume it's definitely assigned there, it should also be definitely assigned after the loop. Doing the same analysis for a non-late-final variable is unsound.

(But I agree we have weird behavior in the implementation.)

[eernstg]

Great feedback again! The remaining issues are:

• I'd prefer to use the word 'immutable' about variables capable of mutation, not just as a flag that says "this variable induces a setter".
• Comment at line 1425, again about the word 'immutable'.
• Comment at line 18232, long discussion.

[eernstg]

We do have a well-defined notion of the declarations considered as syntactic entities. The level which hasn't been defined particularly explicitly is the semantic entity which is introduced (into some other semantic entity like a compile-time scope or a run-time scope). We do say that a declaration "induces a local variable" or "introduces a local variable" into a given scope, which is arguably a reference to a semantic entity.

We are making this distinction already in some situations: An initializing formal introduces a local variable in two scopes.

So I think this will be OK after all.

[eernstg]

I can see the issue. However, I think it would create more confusion to talk about a final variable with a setter as 'mutable' because that seems to imply that (1) it is intended to support updates, and (2) it would be possible to read it twice and get two different values.

I think it makes sense to reserve the word mutable for the situation where mutation is actually intended. The fact that we need to have a "once" setter with some final variables is secondary: The intention and actual semantics of this variable is that it doesn't mutate.

[eernstg]

This is again based on the perspective that a variable is mutable if it induces a setter, even in the case where that setter will ensure at run time that the variable cannot be mutated.

I'd prefer that we only use 'mutable' / 'immutable' in connection with actual mutation, not just with the formal property of having a setter or not.

[eernstg]

One more thing: As I mentioned, we currently use 'statically allocated variable' rather than the old 'static variable' meaning 'library variable or \STATIC{} variable' (that was 100% likely to confuse anyone who doesn't know). We need a better phrase, but it's very easy to change all occurrences because 'statically allocated variable' isn't used otherwise.

[eernstg]

Changed the text to avoid using the word 'mutable' and the word 'immutable' anywhere. It is now spelled out in each case which modifiers are required/assumed.

Changed the text to avoid using 'statically allocated variable' anywhere. Now spells out every time that the variable is a library variable or a static variable (and that's the new meaning of 'static variable', namely: A variable whose declaration includes the word static). In several locations we now use 'non-local variable' where we previously had all kinds of non-local variables anyway (as in 'if $v$ is a library variable, a static variable (new meaning), or an instance variable' becomes 'if $v$ is a non-local variable').

Eliminated the phrase 'static function' (there was exactly one, in non-normative text). Now using 'static member', which is well defined (meaning a member declaration that includes the keyword static).