From 59ed20927bd2213a16d7954b302b3f2033ceb339 Mon Sep 17 00:00:00 2001 From: "Lasse R.H. Nielsen" Date: Thu, 7 Jul 2022 10:37:11 +0200 Subject: [PATCH 1/8] Breaking change to await, update to flatten. Changes **flatten** to be specified for a static type which is a type variable. Changes `await` to throw when provided a `Future` value of a type that could provide an unsound value if awaited. This differes from the current specification, which instead treats the future as a value, so `await someFuture` can evaluate to `someFuture`. It also differs from the current implementation, which awaits `someFuture` to its value, whether the result is sound or not. The result *can* be sound. Compare: ```dart Object o = await (Future.value(3) as FutureOr.value(null) as FutureOr} for some $S$ then $\flatten{T} = S$. +\item If $T$ is a type variable $X$ with bound $B$, + or $T$ is a promoted type variable $X & B$, + then $\flatten{T} = \flatten{B}$. -\item Otherwise if - \code{$T <:$ Future} - then let $S$ be a type such that - \code{$T <:$ Future<$S$>} - and for all $R$, if - \code{$T <:$ Future<$R$>} - then $S <: R$. +\item Otherwise if $T$ is \code{FutureOr<$S$>} for some $S$ + then $\flatten{T} = S$. - \rationale{% - This ensures that - \code{Future<$S$>} - is the most specific generic instantiation of \code{Future} that is - a supertype of $T$. - %% TODO[class-interfaces]: When we have finished the specification of class - %% interface computations we may have the following property, but it is not - %% true at this point. Adjust the following by then! - Note that $S$ is well-defined because of - the requirements on superinterfaces.% - } - - Then $\flatten{T} = S$. +\item Otherwise if $T$ implements \code{Future<$S$>} for some $S$ + (\ref{interfaceSuperinterfaces}) then $\flatten{T} = S$. \item In any other circumstance, $\flatten{T} = T$. \end{itemize} +\commentary{% +This definition guarantees that for any type $T$, +\code{$T <:$ FutureOr<$\flatten{T}$>}.% +} + \LMHash{}% \Case{Positional, arrow} The static type of a function literal of the form @@ -13755,7 +13746,7 @@ \subsubsection{Ordinary Invocation} } \commentary{% -An member access on a type literal +An member access on a type literal (e.g., \code{C.id()}, \code{C.id}, or \code{C?.id()}), always treats the declaration denoted by the literal as a namespace for accessing static members or constructors. @@ -15993,11 +15984,15 @@ \subsection{Await Expressions} % 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. -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. +Let $R$ be the run-time type of $o$. +If $R$ implements \code{Future<$S$>} for some $S$ +(\ref{interfaceSuperinterfaces}) then +it is a dynamic type error if $S$ is not a subtype of $T$. +If $S$ is a subtype of $T$, let $f$ be $o$. + +Otherwise (when $R$ does not implement \code{Future}), +let $f$ be a future object, implementing \code{Future<$T$>}, +which is completed with the value $o$. \LMHash{}% Next, the stream associated with the innermost enclosing asynchronous for loop From c4dfb5728b008d043e59a8ce620df38b9af2afac Mon Sep 17 00:00:00 2001 From: "Lasse R.H. Nielsen" Date: Thu, 7 Jul 2022 11:43:05 +0200 Subject: [PATCH 2/8] Update specification/dartLangSpec.tex Co-authored-by: Erik Ernst --- specification/dartLangSpec.tex | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex index f325128a9e..b6afd594ba 100644 --- a/specification/dartLangSpec.tex +++ b/specification/dartLangSpec.tex @@ -15988,7 +15988,9 @@ \subsection{Await Expressions} If $R$ implements \code{Future<$S$>} for some $S$ (\ref{interfaceSuperinterfaces}) then it is a dynamic type error if $S$ is not a subtype of $T$. -If $S$ is a subtype of $T$, let $f$ be $o$. +Otherwise +(\commentary{if no run-time error occurred}), +let $f$ be $o$. Otherwise (when $R$ does not implement \code{Future}), let $f$ be a future object, implementing \code{Future<$T$>}, From 20b68956f138e3ad3d3e653243d82df425abbefa Mon Sep 17 00:00:00 2001 From: "Lasse R.H. Nielsen" Date: Thu, 7 Jul 2022 11:46:38 +0200 Subject: [PATCH 3/8] Update specification/dartLangSpec.tex Co-authored-by: Erik Ernst --- specification/dartLangSpec.tex | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex index b6afd594ba..21b0b04bc5 100644 --- a/specification/dartLangSpec.tex +++ b/specification/dartLangSpec.tex @@ -11268,7 +11268,9 @@ \subsection{Function Expressions} \begin{itemize} \item If $T$ is a type variable $X$ with bound $B$, - or $T$ is a promoted type variable $X & B$, + or $T$ is an intersection type + (\ref{intersectionTypes}) + \code{$X$\,\,\&\,\,$B$}, then $\flatten{T} = \flatten{B}$. \item Otherwise if $T$ is \code{FutureOr<$S$>} for some $S$ From 46705f2d4691580e0683ea74484b0f7ecf8a0ef8 Mon Sep 17 00:00:00 2001 From: "Lasse R.H. Nielsen" Date: Thu, 7 Jul 2022 11:46:56 +0200 Subject: [PATCH 4/8] Update specification/dartLangSpec.tex Co-authored-by: Erik Ernst --- specification/dartLangSpec.tex | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex index 21b0b04bc5..ca81c296da 100644 --- a/specification/dartLangSpec.tex +++ b/specification/dartLangSpec.tex @@ -15994,7 +15994,8 @@ \subsection{Await Expressions} (\commentary{if no run-time error occurred}), let $f$ be $o$. -Otherwise (when $R$ does not implement \code{Future}), +Otherwise +(\commentary{when $R$ does not implement \code{Future}}), let $f$ be a future object, implementing \code{Future<$T$>}, which is completed with the value $o$. From 30c6debc63531c0e988cdd3e40b44c0da49345c3 Mon Sep 17 00:00:00 2001 From: "Lasse R.H. Nielsen" Date: Thu, 7 Jul 2022 11:47:19 +0200 Subject: [PATCH 5/8] Update specification/dartLangSpec.tex Co-authored-by: Erik Ernst --- specification/dartLangSpec.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex index ca81c296da..63d3d668ef 100644 --- a/specification/dartLangSpec.tex +++ b/specification/dartLangSpec.tex @@ -15996,7 +15996,7 @@ \subsection{Await Expressions} Otherwise (\commentary{when $R$ does not implement \code{Future}}), -let $f$ be a future object, implementing \code{Future<$T$>}, +let $f$ be an object whose run-time type implements \code{Future<$T$>}, which is completed with the value $o$. \LMHash{}% From b250a6888dbcde7637921d66348d4376fc532649 Mon Sep 17 00:00:00 2001 From: "Lasse R.H. Nielsen" Date: Thu, 7 Jul 2022 11:47:32 +0200 Subject: [PATCH 6/8] Update specification/dartLangSpec.tex Co-authored-by: Erik Ernst --- specification/dartLangSpec.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex index 63d3d668ef..4cc551948f 100644 --- a/specification/dartLangSpec.tex +++ b/specification/dartLangSpec.tex @@ -13748,7 +13748,7 @@ \subsubsection{Ordinary Invocation} } \commentary{% -An member access on a type literal +A member access on a type literal (e.g., \code{C.id()}, \code{C.id}, or \code{C?.id()}), always treats the declaration denoted by the literal as a namespace for accessing static members or constructors. From ffab46807915ac109b48663b4b2c9acf6e9f9c59 Mon Sep 17 00:00:00 2001 From: "Lasse R.H. Nielsen" Date: Thu, 7 Jul 2022 11:57:50 +0200 Subject: [PATCH 7/8] Use `\DefEquals`. --- specification/dart.sty | 8 +++++++- specification/dartLangSpec.tex | 15 +++++++++------ 2 files changed, 16 insertions(+), 7 deletions(-) diff --git a/specification/dart.sty b/specification/dart.sty index 299c8c53e0..bad61657c2 100644 --- a/specification/dart.sty +++ b/specification/dart.sty @@ -281,7 +281,7 @@ % name of optional parameters, number of optional parameters. \newcommand{\FunctionTypeNamedArguments}[4]{% \List{#1}{1}{#2},\ \{\PairList{#1}{#3}{{#2}+1}{{#2}+{#4}}\}} - + \newcommand{\FunctionTypeNamedArgumentsStd}{% \FunctionTypeNamedArguments{T}{n}{x}{k}} @@ -387,6 +387,12 @@ \newcommand{\EvaluateElementName}{\metavar{evaluateElement}} \newcommand{\EvaluateElement}[1]{\ensuremath{\EvaluateElementName({#1})}} +\newcommand{\DefEquals}[2]{\ensuremath{{#1}\stackrel{\vartriangle}{=}{#2}}} +\newcommand{\DefEqualsNewline}[2]{ + \ensuremath{{#1}\stackrel{\vartriangle}{=}}\\ + \ensuremath{{#2}}% +} + % ---------------------------------------------------------------------- % Support for hash valued Location Markers diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex index 4cc551948f..e2d9f1be31 100644 --- a/specification/dartLangSpec.tex +++ b/specification/dartLangSpec.tex @@ -11271,15 +11271,18 @@ \subsection{Function Expressions} or $T$ is an intersection type (\ref{intersectionTypes}) \code{$X$\,\,\&\,\,$B$}, - then $\flatten{T} = \flatten{B}$. + then \DefEquals{\flatten{$T$}}{\code{\flatten{$B$}}}. -\item Otherwise if $T$ is \code{FutureOr<$S$>} for some $S$ - then $\flatten{T} = S$. +\item If $T$ is \code{$S$?}\ for some $S$ + then \DefEquals{\flatten{$T$}}{\code{\flatten{$S$}?}}. -\item Otherwise if $T$ implements \code{Future<$S$>} for some $S$ - (\ref{interfaceSuperinterfaces}) then $\flatten{T} = S$. +\item If $T$ is \code{FutureOr<$S$>} then \DefEquals{\flatten{$T$}}{S}. -\item In any other circumstance, $\flatten{T} = T$. +\item If $T$ implements \code{Future<$S$>} + (\ref{interfaceSuperinterfaces}) + then \DefEquals{\flatten{$T$}}{S}. + +\item Otherwise, \DefEquals{\flatten{$T$}}{T}. \end{itemize} \commentary{% From 9733ae87e33c15724d7b8da0ca205840a4710e88 Mon Sep 17 00:00:00 2001 From: "Lasse R.H. Nielsen" Date: Thu, 7 Jul 2022 13:15:25 +0200 Subject: [PATCH 8/8] Math modes --- specification/dartLangSpec.tex | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/specification/dartLangSpec.tex b/specification/dartLangSpec.tex index e2d9f1be31..ec9cfc9c3f 100644 --- a/specification/dartLangSpec.tex +++ b/specification/dartLangSpec.tex @@ -11267,22 +11267,22 @@ \subsection{Function Expressions} which is used below and in other sections, as follows: \begin{itemize} -\item If $T$ is a type variable $X$ with bound $B$, +\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$}}}. + then \DefEquals{\flatten{T}}{\flatten{B}}. -\item If $T$ is \code{$S$?}\ 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$>} then \DefEquals{\flatten{$T$}}{S}. +\item{} If $T$ is \code{FutureOr<$S$>} then \DefEquals{\flatten{T}}{S}. -\item If $T$ implements \code{Future<$S$>} +\item{} If $T$ implements \code{Future<$S$>} (\ref{interfaceSuperinterfaces}) - then \DefEquals{\flatten{$T$}}{S}. + then \DefEquals{\flatten{T}}{S}. -\item Otherwise, \DefEquals{\flatten{$T$}}{T}. +\item{} Otherwise, \DefEquals{\flatten{T}}{T}. \end{itemize} \commentary{%