Skip to content

Update flatten definition #2713

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.

Sign up for GitHub

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

Merged
merged 7 commits into from
Dec 13, 2022
Merged

Update flatten definition #2713

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
9c3c9e9
Updated flatten definition
eernstg Dec 11, 2022
03375fa
Review response
eernstg Dec 13, 2022
2f0b777
Typos; move commentary, keeping normative text in one place
eernstg Dec 13, 2022
0cd0960
Correct font of keyword
eernstg Dec 13, 2022
5f1c339
Review response
eernstg Dec 13, 2022
49307ea
Simplified "future type of T"
eernstg Dec 13, 2022
4f450ab
Improve commentary
eernstg Dec 13, 2022
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
View file
Open in desktop
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
109 changes: 75 additions & 34 deletions specification/dartLangSpec.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11275,35 +11275,56 @@ \subsection{Function Expressions}
where inferred types have already been added.%
}

\LMHash{}%
We define the
\IndexCustom{future type of a type}{type!future type of}
$T$ as follows:

\begin{itemize}
\item If $T$ implements \code{Future<$S$>}
(\ref{interfaceSuperinterfaces})
then the future type of $T$ is \code{Future<$S$>}.
\item Otherwise, if $T$ is \code{FutureOr<$S$>} bounded
(\ref{bindingActualsToFormals})
then the future type of $T$ is \code{FutureOr<$S$>}.
\item Otherwise, if $T$ is \code{Future<$S$>?} bounded
or \code{FutureOr<$S$>?} bounded
then the future type of $T$ is \code{Future<$S$>?}
respectively \code{FutureOr<$S$>?}.
\item Otherwise, $T$ has no future type.
Copy link
Member

Choose a reason for hiding this comment

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

Does not seem to account for X? or (X & B)? (if that exists), because those are not bounded by anything but themselves (they are not type variables or promoted type variables, they just contain some, so the last two clauses of "is-S-bounded" do not apply), and they have no super-interfaces.

Maybe:

  • If T implements Future<S> for some S, T has future type Future<S>.
  • Otherwise, if T is FutureOr<S> for some S, T has future type Future<S>.
  • Otherwise, if T is B bounded for some B and B has future type F, so does T.
  • Otherwise, if T is R? and R has future type F, T has future type F?.
  • Otherwise T has no future type.

Copy link
Member Author

Choose a reason for hiding this comment

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

X? is handled by the first case in flatten, X? does not have a future type of its own.

(X & B)? cannot occur, intersection types are designed to be top-level only.

About the rulesets:

If T implements Future<S> for some S, T has future type Future<S>.

This is my first item.

Otherwise, if T is FutureOr<S> for some S, T has future type Future<S>.

This is different, but flatten would take those two different intermediate results to the same end result.

Otherwise, if T is B bounded for some B and B has future type F, so does T.

This is somewhat redundant: It may include a usage of the first item, but it would then already be covered by the first item.

Otherwise, if T is R? and R has future type F, T has future type F?.

I could use this to make the third item simpler, but it would only be applicable in some cases after having applied item 2.

Otherwise T has no future type.

OK, I don't see any discrepancies so we could use one or the other definition, but it's not obvious to me that this one is simpler to reason about.

\end{itemize}

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

\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 Otherwise, 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 Otherwise, if $T$ has future type \code{Future<$S$>}
or \code{FutureOr<$S$>}
then \DefEquals{\flatten{T}}{S}.

\item{} Otherwise, \DefEquals{\flatten{T}}{T}.
\item Otherwise, if $T$ has future type \code{Future<$S$>?}\ or
\code{FutureOr<$S$>?}\ then \DefEquals{\flatten{T}}{\code{$S$?}}.

\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 +16013,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 +16042,33 @@ \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{%
This use of \flattenName{} 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.%
}

\commentary{%
An await expression can only occur in a function which is declared
Expand All @@ -16047,9 +16091,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