-
Couldn't load subscription status.
- Fork 55
Scenarios #76
Scenarios #76
Changes from 18 commits
f199ebc
63cde43
91b8283
144dc8b
550d543
c735e3c
898da14
13f556f
0916acd
b1f7373
1f7520b
642391a
aa72dca
08ff21d
c999f8c
f0ed505
44ca2df
99fac97
d3ff4d3
69c88ee
fe0f6b0
1a1f4d1
71ed409
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,23 @@ | ||
| # Working Notes | ||
|
|
||
| The purpose of this directory is to hold notes about the current design of the | ||
| Interface Types proposal. These notes are intended as analogous to the | ||
| [WebAssembly design repo](https://github.com/WebAssembly/design/), as a | ||
| less-formal way of designing components of the proposal. Documents should | ||
| reflect our current consensus, but the ideas don't need to be fully fleshed out. | ||
| These documents should inform the final spec. | ||
|
|
||
| Sample topics: | ||
| * How we should handle Wasm exceptions | ||
| * How engines might need to optimize combinations of adapters | ||
| * What is necessary for MVP, and what can be deferred | ||
|
|
||
| In general, we should try to match the conventions that are already established, | ||
| but when inventing some new topic, just making up syntax/instructions is the | ||
| right way to go. | ||
|
|
||
| ### Q: Why not add these to the Explainer? | ||
| These aren't necessarily things that the explainer needs to spell out. If the | ||
| purpose of the explainer is to convey the information to a reader from scratch, | ||
| the nuances of a given design detail is likely to be distracting detail. It is | ||
| likely that some subsets will wind up in the explainer over time. |
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,73 @@ | ||
|
|
||
|
|
||
| ### Records | ||
|
|
||
| Records are collections of named and typed fields. Records can be defined in as | ||
| Interface Types; for example this definition encodes a familiar notion of a | ||
| credit card: | ||
|
|
||
| ```wat | ||
| (@interface datatype @cc | ||
| (record "cc" | ||
|
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. We should discuss whether it's useful to add string names to type definitions. I think it's necessary to name fields (since it allows specifying field type compatibility in an order-independent manner, which is useful), but I don't think it buys us anything to name structs, given that we'll already need to check their contents for type-compatibility anyway. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. If you have alternate cases in an algebraic type then you need to distinguish them. This is going to be an issue especially for C ... to be handled later. addEventListener('type', function, capture?); There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Interesting point. With the current interface types proposal, one never does an "overload resolution" wherein a (name, signature) pair is looked up in some scope, resolving to a function. Rather, the order is inverted: a function is supplied to wasm instantiation and then we ask if that function's type is compatible with the import's declared type. For Web IDL, all declared overloads end up producing a single function that wasm can import and thus the type-compatibility check is against this list of valid signatures. For future APIs (like WASI), I think we'd want to not allow overloading and instead use variant types in the signature (which, of course, have string field names). |
||
| (ccNo u64) | ||
fgmccabe marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| (name string) | ||
| (expires (record | ||
| (mon u8) | ||
| (year u16) | ||
| ) | ||
| ) | ||
| (ccv u16) | ||
| ) | ||
| ) | ||
| ``` | ||
|
|
||
| Lifting and lowering a record involves lifting/lowering the individual fields of | ||
| the record and then 'packing' or 'unpacking' the record as an ordered | ||
| sub-sequence of elements on the stack. | ||
|
|
||
| For example, the sequence: | ||
|
|
||
| ```wat | ||
| ... | ||
| local.get $ccNo | ||
| i64-to-u64 | ||
| local.get $name | ||
| local.get $name.len | ||
| memory-to-string | ||
| i8.local.get $mon | ||
| i8_to_u8 | ||
|
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. IIUC, local.get $mon
i32-to-u8It'd be nice to put this instruction sequence into a proper adapter function (with param/result) so that the types of these |
||
| i16.local.get $year | ||
| i16_to_u16 | ||
| pack @(record (mon u8) (year u16)) | ||
|
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Could There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Yes. In this case though, the record is a structural type; I guess that we could require structural types to be defined too ... |
||
| local.get $ccv | ||
| pack @cc.cc | ||
| ... | ||
| ``` | ||
| creates a credit card information record from various local variables. | ||
|
|
||
| Lowering a record is complimentary, involving an `unpack` operator; together | ||
| with individual lowering operators for the fields: | ||
|
|
||
| ```wat | ||
| ... | ||
| unpack @cc.cc $ccNo $name $expires $ccv | ||
|
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. What if There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. That is essentially what I was thinking, with some syntactic sugar to avoid the multiple lets. |
||
| local.get $ccNo | ||
| u64-to-i64 | ||
| local.get $name | ||
| string-to-memory "malloc" | ||
| local.get $expires | ||
| unpack @(record (mon u8) (year u16)) $mon $year | ||
| local.get $mon | ||
| u8-to-i32 | ||
| local.get $year | ||
| u16-to-i32 | ||
| end | ||
| local.get $ccv | ||
| u16-to-i32 | ||
| end | ||
| ``` | ||
|
|
||
| The result of this unpacking is to leave the fields of the record on the | ||
| stack. If the intention were to store the record in memory then this code could | ||
| be augmented with memory store instructions. | ||
|
|
||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,251 @@ | ||
| # Pay by Credit Card | ||
|
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. It'd be nice to update this example to be in sync with record.md above. E.g., I think There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. agreed |
||
|
|
||
| In order to process a payment with a credit card, various items of information | ||
| are required: credit card details, amount, merchant bank, and so on. This | ||
| example illustrates the use of nominal types and record types in adapter code. | ||
|
|
||
| >Note that we have substantially simplified the scenario in order to construct | ||
| >an illustrative example. | ||
|
|
||
| The signature of `payWithCard` as an interface type is: | ||
|
|
||
| ``` | ||
| cc ::= cc{ | ||
| ccNo : u64; | ||
| name : string; | ||
| expires : { | ||
| mon : u8; | ||
| year : u16 | ||
| } | ||
| ccv : u16 | ||
| } | ||
| payWithCard:(card:cc, amount:s64, session:resource<connection>) => boolean | ||
| ``` | ||
|
|
||
| ## Export | ||
|
|
||
| In order to handle the incoming information, a record value must be passed -- | ||
| including a `string` component -- and a `session` that denotes the bank | ||
| connection must be paired with an existing connection resource. The connection | ||
| information is realized as an `eqref` (an `anyref` that supports equality). | ||
|
|
||
| In this scenario, we are assuming that the credit card information is passed by | ||
| value (each field in a separate argument) to the internal implementation of the | ||
| export, and passed by reference to the import. | ||
|
|
||
| ``` | ||
| (@interface datatype @cc | ||
| (record "cc" | ||
| (ccNo u64) | ||
| (name string) | ||
| (expires (record | ||
| (mon u8) | ||
| (year u16) | ||
| ) | ||
| ) | ||
| (ccv u16) | ||
| ) | ||
| ) | ||
|
|
||
| (@interface typealias @connection eqref) | ||
|
|
||
| (memory (export $memx) 1) | ||
|
|
||
| (func $payWithCard_ (export ("" "payWithCard_")) | ||
| (param i64 i32 i32 i32 i32 i32 eqref) (result i32) | ||
|
|
||
| (@interface func (export "payWithCard") | ||
| (param $card @cc) | ||
| (param $session (resource @connection)) | ||
| (result boolean) | ||
|
|
||
| local.get $card | ||
| field.get #cc.ccNo ;; access ccNo | ||
| u64-to-i64 | ||
|
|
||
| local.get $card | ||
| field.get #cc.name | ||
| string-to-memory $mem1 "malloc" | ||
|
|
||
| local.get $card | ||
| field.get #cc.expires.mon | ||
|
|
||
| local.get $card | ||
| field.get #cc.expires.year | ||
|
|
||
| local.get $card | ||
| field.get #cc.ccv | ||
|
|
||
| local.get $session | ||
| resource-to-eqref @connection | ||
| call $payWithCard_ | ||
| i32-to-enum boolean | ||
| ) | ||
|
|
||
| (func (export "malloc") | ||
| (param $sze i32) (result i32) | ||
| ... | ||
| ) | ||
| ``` | ||
|
|
||
| ## Import | ||
|
|
||
| In this example, we assume that the credit details are passed to the import by | ||
| reference; i.e., the actual argument representing the credit card information is | ||
| a pointer to a block of memory. | ||
|
|
||
| ``` | ||
| (func $payWithCard_ (import ("" "payWithCard_")) | ||
| (param i32 eqref) (result i32) | ||
|
|
||
| (@interface func $payWithCard (import "" "payWithCard") | ||
| (param @cc (resource @connection)) | ||
| (result boolean)) | ||
|
|
||
| (@interface implement (import "" "payWithCard_") | ||
| (param $cc i32) | ||
| (param $conn eqref) | ||
| (result i32) | ||
|
|
||
| local.get $cc | ||
| i64.load {offset #cc.ccNo} | ||
| i64-to-u64 | ||
|
|
||
| local.get $cc | ||
| i32.load {offset #cc.name.ptr} | ||
|
|
||
| local.get $cc | ||
| i32.load {offset #cc.name.len} | ||
| memory-to-string "memi" | ||
|
|
||
| local.get $cc | ||
| i16.load_u {offset #cc.expires.mon} | ||
|
|
||
| local.get $cc | ||
| i16.load_u {offset #cc.expires.year} | ||
|
|
||
| create (record (mon u16) (year u16)) | ||
|
|
||
| local.get $cc | ||
| i16.load_u {offset #cc.ccv} | ||
|
|
||
| create @cc | ||
|
|
||
| local.get $conn | ||
| eqref-to-resource @connection | ||
|
|
||
| call $payWithCard | ||
| enum-to-i32 boolean | ||
| ) | ||
| ``` | ||
|
|
||
| ## Adapter | ||
|
|
||
| Combining the import, exports and distributing the arguments, renaming `cc` for | ||
| clarity, we initially get: | ||
|
|
||
| ``` | ||
| (@adapter implement (import "" "payWithCard_") | ||
| (param $cc i32) | ||
| (param $conn eqref) | ||
| (result i32) | ||
|
|
||
| local.get $cc | ||
| i64.load {offset #cc.ccNo} | ||
| i64-to-u64 | ||
|
|
||
| local.get $cc | ||
| i32.load {offset #cc.name.ptr} | ||
|
|
||
| local.get $cc | ||
| i32.load {offset #cc.name.len} | ||
| memory-to-string "memi" | ||
|
|
||
| local.get $cc | ||
| i16.load_u {offset #cc.expires.mon} | ||
|
|
||
| local.get $cc | ||
| i16.load_u {offset #cc.expires.year} | ||
|
|
||
| create (record (mon u16) (year u16)) | ||
|
|
||
| local.get $cc | ||
| i16.load_u {offset #cc.ccv} | ||
|
|
||
| create @cc | ||
|
|
||
| local.get $conn | ||
| eqref-to-resource @connection | ||
|
|
||
| let $session (resource @connection) | ||
| let $card @cc | ||
|
|
||
| local.get $card | ||
| field.get #cc.ccNo ;; access ccNo | ||
| u64-to-i64 | ||
|
|
||
| local.get $card | ||
| field.get #cc.name | ||
| string-to-memory $mem1 "malloc" | ||
|
|
||
| local.get $card | ||
| field.get #cc.expires.mon | ||
| u16-to-i32 | ||
|
|
||
| local.get $card | ||
| field.get #cc.expires.year | ||
| u16-to-i32 | ||
|
|
||
| local.get $card | ||
| field.get #cc.ccv | ||
| u16-to-i32 | ||
|
|
||
| local.get $session | ||
|
|
||
| resource-to-eqref @connection | ||
| call $payWithCard_ | ||
| i32-to-enum boolean | ||
| end | ||
| end | ||
| enum-to-i32 boolean | ||
| ) | ||
| ``` | ||
|
|
||
| With some assumptions (such as no aliasing, no writing to locals, no | ||
| re-entrancy), we can propagate and inline the definitions of intermediates. This | ||
| amounts to 'regular' inlining where we recurse into records and treat the fields | ||
| of the record in an analogous fashion to arguments to the call. | ||
|
|
||
| ``` | ||
| (@adapter implement (import "" "payWithCard_") | ||
| (param $cc i32) | ||
| (param $conn eqref) | ||
| (result i32) | ||
|
|
||
| local.get $cc | ||
| i64.load {offset #cc.ccNo} | ||
|
|
||
| local.get $cc | ||
| i32.load {offset #cc.name.ptr} | ||
|
|
||
| local.get $cc | ||
| i32.load {offset #cc.name.len} | ||
| string.copy Mi:"mem2" Mx:"memx" "malloc" | ||
|
|
||
| local.get $cc | ||
| i16.load_u {offset #cc.expires.mon} | ||
|
|
||
| local.get $cc | ||
| i16.load_u {offset #cc.expires.year} | ||
|
|
||
| local.get $cc | ||
| i16.load_u {offset #cc.ccv} | ||
|
|
||
| local.get $conn | ||
| call $payWithCard_ | ||
| ) | ||
| ``` | ||
|
|
||
| There would be different sequences for the adapter if the underlying ABI were different -- | ||
| for example, if structured data were passed as a pointer to a local copy for | ||
| example. | ||
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.
For symmetry with how we have
(func $f)/(@interface func $f), how about(type $T)/(@interface type $T)(instead ofdatatype @T)?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.
Am open to adjustment. However, when defining types there are two basic scenarios: defining a new algebraic type and type aliasing. These need to be distinguished. (Examples of 'type aliasing' include type imports)
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.
@fgmccabe, the only reason to distinguish them would be if you wanted nominal typing for algebraic types. But there is little reason to want that in Wasm interfaces. In fact, there is good reason not to want that because it makes everything more complicated and aversely affects modularity.
Uh oh!
There was an error while loading. Please reload this page.
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.
On second thoughts, I think we need to keep the @ character.
If you have a param specification for an interface function; you need to disambiguate:
(param $cc (resource $connection))
could mean a param block with two types that happen to be by reference or a single parameter called cc.
On the other hand
(param @cc (resource @connection))
is unambiguous (a param block of two types)
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, interesting question. If we look at the GC proposal, which similarly introduces type definitions and uses, we can see that, in most cases, a type use occurs as part of a reference type, so you can unambiguously have
(ref $T)for some typedef$T. However, there is one exception: when the field of astructor element of anarrayis stored inline, not by reference; for this the explainer uses(type $T)which is presumably chosen to be symmetric with the MVP text format, where you can write:as the expanded form of the syntactic sugar:
Thus, I think your final example would be most-symmetrically written: