Skip to content

Commit 0cff768

Browse files
authored
Update flatten definition (#2713)
Update the definition of the type function `flatten` such that it handles intersection types and type variables in a way that is still sound, but which preserves the type of the operand of `await` much better than the previous approach. This PR also introduces the notion of 'the future type of a type', which makes it considerably simpler to reason about `flatten` and `await`, because it now consists of two clearly separated simpler steps.
1 parent 64ce120 commit 0cff768

File tree

2 files changed

+86
-37
lines changed

2 files changed

+86
-37
lines changed

specification/dart.sty

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -119,7 +119,8 @@
119119
\newenvironment{commentary}[1]{{\color{commentaryColor}\sf{#1}}}{}
120120

121121
% Auxiliary functions.
122-
\newcommand{\flatten}[1]{\ensuremath{\mbox{\it flatten}({#1})}}
122+
\newcommand{\flattenName}{\mbox{\it flatten}}
123+
\newcommand{\flatten}[1]{\ensuremath{\flattenName({#1})}}
123124
\newcommand{\futureOrBase}[1]{\ensuremath{\mbox{\it futureOrBase}({#1})}}
124125
\newcommand{\overrides}[1]{\ensuremath{\mbox{\it overrides}({#1})}}
125126
\newcommand{\inherited}[1]{\ensuremath{\mbox{\it inherited}({#1})}}

specification/dartLangSpec.tex

Lines changed: 84 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -11275,35 +11275,62 @@ \subsection{Function Expressions}
1127511275
where inferred types have already been added.%
1127611276
}
1127711277

11278+
\LMHash{}%
11279+
We say that $S$ is the
11280+
\IndexCustom{future type of a type}{type!future type of}
11281+
$T$ in the following cases, using the first applicable case:
11282+
11283+
\begin{itemize}
11284+
\item $T$ implements $S$
11285+
(\ref{interfaceSuperinterfaces}),
11286+
and there is a $U$ such that $S$ is \code{Future<$U$>}.
11287+
\item $T$ is $S$ bounded
11288+
(\ref{bindingActualsToFormals}),
11289+
and there is a $U$ such that
11290+
$S$ is \code{FutureOr<$U$>}, \code{Future<$U$>?}, or \code{FutureOr<$U$>?}.
11291+
\end{itemize}
11292+
11293+
\LMHash{}%
11294+
When none of these cases are applicable,
11295+
we say that $T$ does not have a future type.
11296+
11297+
\commentary{%
11298+
Note that if $T$ has a future type $F$ then \SubtypeNE{T}{F},
11299+
and $F$ is always of the form \code{$G$<...>} or \code{$G$<...>?},
11300+
where $G$ is \code{Future} or \code{FutureOr}.%
11301+
}
11302+
1127811303
\LMHash{}%
1127911304
We define the auxiliary function
11280-
\IndexCustom{\flatten{T}}{flatten(t)@\emph{flatten}$(T)$},
11281-
which is used below and in other sections, as follows:
11305+
\IndexCustom{\flatten{T}}{flatten(t)@\emph{flatten}$(T)$}
11306+
as follows, using the first applicable case:
1128211307

1128311308
\begin{itemize}
11284-
\item{} If $T$ is \code{$S$?}\ bounded
11285-
(\ref{bindingActualsToFormals})
11286-
for some $S$ then \DefEquals{\flatten{T}}{\code{\flatten{S}?}}.
11309+
\item If $T$ is \code{$S$?}\ for some $S$
11310+
then \DefEquals{\flatten{T}}{\code{\flatten{S}?}}.
1128711311

11288-
\item{} If $T$ is \code{FutureOr<$S$>} bounded
11289-
then \DefEquals{\flatten{T}}{S}.
11312+
\item If $T$ is \code{$X$\,\&\,$S$}
11313+
for some type variable $X$ and type $S$ then
11314+
\begin{itemize}
11315+
\item if $S$ has future type $U$
11316+
then \DefEquals{\flatten{T}}{\code{\flatten{U}}}.
11317+
\item otherwise,
11318+
\DefEquals{\flatten{T}}{\code{\flatten{X}}}.
11319+
\end{itemize}
1129011320

11291-
\item{} If $T$ implements \code{Future<$S$>}
11292-
(\ref{interfaceSuperinterfaces})
11321+
\item If $T$ has future type \code{Future<$S$>}
11322+
or \code{FutureOr<$S$>}
1129311323
then \DefEquals{\flatten{T}}{S}.
1129411324

11295-
\item{} Otherwise, \DefEquals{\flatten{T}}{T}.
11325+
\item If $T$ has future type \code{Future<$S$>?}\ or
11326+
\code{FutureOr<$S$>?}\ then \DefEquals{\flatten{T}}{\code{$S$?}}.
11327+
11328+
\item Otherwise, \DefEquals{\flatten{T}}{T}.
1129611329
\end{itemize}
1129711330

11298-
\commentary{%
11331+
\rationale{%
1129911332
This definition guarantees that for any type $T$,
11300-
\code{$T <:$ FutureOr<$\flatten{T}$>}.
11301-
Note that when $X$ is a type variable with bound $B$,
11302-
it is possible that \flatten{X} is different from $X$:
11303-
$B$ could, for some $S$, be \code{FutureOr<$S$>},
11304-
or a type variable $Y$ with bound \code{FutureOr<$S$>},
11305-
or a class $C$ that implements \code{Future<$S$>},
11306-
or a type variable $X$ with bound $C$.%
11333+
\code{$T <:$ FutureOr<$\flatten{T}$>}.%
1130711334
}
1130811335

1130911336
\LMHash{}%
@@ -15992,27 +16019,25 @@ \subsection{Await Expressions}
1599216019
\end{grammar}
1599316020

1599416021
\LMHash{}%
15995-
Evaluation of an await expression $a$ of the form \code{\AWAIT{} $e$}
15996-
where $e$ has static type $S$ proceeds as follows:
15997-
First, the expression $e$ is evaluated to an object $o$.
15998-
Let $T$ be \flatten{S}
15999-
(\flatten{} is defined in section \ref{functionExpressions}).
16000-
It is a dynamic type error if the run-time type of $o$ is not a subtype
16001-
of \code{FutureOr<$T$>} \commentary{(that is, if it is neither a subtype
16002-
of $T$ nor of \code{Future<$T$>})}.
16022+
\BlindDefineSymbol{a, e, S}%
16023+
Let $a$ be an expression of the form \code{\AWAIT\,\,$e$}.
16024+
Let $S$ be the static type of $e$.
16025+
The static type of $a$ is then \flatten{S}
16026+
(\ref{functionExpressions}).
1600316027

1600416028
\LMHash{}%
16005-
% NOTICE: Removed the requirement that an error thrown by $e$ is caught in a
16006-
% future. There is no reason $var x = e; await x;$ and $await e$ should behave
16007-
% differently, and no implementation actually implemented it.
16029+
Evaluation of $a$ proceeds as follows:
16030+
First, the expression $e$ is evaluated to an object $o$.
16031+
Let \DefineSymbol{T} be \flatten{S}.
1600816032
If the run-time type of $o$ is a subtype of \code{Future<$T$>},
16009-
then let $f$ be $o$;
16033+
then let \DefineSymbol{f} be $o$;
1601016034
otherwise let $f$ be the result of creating
1601116035
a new object using the constructor \code{Future<$T$>.value()}
1601216036
with $o$ as its argument.
1601316037

1601416038
\LMHash{}%
16015-
Next, the stream associated with the innermost enclosing asynchronous for loop
16039+
Next, the stream associated with
16040+
the innermost enclosing asynchronous \FOR{} loop
1601616041
(\ref{asynchronousFor-in}),
1601716042
if any, is paused.
1601816043
The current invocation of the function body immediately enclosing $a$
@@ -16023,8 +16048,34 @@ \subsection{Await Expressions}
1602316048
(\ref{expressionEvaluation}).
1602416049
If $f$ completes with an object $v$, $a$ evaluates to $v$.
1602516050

16026-
% Otherwise, the value of $a$ is the value of $e$. If evaluation of
16027-
% $e$ raises an exception $x$, $a$ raises $x$.
16051+
\rationale{%
16052+
The use of \flattenName{} to find $T$ and hence determine the dynamic type test
16053+
implies that we await a future in every case where this choice is sound.%
16054+
}
16055+
16056+
\commentary{%
16057+
An interesting case on the edge of this trade-off is when $e$
16058+
has the static type \code{FutureOr<Object>?}.
16059+
You could say that the intention behind this type is that
16060+
the value of $e$ is a \code{Future<Object>},
16061+
or it is an \code{Object} which is not a future,
16062+
or it is \NULL.
16063+
So, presumably, we should await the first kind,
16064+
and we should pass on the second and third kind unchanged.
16065+
However, the second kind could be a \code{Future<Object?>}.
16066+
This object isn't a \code{Future<Object>}, and it isn't \NULL,
16067+
so it \emph{must} be considered to be in the second group.
16068+
Nevertheless, \flatten{\code{FutureOr<Object>?}} is \code{Object?},
16069+
so we \emph{will} await a \code{Future<Object?>}.
16070+
We have chosen this semantics because it was the smallest breaking change
16071+
relative to the semantics in earlier versions of Dart,
16072+
and also because it allows for a simple rule:
16073+
The type of \code{\AWAIT\,\,$e$} is used to decide whether or not
16074+
the future (if any) is awaited, and there are no exceptions---even
16075+
in cases like this example, where the type seems to imply that
16076+
a \code{Future<Object?>} should not be awaited.
16077+
In summary, we await every future that we can soundly await.%
16078+
}
1602816079

1602916080
\commentary{%
1603016081
An await expression can only occur in a function which is declared
@@ -16047,9 +16098,6 @@ \subsection{Await Expressions}
1604716098
Tools may choose to give a hint in such cases.%
1604816099
}
1604916100

16050-
\LMHash{}%
16051-
The static type of $a$ is $T$.
16052-
1605316101

1605416102
\subsection{Postfix Expressions}
1605516103
\LMLabel{postfixExpressions}

0 commit comments

Comments
 (0)