Skip to content
This repository was archived by the owner on Apr 25, 2025. It is now read-only.

3-pronged subtyping hierarchy #310

Merged
merged 9 commits into from
Aug 26, 2022
Merged

3-pronged subtyping hierarchy #310

Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
a19cb15
Missing type opcodes
rossberg Jul 14, 2022
30f6e96
Add note
rossberg Jul 14, 2022
91efeac
Tweaks
rossberg Jul 14, 2022
c2b19aa
Merge branch 'main' into 3pronged
rossberg Jul 14, 2022
c604c34
Merge branch 'main' into 3pronged
rossberg Jul 14, 2022
e0dbd0b
Adjust casts
rossberg Jul 14, 2022
9791652
Apply suggestions from code review
rossberg Aug 2, 2022
902830d
Type opcodes
rossberg Aug 26, 2022
51637ca
Merge branch 'main' into 3pronged
rossberg Aug 26, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
181 changes: 108 additions & 73 deletions proposals/gc/MVP.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,31 @@ Both proposals are prerequisites.

#### Heap Types

[Heap types](https://github.com/WebAssembly/function-references/blob/master/proposals/function-references/Overview.md#types) classify reference types and are extended:
[Heap types](https://github.com/WebAssembly/function-references/blob/master/proposals/function-references/Overview.md#types) classify reference types and are extended. There now are 3 disjoint hierarchies of heap types:

1. _Internal_ (values in Wasm representation)
2. _External_ (values in a host-specific representation)
3. _Functions_

Heap types `extern` and `func` already exist via [reference types proposal](https://github.com/WebAssembly/reference-types), and `(ref null? $t)` via [typed references](https://github.com/WebAssembly/function-references); `extern` and `func` are the common supertypes (a.k.a. top) of all external and function types, respectively.

The following additions are made to the hierarchies of heap types:

* `any` is a new heap type
- `heaptype ::= ... | any`
- the common supertype (a.k.a. top) of all internal types

* `none` is a new heap type
- `heaptype ::= ... | none`
- the common subtype (a.k.a. bottom) of all internal types

* `noextern` is a new heap type
- `heaptype ::= ... | noextern`
- the common subtype (a.k.a. bottom) of all external types

* `nofunc` is a new heap type
- `heaptype ::= ... | nofunc`
- the common subtype (a.k.a. bottom) of all function types

* `eq` is a new heap type
- `heaptype ::= ... | eq`
Expand All @@ -45,24 +69,26 @@ Both proposals are prerequisites.
- `heaptype ::= ... | i31`
- the type of unboxed scalars

* `none` is a new heap type
- `heaptype ::= ... | none`
- the common subtype of all referenceable types (a.k.a. the bottom heap type)
We distinguish these *abstract* heap types from *concrete* heap types `$t` that reference actual definitions in the type section.
Most abstract heap types are a supertype of a class of concrete heap types.
Moreover, they form a small [subtype hierarchy](#subtyping) among themselves.

* `extern` is renamed back to `any`
- the common supertype of all referenceable types
- the name `extern` is kept as an alias in the text format for backwards compatibility

* Note: heap types `func` and `extern` already exist via [reference types proposal](https://github.com/WebAssembly/reference-types), and `(ref null? $t)` via [typed references](https://github.com/WebAssembly/function-references)
#### Reference Types

We distinguish these *abstract* heap types from *concrete* heap types `(type $t)`.
Each abstract heap type is a supertype of a class of concrete heap types.
Moreover, they form a small [subtype hierarchy](#subtyping).
New abbreviations are introduced for reference types in binary and text format, corresponding to `funcref` and `externref`:

* `anyref` is a new reference type
- `anyref == (ref null any)`

#### Reference Types
* `nullref` is a new reference type
- `nullref == (ref null none)`

New abbreviations are introduced for reference types in binary and text format, corresponding to `funcref` and `externref`:
* `nullexternref` is a new reference type
- `nullexternref == (ref null noextern)`

* `nullfuncref` is a new reference type
- `nullfuncref == (ref null nofunc)`

* `eqref` is a new reference type
- `eqref == (ref null eq)`
Expand All @@ -76,13 +102,6 @@ New abbreviations are introduced for reference types in binary and text format,
* `i31ref` is a new reference type
- `i31ref == (ref null i31)`

* `nullref` is a new reference type
- `nullref == (ref null none)`

* `externref` is renamed to `anyref`
- `anyref == (ref null any)`
- the name `externref` is kept as an alias in the text format for backwards compatibility


#### Type Definitions

Expand Down Expand Up @@ -301,11 +320,30 @@ In the [existing rules](https://github.com/WebAssembly/function-references/propo

In addition to the [existing rules](https://github.com/WebAssembly/function-references/proposals/function-references/Overview.md#subtyping) for heap types, the following are added:

* every type is a subtype of `any`
* every internal type is a subtype of `any`
- `t <: any`
- if `t = any/eq/data/array/i31` or `t = $t` and `$t = <structtype>` or `$t = <arraytype>`

* every type is a supertype of `none`
* every internal type is a supertype of `none`
- `none <: t`
- if `t <: any`

* every external type is a subtype of `extern`
- `t <: extern`
- if `t = extern`
- note: there may be other subtypes of `extern` in the future

* every external type is a supertype of `noextern`
- `noextern <: t`
- if `t <: extern`

* every function type is a subtype of `func`
- `t <: func`
- if `t = func` or `t = $t` and `$t = <functype>`

* every function type is a supertype of `nofunc`
- `nofunc <: t`
- if `t <: func`

* `dataref` is a subtype of `eqref`
- `data <: eq`
Expand All @@ -317,32 +355,34 @@ In addition to the [existing rules](https://github.com/WebAssembly/function-refe
* `i31ref` is a subtype of `eqref`
- `i31 <: eq`

* Any concrete type is a subtype of either `data` or `func`
* Any concrete internal type is a subtype of `data`
- `$t <: data`
- if `$t = <structtype>` or `$t = <arraytype>`

* Any concrete function type is a subtype of `func`
- `$t <: func`
- if `$t = <functype>`

* Any concrete array type is a subtype of `array`
- `(type $t) <: array`
- `$t <: array`
- if `$t = <arraytype>`

Note: This creates a hierarchy of *abstract* Wasm heap types that looks as follows.
```
any
/ \
eq func
any extern func
|
eq
/ \
i31 data
\
array
```
All *concrete* heap types (of the form `(type $t)`) are situated below either `data` or `func`.
Not shown in the graph is `none`, which is below every other "leaf" type.
All *concrete* types (of the form `$t`) are situated below either `data` or `func`.
Not shown in the graph are `none`, `noextern`, and `nofunc`, which are below the other "leaf" types.

In addition, a host environment may introduce additional inhabitants of type `any`
that are are in neither of the above three leaf type categories.
The interpretation of such values is defined by the host environment.
A host environment may introduce additional inhabitants of type `any`
that are are in neither of the above leaf type categories.
The interpretation of such values is defined by the host environment, they are opaque within Wasm code.

Note: In the future, this hierarchy could be refined, e.g., to distinguish compound data types that are not subtypes of `eq`.

Expand Down Expand Up @@ -526,8 +566,6 @@ This can compile to machine code that (1) reads the RTT from `$x`, (2) checks th

#### Unboxed Scalars

Tentatively, support a type of guaranteed unboxed scalars.

* `i31.new` creates an `i31ref` from a 32 bit value, truncating high bit
- `i31.new : [i32] -> [(ref i31)]`
- this is a *constant instruction*
Expand All @@ -537,10 +575,22 @@ Tentatively, support a type of guaranteed unboxed scalars.
- traps if the operand is null


#### Classification
#### External conversion

* `extern.internalize` converts an external value into the internal representation
Copy link
Contributor

Choose a reason for hiding this comment

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

In the discussions, in was mentioned that it would be useful for performance to include direct transformations to more specific abstract types. This might be best as a post-MVP feature though.

- `extern.internalize : [(ref null1? extern)] -> [(ref null2? any)]`
- iff `null1? = null2?`
- this is a *constant instruction*
- note: this succeeds for all values, composing this with `extern.externalize` (in either order) yields the original value

* `extern.externalize` converts an internal value into the external representation
- `extern.externalize : [(ref null1? any)] -> [(ref null2? extern)]`
- iff `null1? = null2?`
- this is a *constant instruction*
- note: this succeeds for all values; moreover, composing this with `extern.internalize` (in either order) yields the original value

* `ref.is_func` checks whether a reference is a function
- `ref.is_func : [anyref] -> [i32]`

#### Classification

* `ref.is_data` checks whether a reference is compound data
- `ref.is_data : [anyref] -> [i32]`
Expand All @@ -551,20 +601,6 @@ Tentatively, support a type of guaranteed unboxed scalars.
* `ref.is_i31` checks whether a reference is an i31
- `ref.is_i31 : [anyref] -> [i32]`

* `br_on_func <labelidx>` branches if a reference is a function
- `br_on_func $l : [t0* t] -> [t0* t]`
- iff `$l : [t0* t']`
- and `t <: anyref`
- and `(ref func) <: t'`
- passes operand along with branch as a function, plus possible extra args

* `br_on_non_func <labelidx>` branches if a reference is not a function
- `br_on_non_func $l : [t0* t] -> [t0* (ref func)]`
- iff `$l : [t0* t']`
- and `t <: anyref`
- and `t <: t'`
- passes operand along with branch, plus possible extra args

* `br_on_data <labelidx>` branches if a reference is compound data
- `br_on_data $l : [t0* t] -> [t0* t]`
- iff `$l : [t0* t']`
Expand Down Expand Up @@ -607,11 +643,6 @@ Tentatively, support a type of guaranteed unboxed scalars.
- and `t <: t'`
- passes operand along with branch, plus possible extra args

* `ref.as_func` converts to a function reference
- `ref.as_func : [anyref] -> [(ref func)]`
- traps if reference is not a function
- equivalent to `(block $l (param anyref) (result (ref func)) (br_on_func $l) (unreachable))`

* `ref.as_data` converts to a data reference
- `ref.as_data : [anyref] -> [(ref data)]`
- traps if reference is not compound data
Expand All @@ -636,30 +667,30 @@ Note: The `br_on_*` instructions allow an operand of unrelated reference type, e

RTT-based casts can only be performed with respect to concrete types, and require a data or function reference as input, which are known to carry an RTT.

* `ref.test_canon $t` tests whether a reference value's [runtime type](#values) is a [runtime subtype](#runtime) of a given type
* `ref.test_canon <typeidx>` tests whether a reference value's [runtime type](#values) is a [runtime subtype](#runtime) of a given type
- `ref.test_canon $t : [t'] -> [i32]`
- iff `t' <: (ref null data)` or `t' <: (ref null func)`
- iff `t' <: (ref null data)` and `$t <: data` or `t' <: (ref null func)` and `$t <: func`
- returns 1 if the first operand is not null and its runtime type is a sub-RTT of the RTT operand, 0 otherwise

* `ref.cast_canon $t` casts a reference value down to a type
* `ref.cast_canon <typeidx>` casts a reference value down to a type
- `ref.cast_canon $t : [(ref null1? ht)] -> [(ref null2? $t)]`
- iff `ht <: data` or `ht <: func`
- iff `ht <: data` and `$t <: data` or `ht <: func` and `$t <: func`
- and `null1? = null2?`
- returns null if the first operand is null
- traps if the first operand is not null and its runtime type is not a sub-RTT of `$t`

* `br_on_cast_canon <labelidx>` branches if a value can be cast down to a given reference type
- `br_on_cast_canon $l : [t0* t] -> [t0* t]`
* `br_on_cast_canon <labelidx> <typeidx>` branches if a value can be cast down to a given reference type
- `br_on_cast_canon $l $t : [t0* t] -> [t0* t]`
- iff `$l : [t0* t']`
- and `t <: (ref null data)` or `t <: (ref null func)`
- and `(ref $t') <: t'`
- and `t <: (ref null data)` and `$t <: data` or `t <: (ref null func)` and `$t <: func`
- and `(ref $t) <: t'`
- branches iff the first operand is not null and its runtime type is a sub-RTT of `$t`
- passes cast operand along with branch, plus possible extra args

* `br_on_cast_canon_fail <labelidx>` branches if a value can not be cast down to a given reference type
- `br_on_cast_canon_fail $l $t' : [t0* t] -> [t0* (ref $t')]`
* `br_on_cast_canon_fail <labelidx> <typeidx>` branches if a value can not be cast down to a given reference type
- `br_on_cast_canon_fail $l $t : [t0* t] -> [t0* (ref $t)]`
- iff `$l : [t0* t']`
- and `t <: (ref null data)` or `t <: (ref null func)`
- and `t <: (ref null data)` and `$t <: data` or `t <: (ref null func)` and `$t <: func`
- and `t <: t'`
- branches iff the first operand is null or its runtime type is not a sub-RTT of `$t'`
- passes operand along with branch, plus possible extra args
Expand Down Expand Up @@ -696,11 +727,14 @@ This extends the [encodings](https://github.com/WebAssembly/function-references/
| Opcode | Type | Parameters | Note |
| ------ | --------------- | ---------- | ---- |
| -0x10 | `funcref` | | shorthand, from reftype proposal |
| -0x11 | `anyref` | | shorthand, from reftype proposal |
| -0x11 | `externref` | | shorthand, from reftype proposal |
| -0x12 | `anyref` | | shorthand |
| -0x13 | `eqref` | | shorthand |
| -0x14 | `(ref null ht)` | `ht : heaptype (s33)` | from funcref proposal |
| -0x15 | `(ref ht)` | `ht : heaptype (s33)` | from funcref proposal |
| -0x16 | `i31ref` | | shorthand |
| -0x17 | `nullfuncref` | | shorthand |
| -0x18 | `nullexternref` | | shorthand |
| -0x19 | `dataref` | | shorthand |
| -0x1a | `arrayref` | | shorthand |
| -0x1b | `nullref` | | shorthand |
Expand All @@ -713,9 +747,12 @@ The opcode for heap types is encoded as an `s33`.
| ------ | --------------- | ---------- | ---- |
| i >= 0 | `(type i)` | | from funcref proposal |
| -0x10 | `func` | | from funcref proposal |
| -0x11 | `any` | | from funcref proposal |
| -0x11 | `extern` | | from funcref proposal |
| -0x12 | `any` | | |
| -0x13 | `eq` | | |
| -0x16 | `i31` | | |
| -0x17 | `nofunc` | | |
| -0x18 | `noextern` | | |
| -0x19 | `data` | | |
| -0x1a | `array` | | |
| -0x1b | `none` | | |
Expand Down Expand Up @@ -780,22 +817,20 @@ The opcode for heap types is encoded as an `s33`.
| 0xfb41 | `ref.cast_canon $t` | `$t : typeidx` |
| 0xfb42 | `br_on_cast_canon $l $t` | `$l : labelidx`, `$t : typeidx` |
| 0xfb43 | `br_on_cast_canon_fail $l $t` | `$l : labelidx`, `$t : typeidx` |
| 0xfb50 | `ref.is_func` | |
| 0xfb51 | `ref.is_data` | |
| 0xfb52 | `ref.is_i31` | |
| 0xfb53 | `ref.is_array` | |
| 0xfb58 | `ref.as_func` | |
| 0xfb59 | `ref.as_data` | |
| 0xfb5a | `ref.as_i31` | |
| 0xfb5b | `ref.as_array` | |
| 0xfb60 | `br_on_func` | `$l : labelidx` |
| 0xfb61 | `br_on_data` | `$l : labelidx` |
| 0xfb62 | `br_on_i31` | `$l : labelidx` |
| 0xfb63 | `br_on_non_func` | `$l : labelidx` |
| 0xfb64 | `br_on_non_data` | `$l : labelidx` |
| 0xfb65 | `br_on_non_i31` | `$l : labelidx` |
| 0xfb66 | `br_on_array` | `$l : labelidx` |
| 0xfb67 | `br_on_non_array` | `$l : labelidx` |
| 0xfb70 | `extern.internalize` | |
| 0xfb71 | `extern.externalize` | |


## JS API
Expand Down