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.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/matching.html#match-numtype}{\vdash} {\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}} \href{../valid/matching.html#match-numtype}{\leq} {\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}} } \qquad \end{array}\]

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.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/matching.html#match-vectype}{\vdash} {\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}} \href{../valid/matching.html#match-vectype}{\leq} {\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}} } \qquad \end{array}\]

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{i\scriptstyle31}}\), \(\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/modules.html#syntax-func}{\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/modules.html#syntax-func}{\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}}\).

\[\begin{split}\begin{array}{@{}c@{}}\displaystyle \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/types.html#valid-heaptype}{\vdash} {\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'} : \href{../valid/types.html#valid-heaptype}{\mathsf{ok}} \qquad 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}}'} \qquad 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}}}_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/types.html#syntax-heaptype}{\mathit{heaptype}}}_2 } \\[3ex]\displaystyle \frac{ }{ C \href{../valid/matching.html#match-heaptype}{\vdash} \href{../syntax/types.html#syntax-heaptype}{\mathsf{eq}} \href{../valid/matching.html#match-heaptype}{\leq} \href{../syntax/types.html#syntax-heaptype}{\mathsf{any}} } \qquad \frac{ }{ C \href{../valid/matching.html#match-heaptype}{\vdash} \href{../syntax/types.html#syntax-heaptype}{\mathsf{i\scriptstyle31}} \href{../valid/matching.html#match-heaptype}{\leq} \href{../syntax/types.html#syntax-heaptype}{\mathsf{eq}} } \qquad \frac{ }{ C \href{../valid/matching.html#match-heaptype}{\vdash} \href{../syntax/types.html#syntax-heaptype}{\mathsf{struct}} \href{../valid/matching.html#match-heaptype}{\leq} \href{../syntax/types.html#syntax-heaptype}{\mathsf{eq}} } \qquad \frac{ }{ C \href{../valid/matching.html#match-heaptype}{\vdash} \href{../syntax/types.html#syntax-heaptype}{\mathsf{array}} \href{../valid/matching.html#match-heaptype}{\leq} \href{../syntax/types.html#syntax-heaptype}{\mathsf{eq}} } \\[3ex]\displaystyle \frac{ {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}} \href{../valid/conventions.html#aux-expand-deftype}{\approx} \href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~{{\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}}^\ast} }{ C \href{../valid/matching.html#match-heaptype}{\vdash} {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}} \href{../valid/matching.html#match-heaptype}{\leq} \href{../syntax/types.html#syntax-heaptype}{\mathsf{struct}} } \qquad \frac{ {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}} \href{../valid/conventions.html#aux-expand-deftype}{\approx} \href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~{\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}} }{ C \href{../valid/matching.html#match-heaptype}{\vdash} {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}} \href{../valid/matching.html#match-heaptype}{\leq} \href{../syntax/types.html#syntax-heaptype}{\mathsf{array}} } \qquad \frac{ {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}} \href{../valid/conventions.html#aux-expand-deftype}{\approx} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{\href{../syntax/types.html#syntax-functype}{\mathit{functype}}} }{ C \href{../valid/matching.html#match-heaptype}{\vdash} {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}} \href{../valid/matching.html#match-heaptype}{\leq} \href{../syntax/types.html#syntax-heaptype}{\mathsf{func}} } \\[3ex]\displaystyle \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}}}] \href{../valid/matching.html#match-heaptype}{\leq} {\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}} }{ 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}{\mathit{heaptype}}} } \qquad \frac{ C \href{../valid/matching.html#match-heaptype}{\vdash} {\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}} \href{../valid/matching.html#match-heaptype}{\leq} C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[{\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}}] }{ 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/modules.html#syntax-typeidx}{\mathit{typeidx}}} } \\[3ex]\displaystyle \frac{ C{.}\href{../appendix/properties.html#context-ext}{\mathsf{recs}}{}[i] = \href{../syntax/types.html#syntax-subtype}{\mathsf{sub}}~{\href{../syntax/types.html#syntax-subtype}{\mathsf{final}}^?}~{{\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}}^\ast}~{\mathit{ct}} }{ C \href{../valid/matching.html#match-heaptype}{\vdash} \href{../syntax/types.html#syntax-heaptype}{\mathsf{rec}}~i \href{../valid/matching.html#match-heaptype}{\leq} {{\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}}^\ast}{}[j] } \\[3ex]\displaystyle \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}{\mathsf{any}} }{ C \href{../valid/matching.html#match-heaptype}{\vdash} \href{../syntax/types.html#syntax-heaptype}{\mathsf{none}} \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-heaptype}{\mathit{heaptype}}} \href{../valid/matching.html#match-heaptype}{\leq} \href{../syntax/types.html#syntax-heaptype}{\mathsf{func}} }{ C \href{../valid/matching.html#match-heaptype}{\vdash} \href{../syntax/types.html#syntax-heaptype}{\mathsf{nofunc}} \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-heaptype}{\mathit{heaptype}}} \href{../valid/matching.html#match-heaptype}{\leq} \href{../syntax/types.html#syntax-heaptype}{\mathsf{extern}} }{ C \href{../valid/matching.html#match-heaptype}{\vdash} \href{../syntax/types.html#syntax-heaptype}{\mathsf{noextern}} \href{../valid/matching.html#match-heaptype}{\leq} {\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}} } \\[3ex]\displaystyle \frac{ }{ C \href{../valid/matching.html#match-heaptype}{\vdash} \href{../valid/conventions.html#syntax-valtype-ext}{\mathsf{bot}} \href{../valid/matching.html#match-heaptype}{\leq} {\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}} } \qquad \end{array}\end{split}\]

Reference Types

A reference type \(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}}{{{}_{1}^?}}~{\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}}_1\) matches a reference type \(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}}{{{}_{2}^?}}~{\href{../syntax/types.html#syntax-heaptype}{\mathit{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{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/matching.html#match-heaptype}{\vdash} {\mathit{ht}}_1 \href{../valid/matching.html#match-heaptype}{\leq} {\mathit{ht}}_2 }{ C \href{../valid/matching.html#match-reftype}{\vdash} \href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\mathit{ht}}_1 \href{../valid/matching.html#match-reftype}{\leq} \href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\mathit{ht}}_2 } \qquad \frac{ C \href{../valid/matching.html#match-heaptype}{\vdash} {\mathit{ht}}_1 \href{../valid/matching.html#match-heaptype}{\leq} {\mathit{ht}}_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}}^?}~{\mathit{ht}}_1 \href{../valid/matching.html#match-reftype}{\leq} \href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}~{\mathit{ht}}_2 } \qquad \end{array}\]

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

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/matching.html#match-valtype}{\vdash} \href{../valid/conventions.html#syntax-valtype-ext}{\mathsf{bot}} \href{../valid/matching.html#match-valtype}{\leq} {\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}} } \qquad \end{array}\]

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{array}{@{}c@{}}\displaystyle \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} } \qquad \end{array}\]

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

\[\begin{array}{@{}c@{}}\displaystyle \frac{ 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_{12}^\ast} \href{../valid/matching.html#match-resulttype}{\leq} {t_{22}^\ast} \qquad {x^\ast} = {x_2^\ast} \setminus {x_1^\ast} \qquad (C{.}\href{../valid/conventions.html#context}{\mathsf{locals}}{}[x] = \href{../valid/conventions.html#syntax-init}{\mathsf{set}}~t)^\ast }{ C \href{../valid/matching.html#match-instrtype}{\vdash} {t_{11}^\ast} \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{{x_1^\ast}} {t_{12}^\ast} \href{../valid/matching.html#match-instrtype}{\leq} {t_{21}^\ast} \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{{x_2^\ast}} {t_{22}^\ast} } \qquad \end{array}\]

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:

\[\begin{array}{@{}c@{}}\displaystyle \frac{ 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_{12}^\ast} \href{../valid/matching.html#match-resulttype}{\leq} {t_{22}^\ast} }{ 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} } \qquad \end{array}\]

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

\[\begin{array}{@{}c@{}}\displaystyle \frac{ (C \href{../valid/matching.html#match-fieldtype}{\vdash} {\mathit{yt}}_1 \href{../valid/matching.html#match-fieldtype}{\leq} {\mathit{yt}}_2)^\ast }{ C \href{../valid/matching.html#match-comptype}{\vdash} \href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~({{\mathit{yt}}_1^\ast}~{\mathit{yt}'}_1) \href{../valid/matching.html#match-comptype}{\leq} \href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~{{\mathit{yt}}_2^\ast} } \qquad \frac{ C \href{../valid/matching.html#match-fieldtype}{\vdash} {\mathit{yt}}_1 \href{../valid/matching.html#match-fieldtype}{\leq} {\mathit{yt}}_2 }{ C \href{../valid/matching.html#match-comptype}{\vdash} \href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~{\mathit{yt}}_1 \href{../valid/matching.html#match-comptype}{\leq} \href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~{\mathit{yt}}_2 } \qquad \frac{ C \href{../valid/matching.html#match-functype}{\vdash} {\mathit{ft}}_1 \href{../valid/matching.html#match-functype}{\leq} {\mathit{ft}}_2 }{ C \href{../valid/matching.html#match-comptype}{\vdash} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{\mathit{ft}}_1 \href{../valid/matching.html#match-comptype}{\leq} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{\mathit{ft}}_2 } \qquad \end{array}\]

Field Types

A field type \(({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}}{{{}_{1}^?}}~{\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}}_1)\) matches a type \(({\href{../syntax/types.html#syntax-mut}{\mathsf{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.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/matching.html#match-storagetype}{\vdash} {\mathit{zt}}_1 \href{../valid/matching.html#match-storagetype}{\leq} {\mathit{zt}}_2 }{ C \href{../valid/matching.html#match-fieldtype}{\vdash} {\mathit{zt}}_1 \href{../valid/matching.html#match-fieldtype}{\leq} {\mathit{zt}}_2 } \qquad \frac{ C \href{../valid/matching.html#match-storagetype}{\vdash} {\mathit{zt}}_1 \href{../valid/matching.html#match-storagetype}{\leq} {\mathit{zt}}_2 \qquad C \href{../valid/matching.html#match-storagetype}{\vdash} {\mathit{zt}}_2 \href{../valid/matching.html#match-storagetype}{\leq} {\mathit{zt}}_1 }{ C \href{../valid/matching.html#match-fieldtype}{\vdash} \href{../syntax/types.html#syntax-mut}{\mathsf{mut}}~{\mathit{zt}}_1 \href{../valid/matching.html#match-fieldtype}{\leq} \href{../syntax/types.html#syntax-mut}{\mathsf{mut}}~{\mathit{zt}}_2 } \qquad \end{array}\]

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-packtype}{\mathit{packtype}}_1\) and \(\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}_2\) is a packed type \(\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}_2\) and \(\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}_1\) matches \(\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}_2\).

A packed type \({\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}_1\) matches a type \({\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}_2\) if and only if:

  • The packed type \(\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}_1\) is the same as \(\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}_2\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/matching.html#match-packtype}{\vdash} {\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}} \href{../valid/matching.html#match-packtype}{\leq} {\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}} } \qquad \end{array}\]

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

\[\begin{split}\begin{array}{@{}c@{}}\displaystyle \frac{ {{\href{../valid/conventions.html#aux-clostype}{\mathsf{clos}}}}_{C}({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_1) = {{\href{../valid/conventions.html#aux-clostype}{\mathsf{clos}}}}_{C}({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_2) }{ C \href{../valid/matching.html#match-deftype}{\vdash} {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_1 \href{../valid/matching.html#match-deftype}{\leq} {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_2 } \\[3ex]\displaystyle \frac{ {\href{../valid/conventions.html#aux-unroll-deftype}{\mathrm{unroll}}}({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_1) = \href{../syntax/types.html#syntax-subtype}{\mathsf{sub}}~{\href{../syntax/types.html#syntax-subtype}{\mathsf{final}}^?}~{{\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}}^\ast}~{\mathit{ct}} \qquad C \href{../valid/matching.html#match-heaptype}{\vdash} {{\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}}^\ast}{}[i] \href{../valid/matching.html#match-heaptype}{\leq} {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_2 }{ C \href{../valid/matching.html#match-deftype}{\vdash} {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_1 \href{../valid/matching.html#match-deftype}{\leq} {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_2 } \qquad \end{array}\end{split}\]

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 \({}[ n_1 \href{../syntax/types.html#syntax-limits}{\,{..}\,} m_1 ]\) match limits \({}[ n_2 \href{../syntax/types.html#syntax-limits}{\,{..}\,} 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{array}{@{}c@{}}\displaystyle \frac{ n_1 \geq n_2 \qquad m_1 \leq m_2 }{ C \href{../valid/matching.html#match-limits}{\vdash} {}[ n_1 \href{../syntax/types.html#syntax-limits}{\,{..}\,} m_1 ] \href{../valid/matching.html#match-limits}{\leq} {}[ n_2 \href{../syntax/types.html#syntax-limits}{\,{..}\,} m_2 ] } \qquad \end{array}\]

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}}}_1~{\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}}_1)\) 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{array}{@{}c@{}}\displaystyle \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 } \qquad \end{array}\]

Memory Types

A memory type \(({\href{../syntax/types.html#syntax-limits}{\mathit{limits}}}_1~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\) matches \(({\href{../syntax/types.html#syntax-limits}{\mathit{limits}}}_2~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\) 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{array}{@{}c@{}}\displaystyle \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{../syntax/types.html#syntax-memtype}{\mathsf{page}} \href{../valid/matching.html#match-memtype}{\leq} {\href{../syntax/types.html#syntax-limits}{\mathit{limits}}}_2~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}} } \qquad \end{array}\]

Global Types

A global type \(({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}}{{{}_{1}^?}}~{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}_1)\) matches \(({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}}{{{}_{2}^?}}~{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}_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{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/matching.html#match-valtype}{\vdash} {\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}_1 \href{../valid/matching.html#match-valtype}{\leq} {\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}_2 }{ C \href{../valid/matching.html#match-globaltype}{\vdash} {\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}_1 \href{../valid/matching.html#match-globaltype}{\leq} {\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}_2 } \qquad \frac{ C \href{../valid/matching.html#match-valtype}{\vdash} {\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}_1 \href{../valid/matching.html#match-valtype}{\leq} {\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}_2 \qquad C \href{../valid/matching.html#match-valtype}{\vdash} {\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}_2 \href{../valid/matching.html#match-valtype}{\leq} {\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}_1 }{ C \href{../valid/matching.html#match-globaltype}{\vdash} \href{../syntax/types.html#syntax-mut}{\mathsf{mut}}~{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}_1 \href{../valid/matching.html#match-globaltype}{\leq} \href{../syntax/types.html#syntax-mut}{\mathsf{mut}}~{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}_2 } \qquad \end{array}\]

Tag Types

A tag type \({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_1\) matches \({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_2\) if and only if:

  • Defined type \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}_1\) matches \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}_2\) and vice versa.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/matching.html#match-deftype}{\vdash} {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_1 \href{../valid/matching.html#match-deftype}{\leq} {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_2 \qquad C \href{../valid/matching.html#match-deftype}{\vdash} {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_2 \href{../valid/matching.html#match-deftype}{\leq} {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_1 }{ C \href{../valid/matching.html#match-tagtype}{\vdash} {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_1 \href{../valid/matching.html#match-tagtype}{\leq} {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_2 } \qquad \end{array}\]

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

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/matching.html#match-deftype}{\vdash} {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_1 \href{../valid/matching.html#match-deftype}{\leq} {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_2 }{ C \href{../valid/matching.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_1 \href{../valid/matching.html#match-externtype}{\leq} \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_2 } \qquad \end{array}\]

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{array}{@{}c@{}}\displaystyle \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 } \qquad \end{array}\]

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{array}{@{}c@{}}\displaystyle \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 } \qquad \end{array}\]

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{array}{@{}c@{}}\displaystyle \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 } \qquad \end{array}\]

Tags

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

  • Tag type \(\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}_1\) matches \(\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}_2\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/matching.html#match-tagtype}{\vdash} {\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}}_1 \href{../valid/matching.html#match-tagtype}{\leq} {\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}}_2 }{ C \href{../valid/matching.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-tagtype}{\mathsf{tag}}~{\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}}_1 \href{../valid/matching.html#match-externtype}{\leq} \href{../syntax/types.html#syntax-tagtype}{\mathsf{tag}}~{\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}}_2 } \qquad \end{array}\]