Skip to content

Bug in *flatten* function. #2310

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
lrhn opened this issue Jun 23, 2022 · 8 comments
Closed

Bug in *flatten* function. #2310

lrhn opened this issue Jun 23, 2022 · 8 comments
Labels
bug There is a mistake in the language specification or in an active document

Comments

@lrhn
Copy link
Member

lrhn commented Jun 23, 2022

EDIT: Not a bug in the flatten function, but in the implementations of await.

The flatten function in the language specification is intended to match the behavior of await at the type level.
That's why flatten(Future<int>) is int.

I believe there is a bug in the specification:

flatten(T) is defined by cases on T:

  • if T is S? then flatten(T) = flatten(S)?
  • otherwise if T is S* then flatten(T) = flatten(S)*
  • otherwise if T is FutureOr<S> then flatten(T) = S
  • otherwise if T <: Future then let S be a type such that T <: Future<S> and for all R, if T <: Future<R> then S <: R; then flatten(T) = S
  • otherwise flatten(T) = T

The issue is the third item:

if T is FutureOr<S> then flatten(T) = S

This fails to match await for, e.g., some values of the type FutureOr<Future<Object>>.

Object o = Object();
FutureOr<Future<Object>> f = Future<Object>.value(o);
var r = await f; 
print([r].runtimeType); // List<Future<Object>>
print(r.runtimeType); // Object
print(r.then); // Throws/crashes

The static type of r is flatten(FutureOr<Future<Object>>), which is Future<Object>.
The value of await f is the result of awaiting Future<Object>.value(o), which is o with runtime type Object.

The assignment isn't sound, so the spec for flatten fails to capture the runtime behavior of await.

A quick check in Dartpad shows that our behavior is indeed unsound. As usual, any such failure to be sound can probably be leveraged to convince the compiler of any other unsound thing, through a series of valid deductions starting from the false assumption. The VM gives an error on accessing then, and crashes when precompiled.

Addition: The last item is actually also wrong.

  • otherwise flatten(T) = T

fails for the type Object containing any Future<X?>.value(null).

It used to be that any proper supertype of Future/FutureOr types was a top type. Because of that, saying that await topTypeValue had the same type as the expression was safe.
With null safety, Object (and the equivalent FutureOr<Object>, etc) is a non-top super type of Future.

Object o = Future<Null>.value(null) as Object;
var v = await(o); // Static type `Object`, value `null`. Even in sound null-safe mode.

We need to make it

  • if T is Never, flatten(T) = Never
  • otherwise flatten(T) = T?

(because any non-Never class can have a subclass implementing Future<Object?>, and therefore can be awaited to the value null. Well, not function types, but I don't know if the exception is worth making. Not even sure the Never exception is worth it.)

Solution.

The spec and implementation of flatten should be changed to be sound.

The underlying rule is that the flatten of a union type should be the union of the flatten of the individual types of the union.
(Because await on a value of a union type is an await of a value of one of those types.)
Flattening a non-union type amounts to either reducing an interface type implementing Future<S> to S, or keeping a non-Future type as-is.

The problem is that we don't have a representation of general union types, so we can't just define

flatten(FutureOr<S>) = S | flatten(S)

It's not given that there is a Dart type representing that union. (I hope there always is one, but I haven't found a closed formula for finding it just yet.)

So, TODO: Find formula.

@lrhn lrhn added the bug There is a mistake in the language specification or in an active document label Jun 23, 2022
@lrhn
Copy link
Member Author

lrhn commented Jun 24, 2022

Trying to find a closed function definition which provides the nearest possible supertype of the "union of the flatten of each part of the union type" is an approach. It still has weird behavior for await of an Object.

That's because await is currently defined as a dynamic operation, which inspects the runtime type of the expression it awaits, independently of the static type. We've been trying to match the dynamic behavior in the static type using flatten, but with null safety, the dynamic behavior is no longer well-behaved enough for that to be easy (or perhaps even possible to do precisely).

Consider a different approach, where the await is based on the static type.

Awaiting an expression e with static type T works as:

  • If T is Future<X>, or T is class type which implements Future<X>, await the future and have static type X.
  • If T is S?, then behave like let v = e in v == null ? await Future<Null>.value(null) : await v.
  • If T is FutureOr<X>, then behave like let v = e in v is Future<X> ? await v : await Future<X>.value(v).
  • If T is dynamic, then behave like T was FutureOr<dynamic> (check for Future<dynamic> and wait for that).
  • Otherwise behave like await Future.value<T>(e).

That is, on union types, treat each part individually (which can obviously be optimized to only ever have two branches, one where you await the value, which must be a future, and one where you wrap the value in a future and await that future, because that's the only two possible final outcomes.) We treat dynamic as if it's FutureOr<dynamic>, which is safe and backwards compatible.

That would mean a flatten function defined as:

flatten(T) is defined as
if T implements Future<S>, flatten(T) = S
If T is S?, flatten(T) is flatten(S)?
If T is S*, flatten(T) is flatten(S)*
If T is FutureOr<S>, flattenT is S
Otherwise flattenT is T

That's actually the current flatten function!
So, this changed behavior is what we statically think we're already doing, and which all our existing programs already type-check and run against (without anyone telling us they found an unsafe behavior).
That suggests that the change is very safe to make,.

Also, code which has enabled the await_only_futures lint won't be affected either.

It would change current behavior in a number of potential cases, but those all involve FutureOr<Future<Object>...> or FutureOr<FutureOr<Object>>, where we no longer await the inner future.
If you don't nest future types, which you never should, there should be no change.
One case, which may actually exist, is someone doing Object o = ...; var v = await o;. That will currently await (and work if the future doesn't contain null), and will stop awaiting with this change.

@eernstg
Copy link
Member

eernstg commented Jun 24, 2022

The issue is the third item:

The code example does demonstrate that the behavior of the implementation differs from the specified behavior. Here's the spec language (from the null safety update of the spec) as well as the bindings of symbols in the text (the "actual values"):


  • a -> await f
  • e -> f
  • S -> FutureOr<Future<Object>>
  • o: Instance of Future<Object>
  • T -> Future<Object>
  • Future<T> -> Future<Future<Object>>
  • f -> Instance of Future<Future<Object>>
  • Static type of a -> Future<Object>

Evaluation of an await expression a of the form await e where e has static
type S proceeds as follows: First, the expression e is evaluated to an object o.
Let T be flatten(S) (17.11). It is a dynamic type error if the run-time type of
o is not a subtype of FutureOr<T> (that is, if it is neither a subtype of T nor of
Future<T>) [No dyn. error: Future<Object> <: FutureOr<Future<Object>>].

If the run-time type of o is a subtype of Future<T> [FALSE], then let f be o;
otherwise let f be the result of creating a new object using the constructor
Future<T>.value() with o as its argument [f: Instance of Future<Future<Object>>].

Next, the stream associated with the innermost enclosing asynchronous for
loop (18.6.3), if any, is paused. The current invocation of the function body
immediately enclosing a is suspended until after f completes. At some time after
f is completed, control returns to the current invocation. If f has completed
with an error x and stack trace t, a throws x and t (17.1). If f completes with
an object v, a evaluates to v [Instance of Future<Object>].


To me, this looks like the implemented semantics of await is incorrect, and the resulting behavior demonstrates a soundness violation.

But it looks like a case that we have looked at before, so I'm surprised that there is an issue with this today, I thought it had been fixed a while back.

The Future<Null> example has a similar analysis (with the conclusion that the implemented semantics is different from the specified semantics, and unsound):


  • a -> await o
  • e -> o
  • S -> Object
  • o: Instance of Future<Null>
  • T -> Object
  • Future<T> -> Future<Object>
  • f -> Instance of Future<Future<Object>>
  • Static type of a -> Future<Object>

In this situation, where the currently implemented behavior is unsound, it seems unlikely that we'd want to change the specification to simply specify what the implementations actually do. We seem to agree on this:

The spec and implementation of flatten should be changed to be sound.

However, I don't agree that the spec is unsound, so one obvious approach could be to keep the spec unchanged, and change the implementations accordingly.

@lrhn
Copy link
Member Author

lrhn commented Jun 24, 2022

I had totally forgotten that we have introduced such type checks in await, which would catch these cases of a future at runtime which does not match the static type from flatten.
The spec is (probably) sound then, and the implementations are lacking the mandated type checks.

Apparently the implementation teams didn't know about them either, which might have reminded me when I checked the code.

It's an extra type-check for Future<T>, not just Future, at every await. (Well, if the static type is already Future<T>, we can probably skip the check, because it definitely does satisfy the check. And function types and sealed types never do. So it's only really for awaiting FutureOr, where I'd expecte it anyway, and for Object/dynamic/other classes, which might have a subclass which implements Future). So some more type checks.

@eernstg
Copy link
Member

eernstg commented Jun 24, 2022

I was a bit worried about the performance implications: Is it possible that the specified semantics is significantly more costly than the currently implemented behavior, because the specified behavior will allocate and await a fresh future? Does it matter? — await is intended to cause a suspend operation to take place, so maybe it isn't particularly performance critical?

@lrhn
Copy link
Member Author

lrhn commented Jun 24, 2022

I think we can optimize away the extra future allocation. We just need to schedule the await continuation to continue with the raw value at a later point. Scheduling a microtask to just call continuation(value) directly should be cheaper than allocating a _Future which does the same thing, just with more steps. It's the same function that the awaited future calls when it completes with a value.

@eernstg
Copy link
Member

eernstg commented Jun 24, 2022

Cool! It sounds like we can make the change to the implemented behavior, and it shouldn't hurt.

@lrhn
Copy link
Member Author

lrhn commented Jul 6, 2022

I'd rephrase the:

otherwise let f be the result of creating a new object using the constructor Future<T>.value() with o as its argument

It's bad style to say that we use a specific constructor. In this case the Future.value is overkill, because it takes a FutureOr<T> as argument, but we only need the T part of it (and it would be a mistake to use the Future<T> branch - we won't because we only do the value case after checking for is Future<T>.
Also, the current implementation of Future.value uses a microtask. The implementation of await doesn't need that microtask (which is visible to the current Zone implementatin, and it would be best if it wasn't required to match Future.value.

So, I'd say:

otherwise let f be the result of creating a new object implementing Future<T>, having no public members other
that those of the Future interface and implementing no public interfaces other than Future and Object.
That future object will behave like a future which has been completed with the value o.

(Preferably, I'd actually rewrite completely to just say:

Next, the stream associated with the innermost enclosing asynchronous for
loop (18.6.3), if any, is paused. The current invocation of the function body
immediately enclosing a is suspended.
If the run-time type of o is a subtype of Future<T>, then at some time
after f is completed, control returns to the current invocation. If f has completed
with an error x and stack trace t, a throws x and t (17.1). If f completes with
an object v, a evaluates to v [Instance of Future].
Otherwise, the run-time type of o is a subtype of T and not of Future<T>,
and at some time after the current invocation was suspended, control returns to it,
and a evaluates to o.

Don't introduce a future where one isn't needed. We still get the delay. (We want the resume to correspond to an "event", but we haven't formally specified what that is, and if it's future-driven, it's not actually a microtask.)

@eernstg
Copy link
Member

eernstg commented Jul 7, 2022

I think we've addressed this at the spec level now with #2333. The implementation change is handled in dart-lang/sdk#49396.

@eernstg eernstg closed this as completed Jul 7, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug There is a mistake in the language specification or in an active document
Projects
None yet
Development

No branches or pull requests

2 participants