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

Specify yield* and await for in more detail. #1527

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
110 changes: 76 additions & 34 deletions specification/dartLangSpec.tex
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,7 @@
% - Add requirement that the iterator of a for-in statement must have
% type `Iterator`.
% - Clarify which constructors are covered by the section 'Constant
% Constructors' and removed confusing redundancy in definiton of
% Constructors' and removed confusing redundancy in definition of
Copy link
Member

Choose a reason for hiding this comment

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

Might as well fix and removed --> , and remove.

Copy link
Member Author

Choose a reason for hiding this comment

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

Well spotted.

% potentially constant expressions.
% - Integrate the feature specification of collection literal elements
% (aka UI-as-code).
Expand Down Expand Up @@ -1717,7 +1717,7 @@ \subsection{Function Declarations}
with the built-in identifier \STATIC{}.

\LMHash{}%
When we say that a function $f_1$ \Index{forwards} to another function $f_2$,
When we say that a function $f_1$ \Index{forwards} to another function $f_2$,
we mean that invoking $f_1$ causes $f_2$ to be executed
with the same arguments and/or receiver as $f_1$,
and returns the result of executing $f_2$ to the caller of $f_1$,
Expand Down Expand Up @@ -1952,7 +1952,7 @@ \subsubsection{Optional Formals}
callers from outside the library where it was defined.
If a method outside the library overrode a method with a private optional name,
it would not be a subtype of the original method.
The static checker would of course flag such situations,
The static checker would of course flag such situations,
but the consequence would be that adding a private named formal would break
clients outside the library in a way they could not easily correct.%
}
Expand Down Expand Up @@ -3432,7 +3432,7 @@ \subsubsection{Generative Constructors}
\commentary{%
This means that formal parameters, including initializing formals,
must have distinct names, and that initializing formals
are in scope for the initializer list,
are in scope for the initializer list,
but they are not in scope for the body of the constructor.
When a formal parameter introduces a local variable into two scopes,
it is still one variable and hence one storage location.
Expand Down Expand Up @@ -5230,7 +5230,7 @@ \subsection{Mixin Classes}
% to be compile-time errors.

\commentary{%
It is an error, for example, if $M$ contains a member declaration $d$
It is an error, for example, if $M$ contains a member declaration $d$
which overrides a member signature $m$ in the interface of $S$,
but which is not a correct override of $m$
(\ref{correctMemberOverrides}).%
Expand Down Expand Up @@ -8254,7 +8254,7 @@ \subsection{Constants}
% be computed statically without running user code.

% A validly typed potentially constant expression can still fail when evaluated.
% If that happens in a const invociation, it's a compile-time error.
% If that happens in a const invocation, it's a compile-time error.

\LMHash{}%
It is a compile-time error if an expression is required to be
Expand Down Expand Up @@ -13772,7 +13772,7 @@ \subsubsection{Sending Messages}
Messages are sent by invoking specific methods in the Dart libraries; there is no specific syntax for sending a message.

\commentary{%
In other words, the methods supporting sending messages
In other words, the methods supporting sending messages
embody primitives of Dart that are not accessible to ordinary code,
much like the methods that spawn isolates.%
}
Expand Down Expand Up @@ -16880,13 +16880,13 @@ \subsection{If}

\rationale{%
Under reasonable scope rules such code is problematic.
If we assume that \code{v} is declared
Copy link
Member Author

Choose a reason for hiding this comment

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

Seems my "remove trailing spaces on save" has caught some dangling spaces.

Copy link
Member

Choose a reason for hiding this comment

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

This PR might then need to be rebased: The current version of dartLangSpec.tex (34c4e1a) does not contain any trailing spaces.

Copy link
Member Author

Choose a reason for hiding this comment

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

Trailing spaces are bad, m'kay?

Copy link
Member

Choose a reason for hiding this comment

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

Certainly!

I'm saying that there are no trailing spaces in dartLangSpec.tex today. In general, there shouldn't be many commits where there are any trailing spaces, because I usually remember to remove them, but I can see that this PR starts from a commit where there are quite a few trailing spaces.

But this means that removing trailing spaces in this PR will not remove any trailing spaces from the result of landing this PR (they're gone already), it will just make the merging operation a bit more complex.

I was worried that this kind of "fix something that has been fixed" change could in some situations give rise to a reversal: A line here and there could suddenly be edited back to an earlier version, because it has been changed in this PR, and it contains the old text in this PR (minus that trailing space). So git thinks that the old text is what we really want, and replaces the current text by the old text from this PR.

That's the reason why I suggested doing a rebase on this PR.

in the scope of the method \code{main()},
then when \code{somePredicate} is false,
If we assume that \code{v} is declared
in the scope of the method \code{main()},
then when \code{somePredicate} is false,
\code{v} will be uninitialized when accessed.
The cleanest approach would be to require a block following the test,
The cleanest approach would be to require a block following the test,
rather than an arbitrary statement.
However, this goes against long standing custom,
However, this goes against long standing custom,
undermining Dart's goal of familiarity.
Instead, we choose to insert a block, introducing a scope,
around the statement following the predicate
Expand Down Expand Up @@ -17141,7 +17141,7 @@ \subsubsection{Asynchronous For-in}
It is a compile-time error if a traditional for loop (\ref{forLoop}) is prefixed by the \AWAIT{} keyword.

\rationale{%
An asynchronous loop would make no sense within a synchronous function,
An asynchronous loop would make no sense within a synchronous function,
for the same reasons that an await expression makes no sense
in a synchronous function.%
}
Expand Down Expand Up @@ -18083,7 +18083,8 @@ \subsection{Yield-Each}
if the class of $o$ is not a subtype of \code{Iterable<$T_f$>}.
Otherwise
\item
The method \code{iterator} is invoked upon $o$ returning an object $i$.
The getter \code{iterator} is invoked upon $o$ returning an object $i$.
Otherwise
Copy link
Member

Choose a reason for hiding this comment

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

Should the word Otherwise actually be added here?

Copy link
Member

Choose a reason for hiding this comment

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

Also, the phrase is invoked upon is quite unusual in this spec, and it seems likely that I'm not the only reader who would need to look at it twice in order to understand what it means.

Wouldn't it be more like other parts of the specification if we use Evaluate \code{$o$.iterator} to an object $i$?

(We do say it like Evaluate \code{$v$.iterator}, where $v$ is a fresh variable bound to $o$. in many locations, but we do also have the slight abuse of notation where a symbol is at first denoting an object, and then considered to be a variable. Search for, e.g., 'evaluation of $ee$ is equivalent to the method invocation'.)

Copy link
Member Author

Choose a reason for hiding this comment

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

I should follow the norm here.
I was probably trying to avoid introducing new syntax (which I think is a bad choice in general, semantics should be explained at the semantic level without dipping back into syntax). But that's a much larger rewrite to avoid that.

\item
\label{moveNext} The \code{moveNext} method of $i$ is invoked on it
with no arguments.
Copy link
Member

Choose a reason for hiding this comment

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

And Evaluate \code{$u$.moveNext()}, where $u$ is a fresh variable bound to $i$., or Evaluate \code{$i$.moveNext()}.

Expand Down Expand Up @@ -18117,35 +18118,76 @@ \subsection{Yield-Each}
It is a dynamic type error if the class of $o$
is not a subtype of \code{Stream<$T_f$>}.
Otherwise
\item
If the stream associated with $m$ has been cancelled,
then execution of $s$ completes by returning without a value.
\commentary{In this case, the \code{\YIELD*} operation does
not begin to listen to the stream $o$.}
Otherwise
\item
The $o$ stream is listened to by invoking \code{$v_o$.listen}
Copy link
Member

Choose a reason for hiding this comment

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

Isn't The stream $o$ is more readable?

Copy link
Member Author

Choose a reason for hiding this comment

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

It is.

with system provided arguments,
where $v_o$ is a fresh variable referencing the stream $o$.
Copy link
Member

Choose a reason for hiding this comment

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

Again, fresh variable bound to $o$ would be the completely unsurprising phrase (we use that about 80 times, and variable referencing is only used 3 times).

Copy link
Member Author

Choose a reason for hiding this comment

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

ACK. Much better, yes.

Let $u$ be the stream subscription returned by the call to
\code{$p$.listen} and let $v$ be a fresh variable bound to $u$.
\item
If the stream associated with $m$ is paused, then $u$ is immediately
paused as if by invoking \code{$v$.pause} with no arguments.
Copy link
Member

Choose a reason for hiding this comment

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

What if it throws?

Copy link
Member Author

Choose a reason for hiding this comment

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

The default semantic fallback is that if some sub-part of the semantics of a construct throws, so does the construct itself unless otherwise stated. In this case, nothing otherwise is stated, so if $v$.pause throws, so does the await for body evaluation. (Which then does say what happens in that case - it cancels the subscription and rethrows).

Now, should it work like that? Probably yes.
If pause throws ... the stream probably isn't paused. Something is deeply wrong with that stream, so it's better to exit that loop immediately, and stop handling events from the stream entirely. (We should ignore any events after calling cancel).

It's possible to be obnoxious about the exiting. Say:

label: try {
  yield whatnot;
} finally {
  break label;
}

This will swallow any control flow trying to leave the try block and continue unabated.
We can't entirely control what happens after that, if the stream subscription acts maliciously.
(And that's why C# disallowed control flow in finally blocks!)

\item{}
If the stream associated with $m$ has been cancelled, then
$u$ is cancelled by executing \code{await $v$.cancel();}.
Copy link
Member

Choose a reason for hiding this comment

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

Isn't it more straightforward to say evaluating \code{await $v$.cancel()}. It doesn't bring much value to have that (visually clunky) semicolon. If we wish to make the point that if it evaluates to an object then that object is ignored then we can say that explicitly, but it seems sufficient to actually ignore it by not mentioning it. ;-)

Copy link
Member Author

Choose a reason for hiding this comment

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

ACK. Evaluating an expression is cleaner.

If this execution does not throw, the execution of $s$
completes by returning without a value.
Copy link
Member

Choose a reason for hiding this comment

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

Sounds like we could have commentary saying that it is an unexpected anomaly if await $v$.cancel() throws, it would only occur if listen or pause has side-effects where the stream is cancelled, and this will not occur with a platform provided stream.

Copy link
Member Author

Choose a reason for hiding this comment

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

Actually, cancel is one of the functions which can throw. It's not great when it does, but it's allowed and should be handled gracefully (which means propagating the error).

% This can only happen if a call to "listen" or "pause" above has
% side effects which cancels the stream of $m$.
\item
The nearest enclosing asynchronous for loop (\ref{asynchronousFor-in}),
if any, is paused.
\item
The $o$ stream is listened to, creating a subscription $s$,
and for each event $x$, or error $e$ with stack trace $t$, of $s$:
Execution of $m$ is suspended.
While $m$ is suspended, the following reactions happen if $u$ delivers
an event or if the stream associated with $m$ is paused, resumed or cancelled.
\commentary{It is unspecified what happens if $u$ delivers events
before $m$ is suspended or after $m$ is resumed, or if $u$ delivers events
after a call to \code{$v$.cancel} or a call to \code{$v$.pause} which has
not been followed by a call to \code{$v$.resume}, or after having delivered
a done event.}
% Such events should be ignored.
\begin{itemize}
\item
If the stream $u$ associated with $m$ has been paused,
then execution of $m$ is suspended until $u$ is resumed or canceled.
If the stream associated with $m$ becomes paused,
then $u$ is paused by executing \code{$v$.pause();}.
Copy link
Member

Choose a reason for hiding this comment

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

Similarly to line 18138, this could be evaluating \code{$v$.pause()}.

Copy link
Member Author

Choose a reason for hiding this comment

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

ACK.

It is unspecified what happens if this execution throws.
Copy link
Member

Choose a reason for hiding this comment

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

Wouldn't it be a friendly gesture to the practical developer to mention in commentary that a Stream whose pause throws is an unexpected anomaly, and a platform provided Stream will never do so?

Copy link
Member Author

Choose a reason for hiding this comment

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

Will do.

% The error can be passed to \code{Zone.current.handleUncaughtError}.
\item
If the stream $u$ associated with $m$ has been canceled,
then $s$ is canceled by evaluating \code{\AWAIT{} v.cancel()}
where $v$ is a fresh variable referencing the stream subscription $s$.
Then, if the cancel completed normally,
the stream execution of $s$ returns without an object
(\ref{statementCompletion}).
If the stream associated with $m$ is resumed after being paused,
then $u$ is resumed as by executing \code{$v$.resume();}.
Copy link
Member

Choose a reason for hiding this comment

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

Could again be evaluating \code{$v$.resume()}.

Copy link
Member Author

Choose a reason for hiding this comment

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

ACK

It is unspecified what happens if this execution throws.
Copy link
Member

Choose a reason for hiding this comment

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

Again, commentary could mention that this is an anomaly. Isn't that true, too?

Copy link
Member Author

Choose a reason for hiding this comment

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

Absolutely. If resume throws, it's completely unclear what state the stream subscription is in (did you resume or not?). The best we can do is to bail out as soon as possible and scream bloody murder to all available error channels. This code is just at a position where there is no good error channel.

% The error can be passed to \code{Zone.current.handleUncaughtError}.
\item
If the stream associated with $m$ is cancelled,
then $u$ is also cancelled as by executing \code{await $v$.cancel();}.
Copy link
Member

Choose a reason for hiding this comment

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

And what if await $v$.cancel() throws? ;-)

Copy link
Member Author

Choose a reason for hiding this comment

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

Preferably, the code calling stream.cancel will get the future. That assumes that the cancel comes from cancelling a StreamSubscription, which ... it does, but we haven't been explicit about that.

Maybe I should go back to the drawing board and be explicit about everything.

Calling listen on the stream returned by the async* function returns a stream subscription.
The stream subscription doesn't "become paused", rather someone calls pause on it. That means we have a receiver for any synchronous errors happening during that call. Same for resume and cancel.

Copy link
Member

Choose a reason for hiding this comment

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

be explicit about everything.

How about landing this one in approximately the current form, and then considering an additional revision in a separate PR?


At some future time, execution of $m$ resumes. If the execution above
completed by throwing an error \metavar{er} and stack trace \metavar{st},
then execution of $s$ completes by throwing \metavar{er}
and stack trace \metavar{st}.
Otherwise, execution of $s$ completes by returning without a value.
\item
Otherwise, $x$, or $e$ with $t$, are added to
the stream associated with $m$ in the order they appear in $o$.
\commentary{%
Note that a dynamic error occurs if $x$ is added
and the dynamic type of $x$ is not a subtype of
the element type of said stream.%
}
The function $m$ may suspend.
If $u$ emits a data event with value $x$,
then if the runtime type of $x$ is not a subtype of $T_v$,
then the stream associated with $m$ emits a dynamic type error.
Otherwise the stream associated with $m$ immediately emits
a data event with value $x$.
\item
If $u$ emits an error event with error \metavar{er}
and stack trace \metavar{st},
then the stream associated with $m$ immediately emits an error event
with error \metavar{er} and stack trace \metavar{st}.
\item
If $u$ closes \commentary{(by emitting a done event)},
then execution of $m$ resumes and execution of $s$ completes normally.
\end{itemize}
\item
If the stream $o$ is done, execution of $s$ completes normally.
\end{itemize}


Expand Down