From 9c3c9e9ff2a261aef211484ad8c352f3a67672d3 Mon Sep 17 00:00:00 2001 From: Erik Ernst Date: Mon, 12 Dec 2022 00:01:01 +0100 Subject: [PATCH 1/7] Updated flatten definition --- specification/dartLangSpec.tex | 51 ++++++++++++++++++++++++---------- 1 file changed, 36 insertions(+), 15 deletions(-) diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex index c1aecd6ac2..150d5edcb5 100644 --- a/specification/dartLangSpec.tex +++ b/specification/dartLangSpec.tex @@ -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. +\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}}}. + \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{% 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{}% From 03375fa83c6bd766f8800bd37a9a3357c492552f Mon Sep 17 00:00:00 2001 From: Erik Ernst Date: Tue, 13 Dec 2022 14:50:18 +0100 Subject: [PATCH 2/7] Review response --- specification/dart.sty | 3 +- specification/dartLangSpec.tex | 52 ++++++++++++++++++++++++---------- 2 files changed, 39 insertions(+), 16 deletions(-) diff --git a/specification/dart.sty b/specification/dart.sty index bad61657c2..7896caccd6 100644 --- a/specification/dart.sty +++ b/specification/dart.sty @@ -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})}} diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex index 150d5edcb5..9879f010e3 100644 --- a/specification/dartLangSpec.tex +++ b/specification/dartLangSpec.tex @@ -11322,7 +11322,7 @@ \subsection{Function Expressions} \item Otherwise, \DefEquals{\flatten{T}}{T}. \end{itemize} -\commentary{% +\rationale{% This definition guarantees that for any type $T$, \code{$T <:$ FutureOr<$\flatten{T}$>}.% } @@ -16013,25 +16013,50 @@ \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$ of proceeds as follows: +First, the expression $e$ is evaluated to an object $o$. +Let $T$ be \flatten{S}. If the run-time type of $o$ is a subtype of \code{Future<$T$>}, then let $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. +\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?}. +You could say that the intention behind this type is that +the value of $e$ is a \code{Future}, +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}. +This object isn't a \code{Future}, and it isn't \NULL, +so it \emph{must} be considered to be in the second group. +Nevertheless, \flatten{\code{FutureOr?}} is \code{Object?}, +so we \emph{will} await the future. +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} should not be awaited.% +} + \LMHash{}% Next, the stream associated with the innermost enclosing asynchronous for loop (\ref{asynchronousFor-in}), @@ -16068,9 +16093,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} From 2f0b777a15f8dff9f79b75a8957e398daddd406f Mon Sep 17 00:00:00 2001 From: Erik Ernst Date: Tue, 13 Dec 2022 14:58:30 +0100 Subject: [PATCH 3/7] Typos; move commentary, keeping normative text in one place --- specification/dartLangSpec.tex | 35 ++++++++++++++++------------------ 1 file changed, 16 insertions(+), 19 deletions(-) diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex index 9879f010e3..20663c307f 100644 --- a/specification/dartLangSpec.tex +++ b/specification/dartLangSpec.tex @@ -16020,15 +16020,27 @@ \subsection{Await Expressions} (\ref{functionExpressions}). \LMHash{}% -Evaluation of $a$ of proceeds as follows: +Evaluation of $a$ proceeds as follows: First, the expression $e$ is evaluated to an object $o$. -Let $T$ be \flatten{S}. +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 +(\ref{asynchronousFor-in}), +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$ +(\ref{expressionEvaluation}). +If $f$ completes with an object $v$, $a$ evaluates to $v$. + \rationale{% This use of \flattenName{} implies that we await a future in every case where this choice is sound.% @@ -16047,7 +16059,7 @@ \subsection{Await Expressions} This object isn't a \code{Future}, and it isn't \NULL, so it \emph{must} be considered to be in the second group. Nevertheless, \flatten{\code{FutureOr?}} is \code{Object?}, -so we \emph{will} await the future. +so we \emph{will} await a \code{Future}. 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: @@ -16057,21 +16069,6 @@ \subsection{Await Expressions} a \code{Future} should not be awaited.% } -\LMHash{}% -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$ -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$ -(\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$. - \commentary{% An await expression can only occur in a function which is declared asynchronous. The \AWAIT{} identifier has has no special meaning From 0cd0960ef4410b2a0bfb56122d008ba571ddc6d1 Mon Sep 17 00:00:00 2001 From: Erik Ernst Date: Tue, 13 Dec 2022 15:00:50 +0100 Subject: [PATCH 4/7] Correct font of keyword --- specification/dartLangSpec.tex | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex index 20663c307f..7ebda72445 100644 --- a/specification/dartLangSpec.tex +++ b/specification/dartLangSpec.tex @@ -16030,7 +16030,8 @@ \subsection{Await Expressions} 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$ From 5f1c339d278085953ea0de08fc11a1856631b139 Mon Sep 17 00:00:00 2001 From: Erik Ernst Date: Tue, 13 Dec 2022 17:08:44 +0100 Subject: [PATCH 5/7] Review response --- specification/dartLangSpec.tex | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex index 7ebda72445..8da7e2fe31 100644 --- a/specification/dartLangSpec.tex +++ b/specification/dartLangSpec.tex @@ -16043,8 +16043,8 @@ \subsection{Await Expressions} If $f$ completes with an object $v$, $a$ evaluates to $v$. \rationale{% -This use of \flattenName{} implies that we await a future -in every case where this choice is sound.% +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{% @@ -16067,7 +16067,8 @@ \subsection{Await Expressions} 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} should not be awaited.% +a \code{Future} should not be awaited. +In summary, we await every future that we can soundly await.% } \commentary{% From 49307eacb74305fa5d3ac653dbcb48957cbf6a6a Mon Sep 17 00:00:00 2001 From: Erik Ernst Date: Tue, 13 Dec 2022 18:03:22 +0100 Subject: [PATCH 6/7] Simplified "future type of T" --- specification/dartLangSpec.tex | 35 +++++++++++++++++----------------- 1 file changed, 18 insertions(+), 17 deletions(-) diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex index 8da7e2fe31..b72d7d91d6 100644 --- a/specification/dartLangSpec.tex +++ b/specification/dartLangSpec.tex @@ -11276,34 +11276,35 @@ \subsection{Function Expressions} } \LMHash{}% -We define the +We say that $S$ is the \IndexCustom{future type of a type}{type!future type of} -$T$ as follows: +$T$ in the following cases, using the first applicable case: \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. +\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}.} + \LMHash{}% We define the auxiliary function \IndexCustom{\flatten{T}}{flatten(t)@\emph{flatten}$(T)$}, -which is used below and in other sections, as follows: +as follows, again using the first applicable case: \begin{itemize} \item If $T$ is \code{$S$?}\ for some $S$ then \DefEquals{\flatten{T}}{\code{\flatten{S}?}}. -\item Otherwise, if $T$ is \code{$X$\,\,\&\,\,$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$ @@ -11312,11 +11313,11 @@ \subsection{Function Expressions} \DefEquals{\flatten{T}}{\code{\flatten{X}}}. \end{itemize} -\item Otherwise, if $T$ has future type \code{Future<$S$>} +\item If $T$ has future type \code{Future<$S$>} or \code{FutureOr<$S$>} then \DefEquals{\flatten{T}}{S}. -\item Otherwise, if $T$ has future type \code{Future<$S$>?}\ or +\item If $T$ has future type \code{Future<$S$>?}\ or \code{FutureOr<$S$>?}\ then \DefEquals{\flatten{T}}{\code{$S$?}}. \item Otherwise, \DefEquals{\flatten{T}}{T}. From 4f450ab2e82f8a10ee7b7eb9f8378c1f7af0cef9 Mon Sep 17 00:00:00 2001 From: Erik Ernst Date: Tue, 13 Dec 2022 18:11:26 +0100 Subject: [PATCH 7/7] Improve commentary --- specification/dartLangSpec.tex | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex index b72d7d91d6..95359d933e 100644 --- a/specification/dartLangSpec.tex +++ b/specification/dartLangSpec.tex @@ -11293,12 +11293,17 @@ \subsection{Function Expressions} \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}.} + +\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)$}, -as follows, again using the first applicable case: +\IndexCustom{\flatten{T}}{flatten(t)@\emph{flatten}$(T)$} +as follows, using the first applicable case: \begin{itemize} \item If $T$ is \code{$S$?}\ for some $S$