Matching¶
On most types, a notion of subtyping is defined that is applicable in validation rules, during module instantiation when checking the types of imports, or during execution, when performing casts.
Number Types¶
A number type \(\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}_1\) matches a number type \(\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}_2\) if and only if:
Both \(\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}_1\) and \(\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}_2\) are the same.
Vector Types¶
A vector type \(\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}_1\) matches a vector type \(\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}_2\) if and only if:
Both \(\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}_1\) and \(\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}_2\) are the same.
Heap Types¶
A heap type \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_1\) matches a heap type \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_2\) if and only if:
Either both \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_1\) and \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_2\) are the same.
Or there exists a valid heap type \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'\), such that \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_1\) matches \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'\) and \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'\) matches \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_2\).
Or \(heaptype_1\) is \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{eq}}\) and \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_2\) is \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{any}}\).
Or \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_1\) is one of \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{i31}}\), \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{struct}}\), or \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{array}}\) and \(heaptype_2\) is \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{eq}}\).
Or \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_1\) is a defined type which expands to a structure type and \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_2\) is \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{struct}}\).
Or \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_1\) is a defined type which expands to an array type and \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_2\) is \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{array}}\).
Or \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_1\) is a defined type which expands to a function type and \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_2\) is \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{func}}\).
Or \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_1\) is a defined type \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}_1\) and \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_2\) is a defined type \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}_2\), and \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}_1\) matches \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}_2\).
Or \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_1\) is a type index \(x_1\), and the defined type \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x_1]\) matches \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_2\).
Or \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_2\) is a type index \(x_2\), and \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_1\) matches the defined type \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x_2]\).
Or \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_1\) is \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{none}}\) and \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_2\) matches \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{any}}\).
Or \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_1\) is \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{nofunc}}\) and \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_2\) matches \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{func}}\).
Or \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_1\) is \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{noextern}}\) and \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_2\) matches \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{extern}}\).
Or \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_1\) is \(\href{../valid/conventions.html#syntax-heaptype-ext}{\mathsf{bot}}\).
Reference Types¶
A reference type \(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}_1^?~heaptype_1\) matches a reference type \(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}_2^?~heaptype_2\) if and only if:
The heap type \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_1\) matches \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_2\).
\(\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}_1\) is absent or \(\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}_2\) is present.
Value Types¶
A value type \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_1\) matches a value type \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_2\) if and only if:
Either both \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_1\) and \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_2\) are number types and \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_1\) matches \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_2\).
Or both \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_1\) and \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_2\) are reference types and \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_1\) matches \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_2\).
Or \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_1\) is \(\href{../valid/conventions.html#syntax-valtype-ext}{\mathsf{bot}}\).
Result Types¶
Subtyping is lifted to result types in a pointwise manner. That is, a result type \([t_1^\ast]\) matches a result type \([t_2^\ast]\) if and only if:
Every value type \(t_1\) in \([t_1^\ast]\) matches the corresponding value type \(t_2\) in \([t_2^\ast]\).
Instruction Types¶
Subtyping is further lifted to instruction types. An instruction type \([t_{11}^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x_1^\ast} [t_{12}^\ast]\) matches a type \([t_{21}^ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{x_2^\ast} [t_{22}^\ast]\) if and only if:
There is a common sequence of value types \(t^\ast\) such that \(t_{21}^\ast\) equals \(t^\ast~{t'_{21}}^\ast\) and \(t_{22}^\ast\) equals \(t^\ast~{t'_{22}}^\ast\).
The result type \([{t'_{21}}^\ast]\) matches \([t_{11}^\ast]\).
The result type \([t_{12}^\ast]\) matches \([{t'_{22}}^\ast]\).
For every local index \(x\) that is in \(x_2^\ast\) but not in \(x_1^\ast\), the local type \(C.\href{../valid/conventions.html#context}{\mathsf{locals}}[x]\) is \(\href{../valid/conventions.html#syntax-init}{\mathsf{set}}~t_x\) for some value type \(t_x\).
Note
Instruction types are contravariant in their input and covariant in their output. Subtyping also incorporates a sort of “frame” condition, which allows adding arbitrary invariant stack elements on both sides in the super type.
Finally, the supertype may ignore variables from the init set \(x_1^\ast\). It may also add variables to the init set, provided these are already set in the context, i.e., are vacuously initialized.
Function Types¶
A function type \([t_{11}^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_{12}^\ast]\) matches a type \([t_{21}^ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_{22}^\ast]\) if and only if:
The result type \([t_{21}^\ast]\) matches \([t_{11}^\ast]\).
The result type \([t_{12}^\ast]\) matches \([t_{22}^\ast]\).
Composite Types¶
A composite type \(\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}_1\) matches a type \(\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}_2\) if and only if:
Either the composite type \(\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}_1\) is \(\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_1\) and \(\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}_2\) is \(\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_2\) and:
The function type \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_1\) matches \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_2\).
Or the composite type \(\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}_1\) is \(\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}_1^{n_1}\) and \(\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}_2\) is \(\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}_2\) and:
The arity \(n_1\) is greater than or equal to \(n_2\).
For every field type \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}_{2i}\) in \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}_2^{n_2}\) and corresponding \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}_{1i}\) in \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}_1^{n_1}\)
The field type \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}_{1i}\) matches \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}_{2i}\).
Or the composite type \(\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}_1\) is \(\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}_1\) and \(\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}_2\) is \(\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}_2\) and:
The field type \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}_1\) matches \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}_2\).
Field Types¶
A field type \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}_1~\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}_1\) matches a type \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}_2~\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}_2\) if and only if:
Storage type \(\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}_1\) matches \(\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}_2\).
Either both \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}_1\) and \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}_2\) are \(\href{../syntax/types.html#syntax-mut}{\mathsf{const}}\).
Or both \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}_1\) and \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}_2\) are \(\href{../syntax/types.html#syntax-mut}{\mathsf{var}}\) and \(\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}_2\) matches \(\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}_1\) as well.
A storage type \(\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}_1\) matches a type \(\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}_2\) if and only if:
Either \(\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}_1\) is a value type \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_1\) and \(\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}_2\) is a value type \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_2\) and \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_1\) matches \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}_2\).
Or \(\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}_1\) is a packed type \(\href{../syntax/types.html#syntax-packedtype}{\mathit{packedtype}}_1\) and \(\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}_2\) is a packed type \(\href{../syntax/types.html#syntax-packedtype}{\mathit{packedtype}}_2\) and \(\href{../syntax/types.html#syntax-packedtype}{\mathit{packedtype}}_1\) matches \(\href{../syntax/types.html#syntax-packedtype}{\mathit{packedtype}}_2\).
A packed type \(\href{../syntax/types.html#syntax-packedtype}{\mathit{packedtype}}_1\) matches a type \(\href{../syntax/types.html#syntax-packedtype}{\mathit{packedtype}}_2\) if and only if:
The packed type \(\href{../syntax/types.html#syntax-packedtype}{\mathit{packedtype}}_1\) is the same as \(\href{../syntax/types.html#syntax-packedtype}{\mathit{packedtype}}_2\).
Defined Types¶
A defined type \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}_1\) matches a type \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}_2\) if and only if:
Either \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}_1\) and \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}_2\) are equal when closed under context \(C\).
Or:
Let the sub type \(\href{../syntax/types.html#syntax-subtype}{\mathsf{sub}}~\href{../syntax/types.html#syntax-subtype}{\mathsf{final}}^?~\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}^\ast~\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}\) be the result of unrolling \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}_1\).
Then there must exist a heap type \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_i\) in \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}^\ast\) that matches \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}_2\).
Note
Note that there is no explicit definition of type _equivalence_, since it coincides with syntactic equality, as used in the premise of the former rule above.
Limits¶
Limits \(\{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_1, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m_1^? \}\) match limits \(\{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_2, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m_2^? \}\) if and only if:
\(n_1\) is larger than or equal to \(n_2\).
Either:
\(m_2^?\) is empty.
Or:
Both \(m_1^?\) and \(m_2^?\) are non-empty.
\(m_1\) is smaller than or equal to \(m_2\).
Table Types¶
A table type \((\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1~\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}_1)\) matches \((\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2~\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}_2)\) if and only if:
Limits \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1\) match \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2\).
The reference type \(\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}_1\) matches \(\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}_2\), and vice versa.
Memory Types¶
A memory type \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1\) matches \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2\) if and only if:
Limits \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1\) match \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2\).
Global Types¶
A global type \((\href{../syntax/types.html#syntax-mut}{\mathit{mut}}_1~t_1)\) matches \((\href{../syntax/types.html#syntax-mut}{\mathit{mut}}_2~t_2)\) if and only if:
Either both \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}_1\) and \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}_2\) are \(\href{../syntax/types.html#syntax-mut}{\mathsf{var}}\) and \(t_1\) matches \(t_2\) and vice versa.
Or both \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}_1\) and \(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}_2\) are \(\href{../syntax/types.html#syntax-mut}{\mathsf{const}}\) and \(t_1\) matches \(t_2\).
External Types¶
Functions¶
An external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}_1\) matches \(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}_2\) if and only if:
The defined type \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}_1\) matches \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}_2\).
Tables¶
An external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}_1\) matches \(\href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}_2\) if and only if:
Table type \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}_1\) matches \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}_2\).
Memories¶
An external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}_1\) matches \(\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}_2\) if and only if:
Memory type \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}_1\) matches \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}_2\).
Globals¶
An external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_1\) matches \(\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_2\) if and only if:
Global type \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_1\) matches \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_2\).