Matching¶

On most types, a simple notion of subtyping is defined that is applicable in validation rules or during module instantiation when checking the types of imports.

Todo

externtype matching is used on semantic types; need to define how to reinterpret C for semantic types

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.

\[\begin{split}~\\[-1ex] \frac{ }{ C \href{../valid/matching.html#match-numtype}{\vdash} \href{../syntax/types.html#syntax-numtype}{\mathit{numtype}} \href{../valid/matching.html#match-valtype}{\leq} \href{../syntax/types.html#syntax-numtype}{\mathit{numtype}} }\end{split}\]

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 \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_1\) is a type index that defines a function type and \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_2\) is \(FUNC\).
Or \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_1\) is a type index that defines a function type \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_1\), and \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_2\) is a type index that defines a function type \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_2\), and \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_1\) matches \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_2\).

\[\begin{split}~\\[-1ex] \frac{ }{ C \href{../valid/matching.html#match-heaptype}{\vdash} \href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}} \href{../valid/matching.html#match-heaptype}{\leq} \href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}} } \qquad \frac{ C.\href{../valid/conventions.html#context}{\mathsf{types}}[\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}] = \href{../syntax/types.html#syntax-functype}{\mathit{functype}} }{ C \href{../valid/matching.html#match-heaptype}{\vdash} \href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}} \href{../valid/matching.html#match-heaptype}{\leq} \href{../syntax/types.html#syntax-heaptype}{\mathsf{func}} }\end{split}\]

\[\begin{split}~\\[-1ex] \frac{ C.\href{../valid/conventions.html#context}{\mathsf{types}}[\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}_1] = \href{../syntax/types.html#syntax-functype}{\mathit{functype}}_1 \qquad C.\href{../valid/conventions.html#context}{\mathsf{types}}[\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}_2] = \href{../syntax/types.html#syntax-functype}{\mathit{functype}}_2 \qquad C \href{../valid/matching.html#match-functype}{\vdash} \href{../syntax/types.html#syntax-functype}{\mathit{functype}}_1 \href{../valid/matching.html#match-functype}{\leq} \href{../syntax/types.html#syntax-functype}{\mathit{functype}}_2 }{ C \href{../valid/matching.html#match-heaptype}{\vdash} \href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}_1 \href{../valid/matching.html#match-heaptype}{\leq} \href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}_2 }\end{split}\]

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.

\[\begin{split}~\\[-1ex] \frac{ C \href{../valid/matching.html#match-heaptype}{\vdash} \href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_1 \href{../valid/matching.html#match-heaptype}{\leq} \href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_2 }{ C \href{../valid/matching.html#match-reftype}{\vdash} \href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_1 \href{../valid/matching.html#match-reftype}{\leq} \href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_2 } \qquad \frac{ C \href{../valid/matching.html#match-heaptype}{\vdash} \href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_1 \href{../valid/matching.html#match-heaptype}{\leq} \href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_2 }{ C \href{../valid/matching.html#match-reftype}{\vdash} \href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_1 \href{../valid/matching.html#match-reftype}{\leq} \href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}^?~\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_2 }\end{split}\]

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{../syntax/types.html#syntax-valtype}{\mathsf{bot}}\).

\[\begin{split}~\\[-1ex] \frac{ }{ C \href{../valid/matching.html#match-valtype}{\vdash} \href{../syntax/types.html#syntax-valtype}{\mathsf{bot}} \href{../valid/matching.html#match-valtype}{\leq} \href{../syntax/types.html#syntax-valtype}{\mathit{valtype}} }\end{split}\]

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]\).

\[\begin{split}~\\[-1ex] \frac{ (C \href{../valid/matching.html#match-valtype}{\vdash} t_1 \href{../valid/matching.html#match-valtype}{\leq} t_2)^\ast }{ C \href{../valid/matching.html#match-resulttype}{\vdash} [t_1^\ast] \href{../valid/matching.html#match-resulttype}{\leq} [t_2^\ast] }\end{split}\]

Function Types¶

Subtyping is also defined for function types. However, it is required that they match in both directions, effectively demanding type equivalence. That is, 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_{11}^\ast]\) matches \([t_{21}^\ast]\), and vice versa.
The result type \([t_{12}^\ast]\) matches \([t_{22}^\ast]\), and vice versa.

\[\begin{split}~\\[-1ex] \frac{ \begin{array}{@{}c@{}} C \href{../valid/matching.html#match-resulttype}{\vdash} [t_{11}^\ast] \href{../valid/matching.html#match-resulttype}{\leq} [t_{21}^\ast] \qquad C \href{../valid/matching.html#match-resulttype}{\vdash} [t_{12}^\ast] \href{../valid/matching.html#match-resulttype}{\leq} [t_{22}^\ast] \\ C \href{../valid/matching.html#match-resulttype}{\vdash} [t_{21}^\ast] \href{../valid/matching.html#match-resulttype}{\leq} [t_{11}^\ast] \qquad C \href{../valid/matching.html#match-resulttype}{\vdash} [t_{22}^\ast] \href{../valid/matching.html#match-resulttype}{\leq} [t_{12}^\ast] \end{array} }{ C \href{../valid/matching.html#match-functype}{\vdash} [t_{11}^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_{12}^\ast] \href{../valid/matching.html#match-functype}{\leq} [t_{21}^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_{22}^\ast] }\end{split}\]

Note

In future versions of WebAssembly, subtyping on function types may be relaxed to support co- and contra-variance.

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\).

\[\begin{split}~\\[-1ex] \frac{ n_1 \geq n_2 }{ C \href{../valid/matching.html#match-limits}{\vdash} \{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_1, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m_1^? \} \href{../valid/matching.html#match-limits}{\leq} \{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_2, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~\epsilon \} } \quad \frac{ n_1 \geq n_2 \qquad m_1 \leq m_2 }{ C \href{../valid/matching.html#match-limits}{\vdash} \{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_1, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m_1 \} \href{../valid/matching.html#match-limits}{\leq} \{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_2, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m_2 \} }\end{split}\]

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.

\[\begin{split}~\\[-1ex] \frac{ C \href{../valid/matching.html#match-limits}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1 \href{../valid/matching.html#match-limits}{\leq} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2 \qquad C \href{../valid/matching.html#match-reftype}{\vdash} \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}_1 \href{../valid/matching.html#match-reftype}{\leq} \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}_2 \qquad C \href{../valid/matching.html#match-reftype}{\vdash} \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}_2 \href{../valid/matching.html#match-reftype}{\leq} \href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}_1 }{ C \href{../valid/matching.html#match-tabletype}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1~\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}_1 \href{../valid/matching.html#match-tabletype}{\leq} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2~\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}_2 }\end{split}\]

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\).

\[\begin{split}~\\[-1ex] \frac{ C \href{../valid/matching.html#match-limits}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1 \href{../valid/matching.html#match-limits}{\leq} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2 }{ C \href{../valid/matching.html#match-memtype}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1 \href{../valid/matching.html#match-memtype}{\leq} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2 }\end{split}\]

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\) and \(t_2\) are the same.
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\).

\[\begin{split}~\\[-1ex] \frac{ }{ C \href{../valid/matching.html#match-globaltype}{\vdash} \href{../syntax/types.html#syntax-mut}{\mathsf{var}}~t \href{../valid/matching.html#match-globaltype}{\leq} \href{../syntax/types.html#syntax-mut}{\mathsf{var}}~t } \qquad \frac{ C \href{../valid/matching.html#match-valtype}{\vdash} t_1 \href{../valid/matching.html#match-valtype}{\leq} t_2 }{ C \href{../valid/matching.html#match-globaltype}{\vdash} \href{../syntax/types.html#syntax-mut}{\mathsf{const}}~t_1 \href{../valid/matching.html#match-globaltype}{\leq} \href{../syntax/types.html#syntax-mut}{\mathsf{const}}~t_2 }\end{split}\]

External Types¶

Functions¶

An external type \(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_1\) matches \(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_2\) if and only if:

Function type \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_1\) matches \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_2\).

\[\begin{split}~\\[-1ex] \frac{ C \href{../valid/matching.html#match-functype}{\vdash} \href{../syntax/types.html#syntax-functype}{\mathit{functype}}_1 \href{../valid/matching.html#match-functype}{\leq} \href{../syntax/types.html#syntax-functype}{\mathit{functype}}_2 }{ C \href{../valid/matching.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_1 \href{../valid/matching.html#match-externtype}{\leq} \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_2 }\end{split}\]

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\).

\[\begin{split}~\\[-1ex] \frac{ C \href{../valid/matching.html#match-tabletype}{\vdash} \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}_1 \href{../valid/matching.html#match-tabletype}{\leq} \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}_2 }{ C \href{../valid/matching.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}_1 \href{../valid/matching.html#match-externtype}{\leq} \href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}_2 }\end{split}\]

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\).

\[\begin{split}~\\[-1ex] \frac{ C \href{../valid/matching.html#match-memtype}{\vdash} \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}_1 \href{../valid/matching.html#match-memtype}{\leq} \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}_2 }{ C \href{../valid/matching.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}_1 \href{../valid/matching.html#match-externtype}{\leq} \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}_2 }\end{split}\]

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\).

\[\begin{split}~\\[-1ex] \frac{ C \href{../valid/matching.html#match-globaltype}{\vdash} \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_1 \href{../valid/matching.html#match-globaltype}{\leq} \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_2 }{ C \href{../valid/matching.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_1 \href{../valid/matching.html#match-externtype}{\leq} \href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_2 }\end{split}\]