Remove subtyping (#87)

Per the vote on #69, this PR removes subtyping from the proposal. List of changes:

* Syntax:
  - remove `nullref` type
  - rename `anyref` type to `externref`
  - extend `ref.null` and `ref.is_null` instructions with new immediate of the form `func` or `extern` (this will later have to generalise to a `constype` per the [typed references proposal](https://github.com/WebAssembly/function-references))
* Typing rules:
  - `ref.null`, `ref.is_null`: determine reference type based on new immediate
  - `select`, `call_indirect`, `table.copy`, `table.init`: drop subtyping
  - `br_table`: revert to rule requiring same label types
  - `elem` segment: drop subtyping
  - `global` import: drop subtyping (link time)
* Remove subtyping rules and bottom type.
* Revert typing algorithm (interpreter and spec appendix).
* JS API:
  - remove `"nullref"`
  - rename `"anyref"` to `"externref"`
* Scripts:
  - rename `ref` result to `ref.extern`
  - rename `ref.host` value to `ref.extern`
  - drop subtyping from invocation type check
* JS translation:
  - extend harness with separate eq functions for each ref type
* Adjust tests:
  - apply syntax changes
  - remove tests for subtyping
  - change tests exercising subtyping in other ways

Author: rossberg

document/core/appendix/algorithm.rst

@@ -22,29 +22,24 @@ Data Structures
 ~~~~~~~~~~~~~~~
 
 Types are representable as an enumeration.
-A simple subtyping check can be defined on these types.
 
 .. code-block:: pseudo
 
-   type val_type = I32 | I64 | F32 | F64 | Anyref | Funcref | Nullref | Bot
+   type val_type = I32 | I64 | F32 | F64 | Funcref | Externref
 
    func is_num(t : val_type) : bool =
-     return t = I32 || t = I64 || t = F32 || t = F64 || t = Bot
+     return t = I32 || t = I64 || t = F32 || t = F64
 
    func is_ref(t : val_type) : bool =
-     return t = Anyref || t = Funcref || t = Nullref || t = Bot
-
-   func matches(t1 : val_type, t2 : val_type) : bool =
-     return t1 = t2 || t1 = Bot ||
-       (t1 = Nullref && is_ref(t2)) || (is_ref(t1) && t2 = Anyref)
+     return t = Funcref || t = Externref
 
 The algorithm uses two separate stacks: the *value stack* and the *control stack*.
 The former tracks the :ref:`types <syntax-valtype>` of operand values on the :ref:`stack <stack>`,
 the latter surrounding :ref:`structured control instructions <syntax-instr-control>` and their associated :ref:`blocks <syntax-instr-control>`.
 
 .. code-block:: pseudo
 
-   type val_stack = stack(val_type)
+   type val_stack = stack(val_type | Unknown)
 
    type ctrl_stack = stack(ctrl_frame)
    type ctrl_frame = {
@@ -54,7 +49,8 @@ the latter surrounding :ref:`structured control instructions <syntax-instr-contr
      unreachable : bool
    }
 
-For each value, the value stack records its :ref:`value type <syntax-valtype>`.
+For each value, the value stack records its :ref:`value type <syntax-valtype>`, or :code:`Unknown` when the type is not known.
+
 
 For each entered block, the control stack records a *control frame* with the type of the associated :ref:`label <syntax-label>` (used to type-check branches), the result type of the block (used to check its result), the height of the operand stack at the start of the block (used to check that operands do not underflow the current block), and a flag recording whether the remainder of the block is unreachable (used to handle :ref:`stack-polymorphic <polymorphism>` typing after branches).
 
@@ -73,17 +69,19 @@ However, these variables are not manipulated directly by the main checking funct
 
 .. code-block:: pseudo
 
-   func push_val(type : val_type) =
+   func push_val(type : val_type | Unknown) =
      vals.push(type)
 
-   func pop_val() : val_type =
-     if (vals.size() = ctrls[0].height && ctrls[0].unreachable) return Bot
+   func pop_val() : val_type | Unknown =
+     if (vals.size() = ctrls[0].height && ctrls[0].unreachable) return Unknown
      error_if(vals.size() = ctrls[0].height)
      return vals.pop()
 
-   func pop_val(expect : val_type) : val_type =
+   func pop_val(expect : val_type | Unknown) : val_type | Unknown =
      let actual = pop_val()
-     error_if(not matches(actual, expect))
+     if (actual = Unknown) return expect
+     if (expect = Unknown) return actual
+     error_if(actual =/= expect)
      return actual
 
    func push_vals(types : list(val_type)) = foreach (t in types) push_val(t)
@@ -97,10 +95,10 @@ Pushing an operand value simply pushes the respective type to the value stack.
 Popping an operand value checks that the value stack does not underflow the current block and then removes one type.
 But first, a special case is handled where the block contains no known values, but has been marked as unreachable.
 That can occur after an unconditional branch, when the stack is typed :ref:`polymorphically <polymorphism>`.
-In that case, the :code:`Bot` type is returned, because that is a *principal* choice trivially satisfying all use constraints.
+In that case, an unknown type is returned.
 
 A second function for popping an operand value takes an expected type, which the actual operand type is checked against.
-The types may differ by subtyping, including the case where the actual type is :code:`Bot`, and thereby matches unconditionally.
+The types may differ in case one of them is Unknown.
 The function returns the actual type popped from the stack.
 
 Finally, there are accumulative functions for pushing or popping multiple operand types.
@@ -143,7 +141,7 @@ In that case, all existing operand types are purged from the value stack, in ord
 .. note::
    Even with the unreachable flag set, consecutive operands are still pushed to and popped from the operand stack.
    That is necessary to detect invalid :ref:`examples <polymorphism>` like :math:`(\UNREACHABLE~(\I32.\CONST)~\I64.\ADD)`.
-   However, a polymorphic stack cannot underflow, but instead generates :code:`Bot` types as needed.
+   However, a polymorphic stack cannot underflow, but instead generates :code:`Unknown` types as needed.
 
 
 .. index:: opcode
@@ -175,8 +173,8 @@ Other instructions are checked in a similar manner.
          let t1 = pop_val()
          let t2 = pop_val()
          error_if(not (is_num(t1) && is_num(t2)))
-         error_if(t1 =/= t2 && t1 =/= Bot && t2 =/= Bot)
-         push_val(if (t1 = Bot) t2 else t1)
+         error_if(t1 =/= t2 && t1 =/= Unknown && t2 =/= Unknown)
+         push_val(if (t1 = Unknown) t2 else t1)
 
        case (select t)
          pop_val(I32)
@@ -217,14 +215,11 @@ Other instructions are checked in a similar manner.
          push_vals(ctrls[n].label_types)
 
        case (br_table n* m)
-         pop_val(I32)
          error_if(ctrls.size() < m)
-         let arity = ctrls[m].label_types.size()
          foreach (n in n*)
-           error_if(ctrls.size() < n)
-           error_if(ctrls[n].label_types.size() =/= arity)
-           push_vals(pop_vals(ctrls[n].label_types))
-         pop_vals(ctrls[m].label_types)
+           error_if(ctrls.size() < n || ctrls[n].label_types =/= ctrls[m].label_types)
+         pop_val(I32)
+         pop_vals(ctrls[m].label_types)
          unreachable()
 
 .. note::

document/core/appendix/index-instructions.rst

@@ -215,8 +215,8 @@ Instruction                             Binary Opcode       Type
 (reserved)                              :math:`\hex{CD}`                                                  
 (reserved)                              :math:`\hex{CE}`                                                  
 (reserved)                              :math:`\hex{CF}`                                                  
-:math:`\REFNULL`                        :math:`\hex{D0}`    :math:`[] \to [\NULLREF]`                   :ref:`validation <valid-ref.null>`        :ref:`execution <exec-ref.null>`
-:math:`\REFISNULL`                      :math:`\hex{D1}`    :math:`[\ANYREF] \to [\I32]`                :ref:`validation <valid-ref.is_null>`     :ref:`execution <exec-ref.is_null>`
+:math:`\REFNULL~t`                      :math:`\hex{D0}`    :math:`[] \to [t]`                          :ref:`validation <valid-ref.null>`        :ref:`execution <exec-ref.null>`
+:math:`\REFISNULL~t`                    :math:`\hex{D1}`    :math:`[t] \to [\I32]`                      :ref:`validation <valid-ref.is_null>`     :ref:`execution <exec-ref.is_null>`
 :math:`\REFFUNC~x`                      :math:`\hex{D2}`    :math:`[] \to [\FUNCREF]`                   :ref:`validation <valid-ref.func>`        :ref:`execution <exec-ref.func>`
 :math:`\MEMORYINIT`                     :math:`\hex{FC08}`  :math:`[\I32~\I32~\I32] \to []`             :ref:`validation <valid-memory.init>`     :ref:`execution <exec-memory.init>`
 :math:`\DATADROP`                       :math:`\hex{FC09}`  :math:`[] \to []`                           :ref:`validation <valid-data.drop>`       :ref:`execution <exec-data.drop>`

document/core/appendix/index-rules.rst

@@ -82,10 +82,6 @@ Matching
 ===============================================  ===============================================================================
 Construct                                        Judgement
 ===============================================  ===============================================================================
-:ref:`Number type <match-numtype>`               :math:`\vdashnumtypematch \numtype_1 \matchesvaltype \numtype_2`
-:ref:`Reference type <match-reftype>`            :math:`\vdashreftypematch \reftype_1 \matchesvaltype \reftype_2`
-:ref:`Value type <match-valtype>`                :math:`\vdashvaltypematch \valtype_1 \matchesvaltype \valtype_2`
-:ref:`Result type <match-resulttype>`            :math:`\vdashresulttypematch [t_1^?] \matchesresulttype [t_2^?]`
 :ref:`External type <match-externtype>`          :math:`\vdashexterntypematch \externtype_1 \matchesexterntype \externtype_2`
 :ref:`Limits <match-limits>`                     :math:`\vdashlimitsmatch \limits_1 \matcheslimits \limits_2`
 ===============================================  ===============================================================================

document/core/appendix/index-types.rst

@@ -14,9 +14,8 @@ Category                                  Constructor
 :ref:`Number type <syntax-numtype>`       |F64|                                        :math:`\hex{7C}` (-4 as |Bs7|)
 (reserved)                                                                             :math:`\hex{7B}` .. :math:`\hex{71}`
 :ref:`Reference type <syntax-reftype>`    |FUNCREF|                                    :math:`\hex{70}` (-16 as |Bs7|)
-:ref:`Reference type <syntax-reftype>`    |ANYREF|                                     :math:`\hex{6F}` (-17 as |Bs7|)
-:ref:`Reference type <syntax-reftype>`    |NULLREF|                                    :math:`\hex{6E}` (-18 as |Bs7|)
-(reserved)                                                                             :math:`\hex{6D}` .. :math:`\hex{61}`
+:ref:`Reference type <syntax-reftype>`    |EXTERNREF|                                  :math:`\hex{6F}` (-17 as |Bs7|)
+(reserved)                                                                             :math:`\hex{6E}` .. :math:`\hex{61}`
 :ref:`Function type <syntax-functype>`    :math:`[\valtype^\ast] \to [\valtype^\ast]`  :math:`\hex{60}` (-32 as |Bs7|)
 (reserved)                                                                             :math:`\hex{5F}` .. :math:`\hex{41}`
 :ref:`Result type <syntax-resulttype>`    :math:`[\epsilon]`                             :math:`\hex{40}` (-64 as |Bs7|)

document/core/appendix/properties.rst

@@ -215,9 +215,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
 
 * For each :ref:`reference <syntax-ref>` :math:`\reff_i` in the table's elements :math:`\reff^n`:
 
-  * The :ref:`reference <syntax-ref>` :math:`\reff_i` must be :ref:`valid <valid-ref>` with some :ref:`reference type <syntax-reftype>` :math:`t'_i`.
-
-  * The :ref:`reference type <syntax-reftype>` :math:`t'_i` must :ref:`match <match-reftype>` the :ref:`reference type <syntax-reftype>` :math:`t`.
+  * The :ref:`reference <syntax-ref>` :math:`\reff_i` must be :ref:`valid <valid-ref>` with :ref:`reference type <syntax-reftype>` :math:`t`.
 
 * Then the table instance is valid with :ref:`table type <syntax-tabletype>` :math:`\limits~t`.
 
@@ -227,9 +225,7 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
      \qquad
      n = \limits.\LMIN
      \qquad
-     (S \vdash \reff : t')^n
-     \qquad
-     (\vdashreftypematch t' \matchesvaltype t)^n
+     (S \vdash \reff : t)^n
    }{
      S \vdashtableinst \{ \TITYPE~(\limits~t), \TIELEM~\reff^n \} : \limits~t
    }
@@ -265,19 +261,15 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
 
 * The :ref:`global type <syntax-globaltype>` :math:`\mut~t` must be :ref:`valid <valid-globaltype>`.
 
-* The :ref:`value <syntax-val>` :math:`\val` must be :ref:`valid <valid-val>` with some :ref:`value type <syntax-valtype>` :math:`t'`.
-
-* The :ref:`value type <syntax-valtype>` :math:`t'` must :ref:`match <match-valtype>` the :ref:`value type <syntax-valtype>` :math:`t`.
+* The :ref:`value <syntax-val>` :math:`\val` must be :ref:`valid <valid-val>` with :ref:`value type <syntax-valtype>` :math:`t`.
 
 * Then the global instance is valid with :ref:`global type <syntax-globaltype>` :math:`\mut~t`.
 
 .. math::
    \frac{
      \vdashglobaltype \mut~t \ok
      \qquad
-     S \vdashval \val : t'
-     \qquad
-     \vdashvaltypematch t' \matchesvaltype t
+     S \vdashval \val : t
    }{
      S \vdashglobalinst \{ \GITYPE~(\mut~t), \GIVALUE~\val \} : \mut~t
    }
@@ -291,17 +283,13 @@ Module instances are classified by *module contexts*, which are regular :ref:`co
 
 * For each :ref:`reference <syntax-ref>` :math:`\reff_i` in the elements :math:`\reff^n`:
 
-  * The :ref:`reference <syntax-ref>` :math:`\reff_i` must be :ref:`valid <valid-ref>` with some :ref:`reference type <syntax-reftype>` :math:`t'_i`.
-
-  * The :ref:`reference type <syntax-reftype>` :math:`t'_i` must :ref:`match <match-reftype>` the :ref:`reference type <syntax-reftype>` :math:`t`.
+  * The :ref:`reference <syntax-ref>` :math:`\reff_i` must be :ref:`valid <valid-ref>` with :ref:`reference type <syntax-reftype>` :math:`t`.
 
 * Then the table instance is valid.
 
 .. math::
    \frac{
-     (S \vdash \reff : t')^\ast
-     \qquad
-     (\vdashreftypematch t' \matchesvaltype t)^\ast
+     (S \vdash \reff : t)^\ast
    }{
      S \vdasheleminst \{ \EITYPE~t, \EIELEM~\reff^\ast \} \ok
    }
@@ -535,17 +523,17 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
    }
 
 
-.. index:: host address
+.. index:: extern address
 
-:math:`\REFHOST~\hostaddr`
-..........................
+:math:`\REFEXTERNADDR~\externaddr`
+..................................
 
-* The instruction is valid with type :math:`[] \to [\ANYREF]`.
+* The instruction is valid with type :math:`[] \to [\EXTERNREF]`.
 
 .. math::
    \frac{
    }{
-     S; C \vdashadmininstr \REFHOST~\hostaddr : [] \to [\ANYREF]
+     S; C \vdashadmininstr \REFEXTERNADDR~\externaddr : [] \to [\EXTERNREF]
    }
 
 

document/core/binary/instructions.rst

@@ -76,8 +76,8 @@ Reference Instructions
 .. math::
    \begin{array}{llclll}
    \production{instruction} & \Binstr &::=& \dots \\ &&|&
-     \hex{D0} &\Rightarrow& \REFNULL \\ &&|&
-     \hex{D1} &\Rightarrow& \REFISNULL \\ &&|&
+     \hex{D0}~~t{:}\Breftype &\Rightarrow& \REFNULL~t \\ &&|&
+     \hex{D1}~~t{:}\Breftype &\Rightarrow& \REFISNULL~t \\ &&|&
      \hex{D2}~~x{:}\Bfuncidx &\Rightarrow& \REFFUNC~x \\
    \end{array}
 

document/core/binary/types.rst

@@ -42,8 +42,7 @@ Reference Types
    \begin{array}{llclll@{\qquad\qquad}l}
    \production{reference type} & \Breftype &::=&
      \hex{70} &\Rightarrow& \FUNCREF \\ &&|&
-     \hex{6F} &\Rightarrow& \ANYREF \\ &&|&
-     \hex{6E} &\Rightarrow& \NULLREF \\
+     \hex{6F} &\Rightarrow& \EXTERNREF \\
    \end{array}
 
 

document/core/exec/instructions.rst

@@ -192,25 +192,25 @@ Reference Instructions
 
 .. _exec-ref.null:
 
-:math:`\REFNULL`
-................
+:math:`\REFNULL~t`
+..................
 
-1. Push the value :math:`\REFNULL` to the stack.
+1. Push the value :math:`\REFNULL~t` to the stack.
 
 .. note::
    No formal reduction rule is required for this instruction, since the |REFNULL| instruction is already a :ref:`value <syntax-val>`.
 
 
 .. _exec-ref.is_null:
 
-:math:`\REFISNULL`
-..................
+:math:`\REFISNULL~t`
+....................
 
 1. Assert: due to :ref:`validation <valid-ref.is_null>`, a :ref:`reference value <syntax-ref>` is on the top of the stack.
 
 2. Pop the value :math:`\val` from the stack.
 
-3. If :math:`\val` is |REFNULL|, then:
+3. If :math:`\val` is :math:`\REFNULL~t`, then:
 
    a. Push the value :math:`\I32.\CONST~1` to the stack.
 
@@ -220,10 +220,10 @@ Reference Instructions
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
-   \val~\REFISNULL &\stepto& \I32.\CONST~1
-     & (\iff \val = \REFNULL) \\
-   \val~\REFISNULL &\stepto& \I32.\CONST~0
-     & (\iff \val \neq \REFNULL) \\
+   \val~\REFISNULL~t &\stepto& \I32.\CONST~1
+     & (\iff \val = \REFNULL~t) \\
+   \val~\REFISNULL~t &\stepto& \I32.\CONST~0
+     & (\otherwise) \\
    \end{array}
 
 
@@ -1768,7 +1768,7 @@ Control Instructions
 
 11. Let :math:`r` be the :ref:`reference <syntax-ref>` :math:`\X{tab}.\TIELEM[i]`.
 
-12. If :math:`r` is |REFNULL|, then:
+12. If :math:`r` is :math:`\REFNULL~t`, then:
 
     a. Trap.
 

document/core/exec/modules.rst

@@ -110,15 +110,15 @@ The following auxiliary typing rules specify this typing relation relative to a
 
 .. _valid-ref:
 
-:ref:`Null References <syntax-ref>` :math:`\REFNULL`
-....................................................
+:ref:`Null References <syntax-ref>` :math:`\REFNULL~t`
+......................................................
 
-* The value is valid with :ref:`reference type <syntax-reftype>` :math:`\NULLREF`.
+* The value is valid with :ref:`reference type <syntax-reftype>` :math:`t`.
 
 .. math::
    \frac{
    }{
-     S \vdashval \REFNULL : \NULLREF
+     S \vdashval \REFNULL~t : t
    }
 
 
@@ -137,15 +137,15 @@ The following auxiliary typing rules specify this typing relation relative to a
    }
 
 
-:ref:`Host References <syntax-ref.host>` :math:`\REFHOST~a`
-...........................................................
+:ref:`External References <syntax-ref.extern>` :math:`\REFEXTERNADDR~a`
+.......................................................................
 
-* The value is valid with :ref:`reference type <syntax-reftype>` :math:`\ANYREF`.
+* The value is valid with :ref:`reference type <syntax-reftype>` :math:`\EXTERNREF`.
 
 .. math::
    \frac{
    }{
-     S \vdashval \REFHOST~a : \ANYREF
+     S \vdashval \REFEXTERNADDR~a : \EXTERNREF
    }
 
 
@@ -447,7 +447,10 @@ and list of :ref:`reference <syntax-ref>` vectors for the module's :ref:`element
 
 3. For each :ref:`table <syntax-table>` :math:`\table_i` in :math:`\module.\MTABLES`, do:
 
-   a. Let :math:`\tableaddr_i` be the :ref:`table address <syntax-tableaddr>` resulting from :ref:`allocating <alloc-table>` :math:`\table_i.\TTYPE`.
+   a. Let :math:`\limits_i~t_i` be the :ref:`table type <syntax-tabletype>` :math:`\table_i.\TTYPE`.
+
+   b. Let :math:`\tableaddr_i` be the :ref:`table address <syntax-tableaddr>` resulting from :ref:`allocating <alloc-table>` :math:`\table_i.\TTYPE`
+   with initialization value :math:`\REFNULL~t_i`.
 
 4. For each :ref:`memory <syntax-mem>` :math:`\mem_i` in :math:`\module.\MMEMS`, do:
 
@@ -526,8 +529,9 @@ where:
      \MIEXPORTS~\exportinst^\ast ~\}
      \end{array} \\[1ex]
    S_1, \funcaddr^\ast &=& \allocfunc^\ast(S, \module.\MFUNCS, \moduleinst) \\
-   S_2, \tableaddr^\ast &=& \alloctable^\ast(S_1, (\table.\TTYPE)^\ast, \REFNULL)
-     \qquad\qquad\qquad~ (\where \table^\ast = \module.\MTABLES) \\
+   S_2, \tableaddr^\ast &=& \alloctable^\ast(S_1, (\table.\TTYPE)^\ast, \REFNULL~t)
+     \qquad\qquad\qquad~ (\where \table^\ast = \module.\MTABLES \\ &&
+     \qquad\qquad\qquad~~ \wedge (\table.\TTYPE)^\ast = (\limits~t)^\ast) \\
    S_3, \memaddr^\ast &=& \allocmem^\ast(S_2, (\mem.\MTYPE)^\ast)
      \qquad\qquad\qquad~ (\where \mem^\ast = \module.\MMEMS) \\
    S_4, \globaladdr^\ast &=& \allocglobal^\ast(S_3, (\global.\GTYPE)^\ast, \val^\ast)