Skip to content
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

Update flatten definition #2713

Merged
merged 7 commits into from
Dec 13, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion specification/dart.sty
Original file line number Diff line number Diff line change
Expand Up @@ -119,7 +119,8 @@
\newenvironment{commentary}[1]{{\color{commentaryColor}\sf{#1}}}{}

% Auxiliary functions.
\newcommand{\flatten}[1]{\ensuremath{\mbox{\it flatten}({#1})}}
\newcommand{\flattenName}{\mbox{\it flatten}}
\newcommand{\flatten}[1]{\ensuremath{\flattenName({#1})}}
\newcommand{\futureOrBase}[1]{\ensuremath{\mbox{\it futureOrBase}({#1})}}
\newcommand{\overrides}[1]{\ensuremath{\mbox{\it overrides}({#1})}}
\newcommand{\inherited}[1]{\ensuremath{\mbox{\it inherited}({#1})}}
Expand Down
120 changes: 84 additions & 36 deletions specification/dartLangSpec.tex
Original file line number Diff line number Diff line change
Expand Up @@ -11275,35 +11275,62 @@ \subsection{Function Expressions}
where inferred types have already been added.%
}

eernstg marked this conversation as resolved.
Show resolved Hide resolved
\LMHash{}%
We say that $S$ is the
\IndexCustom{future type of a type}{type!future type of}
$T$ in the following cases, using the first applicable case:

\begin{itemize}
\item $T$ implements $S$
(\ref{interfaceSuperinterfaces}),
and there is a $U$ such that $S$ is \code{Future<$U$>}.
\item $T$ is $S$ bounded
(\ref{bindingActualsToFormals}),
and there is a $U$ such that
$S$ is \code{FutureOr<$U$>}, \code{Future<$U$>?}, or \code{FutureOr<$U$>?}.
\end{itemize}

\LMHash{}%
When none of these cases are applicable,
we say that $T$ does not have a future type.

\commentary{%
Note that if $T$ has a future type $F$ then \SubtypeNE{T}{F},
and $F$ is always of the form \code{$G$<...>} or \code{$G$<...>?},
where $G$ is \code{Future} or \code{FutureOr}.%
}

\LMHash{}%
We define the auxiliary function
\IndexCustom{\flatten{T}}{flatten(t)@\emph{flatten}$(T)$},
which is used below and in other sections, as follows:
\IndexCustom{\flatten{T}}{flatten(t)@\emph{flatten}$(T)$}
as follows, using the first applicable case:

\begin{itemize}
\item{} If $T$ is \code{$S$?}\ bounded
(\ref{bindingActualsToFormals})
for some $S$ then \DefEquals{\flatten{T}}{\code{\flatten{S}?}}.
\item If $T$ is \code{$S$?}\ for some $S$
then \DefEquals{\flatten{T}}{\code{\flatten{S}?}}.

\item{} If $T$ is \code{FutureOr<$S$>} bounded
then \DefEquals{\flatten{T}}{S}.
\item If $T$ is \code{$X$\,\&\,$S$}
for some type variable $X$ and type $S$ then
\begin{itemize}
\item if $S$ has future type $U$
then \DefEquals{\flatten{T}}{\code{\flatten{U}}}.
\item otherwise,
\DefEquals{\flatten{T}}{\code{\flatten{X}}}.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

... which falls back to case-analysis on the bound of X, which means we use the bound, even on a promoted type variable, if it's promoted to a non-future-value-having type.

I'd say \DefEquals{\flatten{T}}{\code{X}} to be consistent with what we have now.

Example:

  • Have <X extends FutureOr<Object?>> and X o = ...;
  • Promote o to X & Object by o is Object.
  • Do await o.
  • X&Object has no future value type, so we fall back on flatten(X)
  • X has future type Object?.
  • So await o, with o of type X & Object, has type Object?.

It's not unsound, because a result type of Object? never is, but I'm not absolutely sure it's what we want.
(Not entirely sure it isn't either. But I want to be sure either way.)

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

we fall back on flatten(X)

Yes flatten(X & Object) is flatten(X), because Object does not have a future type.

But X has future type FutureOr<Object?> so flatten(X) is Object?. So await o will await o and get the Object?, statically typed as Object?, which is sound.

I guess you're saying that if the developer tests explicitly for o is Object then we're supposed to forget that we know that anything-X is a Future<Object?> as well.

It is not obvious to me that this would be the natural behavior. I tend to think it's OK to find the future type in the type variable in the case where the other operand of the intersection type doesn't have any.

\end{itemize}

\item{} If $T$ implements \code{Future<$S$>}
(\ref{interfaceSuperinterfaces})
\item If $T$ has future type \code{Future<$S$>}
or \code{FutureOr<$S$>}
then \DefEquals{\flatten{T}}{S}.

\item{} Otherwise, \DefEquals{\flatten{T}}{T}.
\item If $T$ has future type \code{Future<$S$>?}\ or
\code{FutureOr<$S$>?}\ then \DefEquals{\flatten{T}}{\code{$S$?}}.
eernstg marked this conversation as resolved.
Show resolved Hide resolved

\item Otherwise, \DefEquals{\flatten{T}}{T}.
\end{itemize}

\commentary{%
\rationale{%
This definition guarantees that for any type $T$,
\code{$T <:$ FutureOr<$\flatten{T}$>}.
Note that when $X$ is a type variable with bound $B$,
it is possible that \flatten{X} is different from $X$:
$B$ could, for some $S$, be \code{FutureOr<$S$>},
or a type variable $Y$ with bound \code{FutureOr<$S$>},
or a class $C$ that implements \code{Future<$S$>},
or a type variable $X$ with bound $C$.%
\code{$T <:$ FutureOr<$\flatten{T}$>}.%
}

\LMHash{}%
Expand Down Expand Up @@ -15992,27 +16019,25 @@ \subsection{Await Expressions}
\end{grammar}

\LMHash{}%
Evaluation of an await expression $a$ of the form \code{\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}
(\flatten{} is defined in section \ref{functionExpressions}).
It is a dynamic type error if the run-time type of $o$ is not a subtype
of \code{FutureOr<$T$>} \commentary{(that is, if it is neither a subtype
of $T$ nor of \code{Future<$T$>})}.
\BlindDefineSymbol{a, e, S}%
Let $a$ be an expression of the form \code{\AWAIT\,\,$e$}.
Let $S$ be the static type of $e$.
The static type of $a$ is then \flatten{S}
(\ref{functionExpressions}).

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

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

% Otherwise, the value of $a$ is the value of $e$. If evaluation of
% $e$ raises an exception $x$, $a$ raises $x$.
\rationale{%
The use of \flattenName{} to find $T$ and hence determine the dynamic type test
implies that we await a future in every case where this choice is sound.%
}

\commentary{%
An interesting case on the edge of this trade-off is when $e$
has the static type \code{FutureOr<Object>?}.
You could say that the intention behind this type is that
the value of $e$ is a \code{Future<Object>},
or it is an \code{Object} which is not a future,
or it is \NULL.
So, presumably, we should await the first kind,
and we should pass on the second and third kind unchanged.
However, the second kind could be a \code{Future<Object?>}.
This object isn't a \code{Future<Object>}, and it isn't \NULL,
so it \emph{must} be considered to be in the second group.
Nevertheless, \flatten{\code{FutureOr<Object>?}} is \code{Object?},
so we \emph{will} await a \code{Future<Object?>}.
We have chosen this semantics because it was the smallest breaking change
relative to the semantics in earlier versions of Dart,
and also because it allows for a simple rule:
The type of \code{\AWAIT\,\,$e$} is used to decide whether or not
the future (if any) is awaited, and there are no exceptions---even
in cases like this example, where the type seems to imply that
a \code{Future<Object?>} should not be awaited.
In summary, we await every future that we can soundly await.%
}

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

\LMHash{}%
The static type of $a$ is $T$.


\subsection{Postfix Expressions}
\LMLabel{postfixExpressions}
Expand Down