language icon indicating copy to clipboard operation
language copied to clipboard

The flatten function depends on static type, so it should be declared for type variables.

Open lrhn opened this issue 2 years ago • 13 comments

The flatten function determines/reflects the behavior of await on an expression based on the expression's static type.

The function is not completely defined since it relies on static type, but isn't defined for a type variable.

Example:

Future<void> foo<T>(T value) async {
  var x = await value;
  print([x].runtimeType); // JSArray<Object>, so x is Object
  print(x); // null
}

By the specification, the static type of value doesn't match any of the flatten cases (it's a type variable), so it should hit the last case and make the static type T. Then at runtime it should check is Future<T> before awaiting.

We currently have an unsoundness:

Future<void> foo<T>(T value) async {
  var x = await value;
  print([x].runtimeType); // JSArray<Object>, so x is Object
  print(x); // null
}

void main() async {
  await foo<Object>(Future<Object?>.value(null));
}

It's not clear whether this is just another instance of #2310 - the internal check of is Future<T> is skipped before awaiting.

However, if we do:

Future<void> bar<T extends Future<Object>>(T value) {
  var x = await value;
  print([x].runtimeType);
}

we'd probably expect that await to always await the value. The flatten, as written, still reaches its last case and makes the static type of x be T.

Our implementations do better:

Future<void> bar<T extends Future<A>>(T value) async {
  var x = await value; 
  print([x].runtimeType); // JSArray<A>
  if (value is Future<B>) {
    var y = await value; // value has static type `T & Future<B>`
    print([y].runtimeType); // JSArray<B>
  }
}

void main() async {
  bar<Future<A>>(Future<B>.value(B()));
}

class A {}
class B extends A {}

So, we actually do use the bound/promotion of a type variable (at least in some situations).

I propose making this all explicit by adding the following cases to flatten:

  • If T is type variable X with bound B, then flatten(T) = flatten(B)
  • If T is promoted type variable X & S, then flatten(T) = flatten(S)
  • Otherwise ...

The runtime behavior would be that where we do "If the static type is ..., do ..." we say that "If the static type is ... or it is X with bound B and B is ... or it is X&S and S is ..., do ...". That is, in every way, treat a type variable the same as its bound/promotion around await.

This makes the behavior explicit, and removes the type variable itself from the result. We should then add tests to ensure we have consistent behavior (I only tested in DartPad).

lrhn avatar Jul 02 '22 11:07 lrhn

Good catch!

However, the support for flatten(X) == T where X is a type variable (promoted or not) with bound Future<T> has actually already been addressed in the null safety updates to the language specification.

We have the notion of "a type S implements a type T":

When we say that a type $S$
\IndexCustom{implements}{type!implements a type}
another type $T$,
this means that $T$ is a superinterface of $S$,
or $S$ is $S_0$ bounded for some type $S_0$
(\ref{typesBoundedByTypes}),
and $T$ is a superinterface of $S_0$.
Assume that $G$ is a raw type
(\ref{instantiationToBound})
whose declaration declares $s$ type parameters.
When we say that a type $S$
\IndexCustom{implements}{type!implements a raw type}
$G$,
this means that there exist types \List{U}{1}{s}
such that $S$ implements \code{$G$<\List{U}{1}{s}>}.

A type variable X with bound B is 'bounded by' B; if B is itself a type variable bounded by B2 then X is also bounded by B2, and so on:

For a given type $T_0$, we introduce the notion of a
\IndexCustom{$T_0$ bounded type}{type!T0 bounded}:
$T_0$ itself is $T_0$ bounded;
if $B$ is $T_0$ bounded and
$X$ is a type variable with bound $B$
then $X$ is $T_0$ bounded;
finally, if $B$ is $T_0$ bounded and
$X$ is a type variable
then $X \& B$ is $T_0$ bounded.

So we're including type variables and promoted type variables in the definition of flatten because it says 'implements':

\begin{itemize}
\item If $T$ is \code{$S$?}\ for some $S$
  then \DefEquals{\Flatten{$T$}}{\code{\Flatten{$S$}?}}.
\item If $T$ is \code{FutureOr<$S$>} then \DefEquals{\Flatten{$T$}}{S}.
\item If $T$ implements \code{Future<$S$>}
  (\ref{interfaceSuperinterfaces})
  then \DefEquals{\Flatten{$T$}}{S}.
\item Otherwise,
  \DefEquals{\Flatten{$T$}}{T}.
\end{itemize}

which is rendered approximately as follows:

  • If T is S? for some S then flatten(T) = flatten(S)?.
  • If T is FutureOr<S> then flatten(T) = S.
  • If T implements Future<S> (11.2) then flatten(T) = S.
  • Otherwise, flatten(T) = T.

However, we still need to make a spec change in order to maintain soundness:

  • If T is S? for some S then flatten(T) = flatten(S)?.
  • If T is FutureOr<S> then flatten(T) = S.
  • If T implements Future<S> (11.2) then flatten(T) = S.
  • If T is a B bounded type variable or promoted type variable where is Object <: B, then flatten(T) = Object?.
  • Otherwise, flatten(T) = T.

The new 4th item ensures that flatten(X) == Object? when X is a type variable with bound Object or a top type. This is necessary, because an object of type X could be a Future<S> for any S.

Let's consider the examples based on this definition of flatten. I've inserted /**/ comments to indicate the static type of the await expressions:

We currently have an unsoundness:

Future<void> foo<T>(T value) async {
  var x = await value; /*Object?*/
  print([x].runtimeType); // Should be `JSArray<Object?>`.
  print(x); // null, no problem.
}

void main() async {
  await foo<Object>(Future<Object?>.value(null));
}

It's not clear whether this is just another instance of https://github.com/dart-lang/language/issues/2310 - the internal check of is Future<T> is skipped before awaiting.

However, if we do:

Future<void> bar<T extends Future<Object>>(T value) {
  var x = await value; /*Object*/
  print([x].runtimeType); // Should be `JSArray<Object>`.
}

we'd probably expect that await to always await the value. The flatten, as written, still reaches its last case and makes the static type of x be T.

This has now been corrected.

Our implementations do better:

Future<void> bar<T extends Future<A>>(T value) async {
  var x = await value; /*A*/
  print([x].runtimeType); // Should be `JSArray<A>`.
  if (value is Future<B>) {
    var y = await value; /*B*/ // `value` has static type `T & Future<B>`.
    print([y].runtimeType); // Should be `JSArray<B>`.
  }
}

void main() async {
  bar<Future<A>>(Future<B>.value(B()));
}

class A {}
class B extends A {}

Cool! So the implementations already behave as the updated definition of flatten requires. I updated the null safety spec PR to include the new 4th item in the definition of flatten.

eernstg avatar Jul 04 '22 14:07 eernstg

I think we still need to fix the cases prior to "implements Future<S>, because T is FutureOr<S> is not true for a type variable X with bound FutureOr<S>, and "is S?" is also not true for X with bound S?.

  • If T is S?, or is a type variable bounded by S?, for some S then flatten(T) = flatten(S)?.
  • If T is FutureOr<S>, or is a type variable bounded by FutureOr<S>, for some S, then flatten(T) = S.
  • If T implements Future<S> (11.2) then flatten(T) = S.
  • Otherwise, flatten(T) = T.

We don't actually need to make a change to flatten(Object) as long as the runtime semantics does an "is Future<flatte(T)>" before awaiting a future coming from an expression of type T. (In this case, if flatten(T) is Object, only await a future if it's a Future<Object>. If it's a Future<Object?>, it's just treated as an object. That's what we do in the other cases, like FutureOr<Object>.)

(I'd love to not actually do an await on a non-dynamic non-Future-implementing and non-FutureOr type (?/* qualified if necessary), but that's a breaking change.)

lrhn avatar Jul 04 '22 14:07 lrhn

True again, we do need to consider type variables with S? and FutureOr<S> as well.

  • If T is a type variable X with bound B then flatten(T) = flatten(B).
  • If T is an intersection type X & B then flatten(T) = flatten(B).
  • If T is S? for some S then flatten(T) = flatten(S)?.
  • If T is FutureOr<S> then flatten(T) = S.
  • If T implements Future<S> (11.2) then flatten(T) = S.
  • If T is Object then flatten(T) = Object?.
  • Otherwise, flatten(T) = T.

We also still need the special case for Object, because we could have await e where e has static type Object, but at run time e evaluates to an instance of Future<Object?>, so await e can't have static type Object.

eernstg avatar Jul 04 '22 15:07 eernstg

About Object, we can have flatten(Object) be Object if the runtime behavior is only to await a Future<Object>, not a Future<Object?>.

That is what we do for a static type of FutureOr<Object>, which also has a flatten of Object, so its consistent to do the same thing for Object itself. That is, if the static type doesn't mention Future (directly or through FutureOr), we assume that it isn't a future and use the static type of the expression directly as the static type of the await. If it turns out to be a future anyway, we only await it if it will still match the assumed static result type. (And if it's a FutureOr<X>, we assume it's either a Future<X> or a non-future X. And again, if the X turns out to allow a future, we only await it if it would match the expected result type.)

lrhn avatar Jul 05 '22 07:07 lrhn

if the runtime behavior is only to await a Future<Object>...

But await e should await any future, and it's up to the static type of the expression to faithfully allow for any outcome that this could produce. In particular, await Future.value(null) must evaluate to null, not to a future, and this does not depend on the context type of the expression.

The notion that some futures aren't awaited is associated with return statements in asynchronous functions, not with an awaitExpression. For instance, Future<Object> f() async { return Future<Object?>.value(); }.

The treatment of FutureOr<Object> is indeed another soundness issue:

import 'dart:async';

void main() async {
  final FutureOr<Object> fut = Future<Object?>.value();
  var x = await fut;
  // int i = x; shows that `x` has type `Object`.
  print(x); // 'null'.
}

eernstg avatar Jul 05 '22 08:07 eernstg

import 'dart:async';

void main() async {
  final FutureOr<Object> fut = Future<Object?>.value();
  var x = await fut;
  // int i = x; shows that `x` has type `Object`.
  print(x); // 'null'.
}

Interesting issue. Would @lrhn's condition fix this?

(And if it's a FutureOr<X>, we assume it's either a Future<X> or a non-future X. And again, if the X turns out to allow a future, we only await it if it would match the expected result type.)

In this case, since fut is a FutureOr<Object>, X = Object. But fut is neither a Future<Object> nor a non-future Object, it's a Future<Object?>, as indicated by print(fut.runtimeType). Future<Object?> is not a Future<Object>, though the opposite may be true. So why does await allow this?

Is this because the above conditions aren't actually implemented, or is it some sort of variance issue because of the generics?

Levi-Lesches avatar Jul 05 '22 08:07 Levi-Lesches

@eernstg

But await e should await any future, and it's up to the static type of the expression to faithfully allow for any outcome that this could produce.

That's what I thought in the first post of #2310, but you corrected me and pointed out that the specification states otherwise.

For await e where e has static type FutureOr<Object>, the specification says to only await a Future<Object>, not a Future<Object?> (which is an Object). That's why it wasn't a soundness issue that flatten(Future<Object>) is Object. (The soundness issue was that the implementations doesn't do that is Future<Object> test.)

lrhn avatar Jul 05 '22 08:07 lrhn

That's what I thought

Ah, you're right, we do specify await e with a check (that often needs to be a dynamic check) for whether we have a Future<flatten(staticTypeOf(e))>, it is not a special rule about return statements! Note to self: Do check the spec one more time, every time. ;-)

The spec was changed in https://github.com/dart-lang/language/pull/610, based on soundness issues with the old approach (where every future was awaited), in particular based on nested futures. For instance, we could encounter a Future<int> with static type FutureOr<Future<int>>, and it would then be a soundness issue if we await it and get an int with static type Future<int>.

The situation is similar with an e with static type Object or FutureOr<Object>: It is unsound to await e by awaiting a Future<Object?> that yields null, because it gets the static type Object.

Of course, we do have the option to change that static type to Object? by adjusting flatten, which would change the static type of some await expressions, and preserve the current dynamic semantics in this case. The spec section about await expressions would remain unchanged, it's only flatten which is modified (but the check for Future<T> would now be a check for Future<Object?>, and it would be awaited).

In the case where a Future<int> has static type FutureOr<Future<int>> it seems unlikely to me that we'd want to change flatten such that the future is awaited in an await expression. We would potentially await a Future<int> to get an int that would subsequently be passed to a context that needs a Future<int>. So we would be going one step too far, and it seems wrong to do that and then create a Future<int>.value(thatInt) (or to create an error future) in order to "go back again". I also don't think it's feasible to change flatten such that int <: flatten(FutureOr<Future<int>>).

So we do still need the check for Future<T> in the semantics of await expressions. It's only flatten that might be adjusted, and I'm only proposing that we consider doing that for the cases flatten(Object) and flatten(FutureOr<Object>)).

eernstg avatar Jul 05 '22 11:07 eernstg

import 'dart:async';

void main() async {
  final FutureOr<Object> fut = Future<Object?>.value();
  var x = await fut;
  // int i = x; shows that `x` has type `Object`.
  print(x); // 'null'.
}

@Levi-Lesches wrote, about this FutureOr<Object> soundness violation:

So why does await allow this?

The soundness violation could be eliminated in two ways:

  • During the evaluation of await fut, detect that fut is an object with a dynamic type that implements Future<Object?>, compute the T in the await specification to Object, determine that fut is Future<Object> is false, and await Future<Object>.value(fut);. This means that we'd change the behavior of the implementations to match the specification.
  • Change flatten such that flatten(Object) == flatten(FutureOr<Object>) == Object?. In this case we do await the Future<Object?> and get null, but the static type of await fut is now Object? so there is no soundness issue.

The unsound behavior is currently allowed because of a bug. There's no justification for any soundness violation, but the fix could be in the static type of an expression as well as in the dynamic behavior of its evaluation.

eernstg avatar Jul 05 '22 13:07 eernstg

@lrhn wrote:

For await e where e has static type FutureOr<Object>, the specification says to only await a Future<Object>, not a Future<Object?> (which is an Object).

Thinking again, I agree that we should keep the specification exactly as it is for await expressions (in the spec update that adds null safety), and we should only correct flatten to handle type variables and intersection types, and there should not be a new case for Object or FutureOr<Object>.

So we should request that the tools implement the semantics where the dynamic check for Future<T> in the specification of await is performed (of course, in some cases it can be shown at compile-time that it will succeed, in which case it's not necessary to do it at run time, but we should enforce the rule strictly).

The reason why we should do this (rather than changing the static type of await e in some cases) is that the Object exception fails to generalize when we have multiple FutureOr:

void main() async {
  FutureOr<FutureOr<Object>> fut = Future<Object?>.value();
  var x = await fut; // Static type of `x` is `FutureOr<Object>`.
  print(x); // 'null'.
}

The static type of x is FutureOr<Object>, both before the corrections to flatten, with the corrections where type variables and intersection types are taken into account, and with the extra Object item that I proposed (but that I no longer support). So everybody agrees on FutureOr<Object>.

If we want to change flatten in order to eliminate this new soundness violation example, then we would have to ensure that null is flatten(FutureOr<FutureOr<Object>>), e.g., by setting flatten(FutureOr^{k+1}<Object>) == FutureOr^k<Object>? for all k (we'd then have flatten(FutureOr<Object>) == Object? as a special case). But, for soundness, we would also need to include flatten(FutureOr^{k+1}<X>) == FutureOr^k<X>? where X is a type variable whose bound is Object or FutureOr^k<Object> for some k.

It gets silly. ;-)

I think it's better to specify that a Future<Object?> with static type Object (or FutureOr<FutureOr<...<Object>...>>, or one of those other types using a type variable) should not be awaited by await. The above rule about FutureOr<FutureOr<....<Object>...>> and similar types is a non-intuitive exception, which is determined by a deeply nested subterm of the type. In particular, it's triggered by Object or X, and it wouldn't be triggered by any other type T in FutureOr<FutureOr...<T>...>>.


The definition of flatten would then be as follows:

\item If $T$ is a type variable $X$ with bound $B$,
  or $T$ is an intersection type
  (\ref{intersectionTypes})
  \code{$X$\,\,\&\,\,$B$},
  then \DefEquals{\Flatten{$T$}}{\code{\Flatten{$B$}}}.
\item If $T$ is \code{$S$?}\ for some $S$
  then \DefEquals{\Flatten{$T$}}{\code{\Flatten{$S$}?}}.
\item If $T$ is \code{FutureOr<$S$>} then \DefEquals{\Flatten{$T$}}{S}.
\item If $T$ implements \code{Future<$S$>}
  (\ref{interfaceSuperinterfaces})
  then \DefEquals{\Flatten{$T$}}{S}.
\item Otherwise,
  \DefEquals{\Flatten{$T$}}{T}.

that is,

  • If T is a type variable X with bound B, or T is an intersection type (20.14) X & B, then flatten(T) = flatten(B).
  • If T is S? for some S then flatten(T) = flatten(S)?.
  • If T is FutureOr<S> then flatten(T) = S.
  • If T implements Future<S> (11.2) then flatten(T) = S.
  • Otherwise, flatten(T) = T.

eernstg avatar Jul 05 '22 14:07 eernstg

Cf. https://github.com/dart-lang/language/pull/2333.

eernstg avatar Jul 07 '22 10:07 eernstg

Should flatten also be defined for ?/_ (the unknown type used when there is no context type during type inference)?

I think it's not necessary. We only use flatten on the static type of another expression, and the static type of an expression is never ?. We will pick a real type at that point.

lrhn avatar Jul 07 '22 17:07 lrhn

I'm working on an update to the language specification that introduces a number of sections about type inference (to be landed after the null safety updates). I think the need to deal with the unknown type in flatten can be handled as part of that effort.

eernstg avatar Jul 08 '22 07:07 eernstg

Closing: This specification update was landed in https://github.com/dart-lang/language/commit/a3b45ab2bc4e2442c909252858119ffd2e8c685a.

eernstg avatar Dec 02 '22 16:12 eernstg