First go at MVP proposal (WebAssembly#34)

proposals/gc/MVP.md

@@ -0,0 +1,317 @@
+# GC v1 Extensions
+
+*Note: This design is still in flux!*
+
+See [overview](Overview.md) for background.
+
+
+## Language
+
+Based on [reference types proposal](https://github.com/WebAssembly/reference-types), which introduces type `anyref` etc.
+
+### Types
+
+#### Value Types
+
+* `eqref` is a new reference type
+  - `reftype ::= ... | eqref`
+
+* `ref <typeidx>` is a new reference type
+  - `reftype ::= ... | ref <typeidx>`
+  - `ref $t ok` iff `$t` is defined in the context
+
+* `optref <typeidx>` is a new reference type
+  - `reftype ::= ... | optref <typeidx>`
+  - `optref $t ok` iff `$t` is defined in the context
+
+* `i31ref` is a new reference type
+  - `reftype ::= ... | i31ref`
+
+
+#### Type Definitions
+
+* `deftype` is a new category of types that generalises the existing type definitions in the type section
+  - `deftype ::= <functype> | <structtype> | <arraytype>`
+  - `module ::= {..., types vec(<deftype>)}`
+
+* `structtype` describes a structure with statically indexed fields
+  - `structtype ::= struct <fieldtype>*`
+
+* `arraytype` describes an array with dynamically indexed fields
+  - `arraytype ::= array <fieldtype>`
+
+* `fieldtype` describes a struct or array field and whether it is mutable
+  - `fieldtype ::= <mutability> <storagetype>`
+  - `storagetype ::= <valtype> | <packedtype>`
+  - `packedtype ::= i8 | i16`
+
+* Unpacking a storage type yields `i32` for packed types, otherwise the type itself
+  - `unpacked(t) = t`
+  - `unpacked(pt) = i32`
+
+
+#### Imports
+
+* `type <typetype>` is an import description with an upper bound
+  - `importdesc ::= ... | type <reftype>`
+  - Note: `type` may get additional parameters in the future
+
+* Type imports have indices prepended to the type index space, similar to other imports.
+  - Note: due to bounds, type imports can be mutually recursive with other type imports as well as regular type definitions. Hence they have to be validated together with the type section.
+
+
+#### Exports
+
+* `type <typeidx>` is an export description
+  - `exportdesc ::= ... | type <typeidx>`
+  - `type $t ok` iff `$t` is defined in the context
+
+
+#### Subtyping
+
+Greatest fixpoint (co-inductive interpretation) of the given rules (implying reflexivity and transitivity).
+
+In addition to the rules for basic reference types:
+
+* `eqref` is a subtype of `anyref`
+  - `eqref <: anyref`
+  - Note: `i31ref` and `anyfunc` are *not* a subtypes of `eqref`, i.e., those types do not expose reference equality
+
+* `nullref` is a subtype of `eqref`
+  - `nullref <: eqref`
+
+* `i31ref` is a subtype of `anyref`
+  - `i31ref <: anyref`
+  - Note: `i31ref` is *not* a supertype of `nullref`, i.e., nut nullable
+
+* Any nullable reference type is a subtype of `anyref` and a supertype of `nullref`
+  - `optref $t <: anyref`
+  - `nullref <: optref $t`
+
+* Any concrete reference type is a subtype of the respective nullable reference type (and thereby of `anyref`)
+  - `ref $t <: optref $t`
+  - Note: concrete reference types are *not* supertypes of `nullref`, i.e., not nullable
+
+* Any function reference type is a subtype of `anyfunc`
+  - `ref $t <: anyfunc`
+     - iff `$t = <functype>`
+
+* Any optional reference type (and thereby respective concrete reference type) is a subtype of `eqref` if its not a function
+  - `optref $t <: eqref`
+     - if `$t = <structtype>` or `$t = <arraytype>`
+     - or `$t = type rt` and `rt <: eqref`
+  - TODO: provide a way to make data types non-eq, especially immutable ones
+
+* Concrete and optional reference types are covariant
+  - `ref $t1 <: ref $t2`
+     - iff `$t1 <: $t2`
+  - `optref $t1 <: optref $t2`
+     - iff `$t1 <: $t2`
+
+* Structure types support width and depth subtyping
+  - `struct <fieldtype1>* <fieldtype1'>* <: struct <fieldtype2>*`
+    - iff `(<fieldtype1> <: <fieldtype2>)*`
+
+* Array types support depth subtyping
+  - `array <fieldtype1> <: array <fieldtype2>`
+    - iff `<fieldtype1> <: <fieldtype2>`
+
+* Field types are covariant if they are immutable, invariant otherwise
+  - `const <valtype1> <: const <valtype2>`
+    - iff `<valtype1> <: <valtype2>`
+  - `var <valtype> <: var <valtype>`
+  - Note: mutable fields are *not* subtypes of immutable ones, so `const` really means constant, not read-only
+
+
+#### Defaultability
+
+* Any numeric value type is defaultable
+
+* A reference value type is defaultable if it is not of the form `ref $t`
+
+* Locals must have a type that is defaultable.
+
+* Table definitions with non-zero minimum size must have an element type that is defaultable. (Imports are not affected.)
+
+
+### Instructions
+
+#### Equality
+
+* `ref.eq` compares two references whose types support equality
+  - `ref.eq : [eqref eqref] -> [i32]`
+
+
+#### Functions
+
+* `ref.func` creates a function reference from a function index
+  - `ref.func $f : [] -> (ref $t)`
+     - iff `$f : $t`
+
+* `call_ref` calls a function through a reference
+  - `call_ref : [t1* (optref $t)] -> [t2*]`
+     - iff `$t = [t1*] -> [t2*]`
+  - traps on `null`
+
+
+#### Structures
+
+* `struct.new <typeidx>` allocates a structure of type `$t` and initialises its fields with given values
+  - `struct.new $t : [t*] -> [(ref $t)]`
+    - iff `$t = struct (mut t)*`
+
+* `struct.new_default <typeidx>` allocates a structure of type `$t` and initialises its fields with default values
+  - `struct.new_default $t : [] -> [(ref $t)]`
+    - iff `$t = struct (mut t)*`
+    - and all `t*` are defaultable
+
+* `struct.get <typeidx> <fieldidx>` reads field `$x` from a structure
+  - `struct.get $t i : [(optref $t)] -> [t]`
+    - iff `$t = struct (mut1 t1)^i (mut ti) (mut2 t2)*`
+    - and `t = unpacked(ti)`
+  - traps on `null`
+
+* `struct.set <typeidx> <fieldidx>` writes field `$x` of a structure
+  - `struct.set $t i : [(optref $t) ti] -> []`
+    - iff `$t = struct (mut1 t1)^i (var ti) (mut2 t2)*`
+    - and `t = unpacked(ti)`
+  - traps on `null`
+
+
+#### Arrays
+
+* `array.new <typeidx>` allocates an array of type `$t` and initialises its fields with a given value
+  - `array.new $t : [t i32] -> [(ref $t)]`
+    - iff `$t = array (mut t)`
+
+* `array.new_default <typeidx>` allocates an array of type `$t` and initialises its fields with the default value
+  - `array.new_default $t : [i32] -> [(ref $t)]`
+    - iff `$t = array (mut t)`
+    - and `t` is defaultable
+
+* `array.get <typeidx>` reads an element from an array
+  - `array.get $t : [(optref $t) i32] -> [t]`
+    - iff `$t = array (mut t')`
+    - and `t = unpacked(t')`
+  - traps on `null`
+
+* `array.set <typeidx>` writes an element to an array
+  - `array.set $t : [(optref $t) i32 t] -> []`
+    - iff `$t = array (var t')`
+    - and `t = unpacked(t')`
+  - traps on `null`
+
+* `array.len <typeidx>` inquires the length of an array
+  - `array.len $t : [(optref $t)] -> [i32]`
+    - iff `$t = array (mut t)`
+  - traps on `null`
+
+
+#### Integer references
+
+Tentatively, support a type of guaranteed unboxed scalars.
+TODO: Is 31 bit value range the right choice?
+
+* `i31ref.new` creates an `i31ref` from a 32 bit value, truncating high bit
+  - `i31ref : [i32] -> [i31ref]`
+
+* `i31ref.get_u` extracts the value, zero-extending
+  - `i31ref.get_u : [i31ref] -> [i32]`
+
+* `i31ref.get_s` extracts the value, sign-extending
+  - `i31ref.get_s : [i31ref] -> [i32]`
+
+
+#### Casts
+
+TODO. Want to introduce explicit runtime type values to support casts in a pay-as-you-go manner. Deferred to a separate PR. Casts themselves could then look something like this:
+
+* `cast <reftype> <reftype>` casts a value down to a given reference type
+  - `cast t t' : [t (rtti t')] -> [t']`
+     - iff `t' <: t <: anyref`
+  - traps if the operand is not of type `t'` at runtime
+  - equivalent to `block [t (rtti t')]->[t'] (br_on_cast 0 t t') unreachable end`
+
+* `br_on_cast <labelidx> <reftype> <reftype>` branches if a value can be cast down to a given reference type
+  - `br_on_cast $l t t' : [t (rtti t')] -> [t]`
+    - iff `t' <: t <: anyref`
+    - and `$l : [t']`
+  - passes cast operand along with branch
+
+
+#### Local Bindings
+
+* `let <valtype>* <blocktype> <instr>* end` locally binds operands to variables
+  - `let t* bt instr* end : [t* t1*] -> [t2*]`
+    - iff `bt = [t1*] -> [t2*]`
+    - and `instr* : bt` under a context with `locals` extended by `t*` and `labels` extended by `[t2*]`
+
+
+## Binary Format
+
+TODO.
+
+
+## JS API
+
+Based on the JS type reflection proposal.
+
+### Type Representation
+
+* A `ValueType` can be described by an object of the form `{ref: DefType}` and `{optref: DefType}`
+  - `type ValueType = ... | {ref: DefType} | {optref: DefType}`
+
+* A `ValueType` can be described by the string `eqref`
+  - `type ValueType = ... | "eqref"`
+
+* A `DefType` is described by a kind and a definition
+  - `type DefKind = "func" | "struct" | "array"`
+  - `type DefType = {kind: DefKind, definition: FuncType | StructType | ArrayType}`
+
+* TODO: ...`StructType` and `ArrayType`...
+
+
+### Value Conversions
+
+#### Reference Types
+
+In addition to the rules for basic reference types:
+
+* Any function that is an instance of `WebAssembly.Function` with type `<functype>` is allowed as `ref <functype>`.
+
+* The `null` value is allowed as `eqref` and `optref $t`.
+
+* TODO: ...rules for structure and array types.
+
+
+#### Equality Types
+
+* Any JS object (non-primitive value) or symbol or `null` can be passed as `eqref` to a Wasm function, stored in a global, or in a table.
+
+
+### Constructors
+
+#### `Global`
+
+* `TypeError` is produced if the `Global` constructor is invoked without a value argument but a type that is not defaultable.
+
+#### `Table`
+
+* The `Table` constructor gets an additional optional argument `init` that is used to initialise the table slots. It defaults to `null`. A `TypeError` is produced if the argument is omitted and the table's element type is not defaultable.
+
+#### `Type`
+
+TODO.
+
+
+## Questions
+
+* Have explicit RTTI representations?
+
+* Distinguish reference types that are castable (and therefore have RTTI)?
+
+* Provide a way to make data types non-eq, especially immutable ones?
+
+* Allow closures into function reference types, via a `func.bind` operator?
+
+* Should we rename `anyfunc` to `funcref` for more consistency?

proposals/gc/Overview.md

@@ -4,6 +4,8 @@
 
 Note: Basic support for simple host reference types has been carved out into a [separate proposal](https://github.com/WebAssembly/reference-types/blob/master/proposals/reference-types/Overview.md) that should become the future basis for this proposal.
 
+See [MVP](MVP.md) for a concrete v1 proposal.
+
 
 ### Motivation
 
@@ -33,10 +35,10 @@ Note: Basic support for simple host reference types has been carved out into a [
 
 ### Approach
 
-* Only basic but general structure: structs and arrays
+* Only basic but general structure: tuples (structs) and arrays
 * No heavyweight object model
-* Accept minimal amount of dynamic overhead (checked casts) as price for simplicity/universality
 * Independent from linear memory
+* Accept minimal amount of dynamic overhead (checked casts) as price for simplicity/universality
 * Pay as you go; in particular, no effect on code not using GC
 * Don't introduce dependencies on GC for other features (e.g., using resources through tables)
 * Avoid generics or other complex type structure _if possible_