-
Notifications
You must be signed in to change notification settings - Fork 72
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
Use open
instead of final
in the text format
#413
Conversation
\Tsubtype &\equiv& | ||
\text{(}~~\text{rec}~~\Tsubtype~~\text{)} \\ | ||
\Tdeftype &\equiv& | ||
\text{(}~~\text{rec}~~\Tdeftype~~\text{)} \\ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is not related to my work, but I believe it to be a bug in the spec that is easy to fix.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No, I think this was correct before.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't see how it could be correct before. According to the grammar above, recursion groups contain deftypes ((rec vec(deftype))
), and deftypes contain subtypes ((type subtype)
). The production subtype = (rec subtype)
therefore doesn't make sense, as it implies that it expands to something like (rec (sub (struct)))
, which violates the main grammar.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@bvisness's fix here looks right to me. We don't want to allow (sub (struct))
, a subtype, to appear on its own, but we do want to allow (type (sub (struct)))
, a deftype, to appear on its own.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah, you are right, I was confused by the impedance mismatch with the abstract syntax, where deftype is something else. We should probably not be naming this one in the text format deftype, but rather something else (typedef?).
\begin{array}{llclll} | ||
\production{reference type} & | ||
\begin{array}{lcl} | ||
\production{reference type} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is also unrelated to my work, but this table was jank, and now it is not.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah, the production name needs its own column, in case its used. The correct fix here is to add &
's below, i.e., change each \\
to \\&
(perhaps except the last). You can simplify the column scheme to {llcl}
.
\production{sub type} & | ||
\Tcomptype &\equiv& | ||
\text{(}~~\text{sub}~~\text{final}~~\epsilon~~\Tcomptype~~\text{)} \\ | ||
\text{(}~~\text{sub}~~\Tcomptype~~\text{)} \\ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's not clear to me why the epsilon
was in here, but I can add it back if it was actually necessary.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It probably represented the empty vector of supertypes. I think it would make sense to put it and the "and arguments" language back.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What @tlively said, this was intentional.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm afraid this PR is rather incomplete.
The text format is intended to be a direct reflection of the abstract syntax. So, if we toggle the text format, then it's necessary that we apply the same change to the abstract syntax. Similarly the interpreter AST.
A further consequence then is that we'll also need to adjust the spec terminology. It's confusing if it talks about final types everywhere when the syntax inversely only speaks of open types. We'd probably want to replace all occurrence of "final type" with "non-open" type.
Unfortunately, I think that would have a rather adverse affect on overall spec clarity. Less clear terminology for the sole purpose of a shorthand in the text format is perhaps not a good trade-off.
The one way out I see is to fall back to the earlier suggestion of having both final
and open
keyword and neither is optional. That might also lead to less surprise in the text format than this PR – I suspect very few readers would expect subtype definitions to implicitly mean final.
\begin{array}{llclll} | ||
\production{reference type} & | ||
\begin{array}{lcl} | ||
\production{reference type} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah, the production name needs its own column, in case its used. The correct fix here is to add &
's below, i.e., change each \\
to \\&
(perhaps except the last). You can simplify the column scheme to {llcl}
.
&\Rightarrow& \TSUB~\TFINAL^?~x^\ast~\X{ct} \\ | ||
\end{array} | ||
|
||
.. note:: | ||
A subtype is :ref:`final <syntax-subtype>` if the :math:`\text{open}` keyword is not present, and vice versa. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
See above, this comment shouldn't be needed if the text format is consistent with the AST.
|
||
Abbreviations | ||
............. | ||
|
||
Singular recursive types can omit the |Trec| keyword: | ||
Singular recursive types can omit the :math:`\text{rec}` keyword: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why this change?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Because it refers to a keyword of the text format, not a structural element of a wasm module. The primary difference is in how they render, but suppose the structural element were named "recgrp" instead of "rec" - if that were the case, the sentence would make no sense, as recgrp
is not a text format keyword.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It may be useful to note that macros.def does not define Trec
, so I think it is parsing as |TREC|
, which does link to the abstract syntax rather than the textual keyword.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah, good points.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done as a standalone fix in #426.
\Tsubtype &\equiv& | ||
\text{(}~~\text{rec}~~\Tsubtype~~\text{)} \\ | ||
\Tdeftype &\equiv& | ||
\text{(}~~\text{rec}~~\Tdeftype~~\text{)} \\ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No, I think this was correct before.
|
||
.. math:: | ||
\begin{array}{llclll} | ||
\begin{array}{lcl} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this needs to be at least llcl
, otherwise Latex will barf.
\production{sub type} & | ||
\Tcomptype &\equiv& | ||
\text{(}~~\text{sub}~~\text{final}~~\epsilon~~\Tcomptype~~\text{)} \\ | ||
\text{(}~~\text{sub}~~\Tcomptype~~\text{)} \\ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What @tlively said, this was intentional.
I would support having both @bvisness, will you have time to work on this more today and Monday? If not, I can help out. |
@rossberg, would it suffice to add |
I think we should keep them consistent. It actually simplifies some formulations as well when we have a named phrase like |
@rossberg, would you be able to work on completing this change? If not, I will take a stab at it in the morning pacific time. |
@tlively, I can try, but I can't promise anything — I'm on an a flight Odyssee right now after I was dumped from my flight back to Europe yesterday. Hence my bigger concern is that I even make it back in time for the meeting tomorrow. ;) |
Apologies for my absence. I can resume work on this tomorrow if it's not already done. |
Instead of using final? in the syntax, use ext ::= open | final. Implements the design discussed in #413. Update the interpreter, the abstract syntax, the binary and text formats, and MVP.md.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
\Tsubtype &\equiv& | ||
\text{(}~~\text{rec}~~\Tsubtype~~\text{)} \\ | ||
\Tdeftype &\equiv& | ||
\text{(}~~\text{rec}~~\Tdeftype~~\text{)} \\ |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't see how it could be correct before. According to the grammar above, recursion groups contain deftypes ((rec vec(deftype))
), and deftypes contain subtypes ((type subtype)
). The production subtype = (rec subtype)
therefore doesn't make sense, as it implies that it expands to something like (rec (sub (struct)))
, which violates the main grammar.
|
||
Abbreviations | ||
............. | ||
|
||
Singular recursive types can omit the |Trec| keyword: | ||
Singular recursive types can omit the :math:`\text{rec}` keyword: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Because it refers to a keyword of the text format, not a structural element of a wasm module. The primary difference is in how they render, but suppose the structural element were named "recgrp" instead of "rec" - if that were the case, the sentence would make no sense, as recgrp
is not a text format keyword.
Addresses discussion from #333. With this patch, the keyword
final
in subtypes has been replaced with the keywordopen
:This avoids a confusing flip-flopping behavior where a seemingly-unnecessary empty
sub
was commonly used to make types non-final. An emptysub
is now equivalent to nosub
, making the abbreviation more obvious.This patch is currently quite minimal, and only modifies enough of the spec and interpreter to support
open
in the text format. The wordfinal
is otherwise used throughout the spec and interpreter. If we would rather use the wordopen
everywhere, I'd be happy to update the rest of the spec and interpreter to match.