Introduced "future value type" of async functions; used it to correct return rules

[eernstg]

Turns out that the existing rules did not correctly cover the following case:

import 'dart:async';

Future<Future<int>> g() async {
  return Future<int>.value(42);
}

The introduction of the future value type of an async function ensures that the situation gets one level of indirection simpler, and I used this simplification to solve the above problem.

This also means that the rules about return statements in async functions have been changed such that they are no longer based on wrapping both the type of the expression whose value is used to complete the returned future, as well as the component type of the returned future (that is, the constraint on the possible instances used to complete that future). This is discussed in #914.

[leafpetersen]

Please don't land this, at least until we've discussed what the path forward is. If I understand this correctly, you're proposing a change to the pre-nnbd return rules? I don't know that we're planning to make any changes there. Or if this is intended to be an NNBD change, we need to land this in the NNBD feature spec as well (even if this is just in the form of a callout in the feature spec pointing to a diff to the formal spec). I also feel very strongly that we only have bandwidth for one round of changes around returns. We should aim to have:

• A single PR with the new rules.
• An accompanying set of tests for the changes .

[eernstg]

you're proposing a change to the pre-nnbd return rules?

I'm proposing that we fix the spec bug which makes the Future<Future<...>> example a compile-time error. Note that dart and dart2js accept and run this program, and the analyzer reports an error where both the return type and the type of the returned expression is obviously wrong (so the associated code in the analyzer must be revisited in any case, and checking "S is assignable to T or flatten(S) is assignable to T" could be a very localized change).

With that, I believe that this PR makes the pre-nnbd return rules for the relevant situation say what we intended to say all the time.

Cf. the discussion in #914:

If you both prefer model/option 1 then we should not put it into the language specification at this point, because that is a breaking change:

import 'dart:async';

Future<num> f() {
  Future f = Future<int>.value(2); // Or `FutureOr f = ..`.
  return f;
}

void main() async {
  print(await f());
}

This program works in pre-null-safety Dart, but with model 1 it will be a compile-time error, and I'm not convinced that it is helpful for anybody to backport this breaking change.

[leafpetersen]

I don't think changing the pre-nnbd rules is a priority right now.

[eernstg]

I expect that the language specification with null-safety will rely on the existing language specification for thousands of details. So fixing a bug there serves both the direct purpose of fixing the bug in pre-nnbd Dart (and I understand that you think this is less important), but it also ensures that the specification is ready for null-safety.

This ensures that the transition to null-safety will be well understood: If we wish to switch from model 2 ('S is assignable to T or flatten(S) is assignable to T') to model 1 ('S is assignable to T or flatten(S) <: T'), then that's what we will say in the nnbd spec.

If we don't fix the spec bug now then we'll need to do it later, and it will be more difficult to understand what difference null-safety makes for async returns, because it will be a combination of a bug fix and an actual breaking change (2 -> 1, if we do want that).

[lrhn]

I don't think that changing the pre-NNBD behavior is a priority.
If we change the specification, it should be to match the actual behavior.
We've lived with the current behavior for years now, so changing it is not urgent.

The NNBD behavior is more important because it doesn't work unless modified.
We need to fix that, and ensure that the fix is of good enough quality to keep working for some more years without further changes.

That's still limited by not wanting to add too big changes to NNBD at this point.
(Which is why I don't expect the "don't await futures at all" solution to get through, sadly).

[eernstg]

Just wondering, @lrhn, do you agree that the notion of the 'future value type' of an async function (or element type, or whatever we want to call it) clarifies and simplifies the rules overall?

Also, do you agree that Future<Future<int>> f() async => Future<int>.value(42); should not be a compile-time error?

If we change the specification, it should be to match the actual behavior.

I believe this PR describes the existing behavior of the CFE. The analyzer reports an error for the case that I mentioned (that is, return aFutureOfU with return type Future<Future<U>>, plus various situations that are small variations of this situation).

We could decide by fiat that there is no implementation effort: The CFE is fine, and the analyzer behavior is a known bug (because it is a faithful implementation of a spec rule that didn't have exactly the intended properties). So we just decide that we don't intend to fix it before null-safety is introduced.

The NNBD behavior is more important because it doesn't work unless modified

We can easily keep 'S is assignable to T or flatten(S) is assignable to T', or change it to 'S is assignable to T or flatten(S) <: T'.

With that, and the rest of the specification switched to null-safety, I do believe that we have a working model.

For the dynamic semantics, I don't see why we shouldn't be able to keep the current specification, if we prefer that.

I proposed the 'extended static await' (xsa) rules in order to make all properties, and in particular the presence/absence of await, statically known whenever possible.

I checked that it is a non-breaking change (except for that very marginal case where the returned expression e has static type T and evaluates to an object that has type T as well as type Future<T>; in that case the current semantics will await the future, and the xsa semantics will use the object directly). Other than that, the difference between the current semantics and the xsa semantics is only that the current semantics will incur a dynamic error in some cases where the xsa semantics continues execution.

So the xsa rules are a very-very-nearly non-breaking change, and I find the static nature of these rules helpful, in order to be able to tell developers what's going on.

If we use flatten(S) <: T then I believe that the two semantics coincide apart from the weird T & Future<T> case (the extras allowed by the xsa semantics are then compile-time errors).

I would still prefer to use the xsa rules because they are more static (and I think they make programs more predictable), but the difference is very small at that point.

[lrhn]

Just wondering, @lrhn, do you agree that the notion of the 'future value type' of an async function (or element type, or whatever we want to call it) clarifies and simplifies the rules overall?

That's a good move, especially since it's not just flatten of the return type, as I initially assumed.

Also, do you agree that Future<Future> f() async => Future.value(42); should not be a compile-time error?

Yes. That's just wrong. That said, I don't particularly care whether we fix it in pre-NNBD code, as long as we fix it for post-NNBD code. We've lived with the pre-NNBD behavior for years now, and haven't gotten any serious complaints. Risking a breaking change is not worth it. So ...

We could decide by fiat that there is no implementation effort: The CFE is fine, and the analyzer behavior is a known bug (because it is a faithful implementation of a spec rule that didn't have exactly the intended properties). So we just decide that we don't intend to fix it before null-safety is introduced.

Yes to that. The analyzer can fix the bug eventually, if they want to, but there is no urgency, but we'd have to specify the behavior they should fix it to (and not as "what the CFE does").

So, post-NNBD. I think I prefer "flatten(S) <: T" to "flatten(S) assignable to T".

I prefer just "S assignable to T" even more, but fear it's too breaking (would require changes to the migration tool, and it's probably too late now, because it would require re-migrating already migrated code).

The extended static await rule is interesting, though.

1. If S <: T: Desugar to _return r.
2. If S is dynamic: Desugar to _return (r is Future<T>) ? await r : (r as T).
3. If S implements Future<U>, U assignable to T: Desugar to _return await r, resp. _return (await r) as T.
4. If S is FutureOr<U>, U assignable to T: Desugar to if (r is Future<T>) _return await r; else _return r;, resp. the same thing with as T in the else branch.

The tricky case is:

Future<Future<int>> foo() async {
  Future<dynamic> x = Future<int>.value(42);
  return x;
}

Here the static rules would use item 3. and await the Future<dynamic>, get an int and throw because it's not a Future<int>. Had it not awaited, the code would have worked.

That code currently works in our implementations, and it's allowed by the run-time semantics, so that would be the breaking change.

I do like that the only implicit down-casts happen when the original static type contains dynamic.
I'm slightly iffy about the difference between Future<dynamic> and FutureOr<dynamic>.

The former will await any future, then down-cast the result to T . The latter only awaits Future<T>s, then tries to downcast other futures to T, so an actual Future<dynamic> would not be awaited even though it's not a T. That's an asymmetry which irks me.

How about these "generalized static await" rules (to give them a name):

• S <: T ↦ _return r;
• S is dynamic ↦ _return r is Future<T> ? await r : (r as T);
• S implements Future<T> ↦ _return await r;
• S implements Future<dynamic> ↦ _return (await r) as T;
• S is FutureOr<U> and U <: T ↦ _return r is Future<U> ? await r : r;
• S is FutureOr<dynamic> _return (r is Future<dynamic> ? await r : r) as T;

I like that the type we are checking the FutureOr<U>/FutureOr<dynamic> against is one of the parts of the union type. This guarantees that we are actually deconstructing the union type, and not accidentally cutting along some other division line and getting accidental matches.
(If Future<T> allows part of U, then deconstructing FutureOr<U> by checking is Future<T> may potentially await some Us that are not Future<U>s. It still works type-wise, but it feels wrong).

I think the rules can be written shorter as:

• S <: T ↦ _return r;
• S is dynamic ↦ _return r is Future<T> ? await r : (r as T);
• R = flatten(S) ≠ S and R assignable to T ↦ _return (r is Future<R> ? await r : r) as T;

with some of the tests and casts being redundant in some cases.

[eernstg]

Here's a possible way forward:

We land this as is (containing 'S is assignable to T or flatten(S) is assignable to T', because that's the rule which will fix the spec bug and make no breaking changes). Note that this PR does not make any changes to the dynamic semantics. Also, there is no implementation effort:

I'll create an implementation issue for the analyzer, give it the lowest priority, and explain that there is this discrepancy between the spec and the analyzer behavior, but we do not plan to fix it because pre-null-safety Dart will soon be in the past and we have lived with this behavior for years.

Next, I'll create a PR on the nnbd spec: It will require the above phrase to be changed to 'S assignable to T or flatten(S) <: T', and it update the specification of the dynamic semantics to whatever not-very-breaking variant we want, with 'generalized static await' as the starting point.

How do you like that?

[lrhn]

Initial steps seem fine.

The one thing I worry about wrt. NNBD semantics is that we change the run-time semantics in a way that cause new run-time errors. That is, the same programs are still accepted, but they have slightly different semantics in a few edge cases. That's still going to hit some people, and there won't be any good static help.
Statically refusing something that will be a run-time error is good, though. As always. :)

[eernstg]

We agreed to perform all the changes in null-safety world, so there will not be any changes to the language specification at this point (it happens in the nnbd spec). So I'll close this PR without landing it.