-
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
Incorporate generative RTT #86
Conversation
Can you briefly explain what "generative" means in this context and what alternatives it differentiates from? |
- multiple invocations of this instruction with the same operand yield the same observable RTTs | ||
- each invocation of this instruction yields a distinct RTT |
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.
@tlively: Here is the most important change (along with the matching change in rtt.get
to rtt.new
). An "applicative" system returns the same value when given the same inputs (previous semantics), whereas a "generative" system returns a new value distinct from all previous values (new semantics).
|
||
* `rtt.sub <typeuse>` returns the RTT of the specified type as a sub-RTT of a given parent RTT operand | ||
- `rtt.sub t : [(rtt t')] -> [(rtt t)]` | ||
- iff `t <: t'` | ||
- multiple invocations of this instruction with the same operand yield the same observable RTTs | ||
- each invocation of this instruction yields a distinct RTT | ||
- this is a *constant instruction* |
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.
Also, this assertion was already present but wasn't true. For an applicative semantics, one must canonicalize the structure of the type (which is not constant time), hash it (again not constant time), and then use a host-global concurrent hash map to get the canonical rtt
for the type (requiring another non-constant-time equality comparison). When the type is known it compile time, which is currently the case for this proposal, then all of that can be done at compile time and the instruction replaced with the precomputed rtt
, which is where the assertion that this instruction is constant time comes from. However, the proposal also recommends adding parametric polymorphism later on, which will introduce type parameters that the type in rtt.get
can refer to, in which case all of this will have to be done at run time and the instruction will no longer be constant time. With the generative semantics, this is constant time even in the presence of type variables.
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.
"Constant instruction" is spec terminology that has nothing to do with constant time.
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, thanks for the correction and the link!
The current docs do not incorporate generative types yet, neither statically nor dynamically. If we add nominal types then of course we'd also want to add generative RTTs. However, that does not eliminate the need for non-generative RTTs, for the same reason as with static types. So such a change should add |
Could you give some examples? In your talk at the in-person meeting, you advocating for removing anything from the MVP that could reasonably be expressed without it. I removed |
* Fix expected trap messages. The spec interpreter says "element segment dropped", rather than "elements segment dropped". * Fix "zero len, but dst offset out of bounds" test. Fix this test to test what it's comment says it's testing. * Add more tests for zero-length operations. * Update the Overview text to reflect the zero-length at-the-end semantics.
I'll close this PR since we won't be including RTTs of any kind in the MVP. |
Thanks to a number of discussions, I now have enough understanding of the expected conventions for this proposal to suggest a modest revision that should address a number of open questions.
First, the proposal already has in place an expectation to use run-time type information, RTT(I)s. One thing that was unclear is what precisely the semantics of RTTIs should be. For example, if$t1$ is a subtype of $t2, should an
anyref
with the RTT(rtt.get $t1)
be castable to a$t2
via(rtt.get $t2)
? According to the current semantics, the answer is no—the cast should only succeed if the two types are exactly the same. This is good for performance, but it did bring into question how modules should share values viaanyref
since it means they have to agree exactly on what run-time types to use.The expectation now, though, is that coordinated "share-nothing" module communication will be done via Interface Types. Furthermore, in #85, we agreed that for uncoordinated/heterogeneous communication (say via
anyref
), it is important for correctness that modules be able to distinguish their values (via generative tags, like with exceptions) from those of other values (even if they happen to have the same structure).Furthermore, in WebAssembly/proposal-type-imports#7, we came to the conclusion that, in order to prevent client modules from inspecting the internals of abstract exported types, we need to be able to guarantee that exported values can only be cast to a target (structural) type if the module also exports its own (generative)
rtt
for the target type.Altogether, this indicates that
rtt
s should be generative. On top of that, I was able to go through the overview and easily switch all the examples to generative RTTs, so the adjustment seems to be compatible with the known usage patterns. The adjustment required little change to the instructions, with the most significant being thatrtt.sub
semantics are now to always generate a newrtt
rather than to always reproduce the samertt
with the same inputs.My hope is that, by pinning answers to some of the major open questions, this gets us all on the same page as to what this proposal entails and how it should be expected to be used and implemented.