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.
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:
\[\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}\]
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:
\[\begin{split}~\\[-1ex]
\frac{
}{
C \href{../valid/matching.html#match-vectype}{\vdash} \href{../syntax/types.html#syntax-vectype}{\mathit{vectype}} \href{../valid/matching.html#match-valtype}{\leq} \href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}
}\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 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 function type \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_1\) and \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_2\) is 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\).
Or \(\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_1\) is a type index \(x_1\), and \(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 \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[x_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/matching.html#match-heaptype}{\vdash} \href{../syntax/types.html#syntax-functype}{\mathit{functype}} \href{../valid/matching.html#match-heaptype}{\leq} \href{../syntax/types.html#syntax-heaptype}{\mathsf{func}}
}\end{split}\]
\[\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-heaptype}{\vdash} \href{../syntax/types.html#syntax-functype}{\mathit{functype}}_1 \href{../valid/matching.html#match-heaptype}{\leq} \href{../syntax/types.html#syntax-functype}{\mathit{functype}}_2
}\end{split}\]
\[\begin{split}~\\[-1ex]
\frac{
C \href{../valid/matching.html#match-heaptype}{\vdash} C.\href{../valid/conventions.html#context}{\mathsf{types}}[\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}_1] \href{../valid/matching.html#match-heaptype}{\leq} \href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}_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/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} C.\href{../valid/conventions.html#context}{\mathsf{types}}[\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}_2]
}{
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/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:
\[\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}\]
Instruction Types
Subtyping is further lifted to instruction types.
An instruction type \([t_{11}^\ast] \def\mathdef4324#1{\rightarrow_{#1}}\mathdef4324{x_1^\ast} [t_{12}^\ast]\) matches a type \([t_{21}^ast] \def\mathdef4325#1{\rightarrow_{#1}}\mathdef4325{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{../syntax/types.html#syntax-init}{\mathsf{set}}~t_x\) for some value type \(t_x\).
\[\begin{split}~\\[-1ex]
\frac{
\begin{array}{@{}c@{\qquad}l@{}}
C \href{../valid/matching.html#match-resulttype}{\vdash} [t_{21}^\ast] \href{../valid/matching.html#match-resulttype}{\leq} [t_{11}^\ast]
&
\{ x^\ast \} = \{ x_2^\ast \} \setminus \{ x_1^\ast \}
\\
C \href{../valid/matching.html#match-resulttype}{\vdash} [t_{12}^\ast] \href{../valid/matching.html#match-resulttype}{\leq} [t_{22}^\ast]
&
(C.\href{../valid/conventions.html#context}{\mathsf{locals}}[x] = \href{../syntax/types.html#syntax-init}{\mathsf{set}}~t_x)^\ast
\end{array}
}{
C \href{../valid/matching.html#match-instrtype}{\vdash} [t_{11}^\ast] \def\mathdef4326#1{\rightarrow_{#1}}\mathdef4326{x_1^\ast} [t_{12}^\ast] \href{../valid/matching.html#match-instrtype}{\leq} [t^\ast~t_{21}^\ast] \def\mathdef4327#1{\rightarrow_{#1}}\mathdef4327{x_2^\ast} [t^\ast~t_{22}^\ast]
}\end{split}\]
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
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:
\[\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:
\[\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:
\[\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\) 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\).
\[\begin{split}~\\[-1ex]
\frac{
C \href{../valid/matching.html#match-valtype}{\vdash} t_1 \href{../valid/matching.html#match-valtype}{\leq} t_2
\qquad
C \href{../valid/matching.html#match-valtype}{\vdash} t_2 \href{../valid/matching.html#match-valtype}{\leq} t_1
}{
C \href{../valid/matching.html#match-globaltype}{\vdash} \href{../syntax/types.html#syntax-mut}{\mathsf{var}}~t_1 \href{../valid/matching.html#match-globaltype}{\leq} \href{../syntax/types.html#syntax-mut}{\mathsf{var}}~t_2
}
\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:
\[\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:
\[\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:
\[\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:
\[\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}\]
