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¶

The number type \({\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}}\) matches only itself.

\[\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¶

The vector type \({\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}}\) matches only itself.

\[\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¶

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}''}\) matches the heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'''}\) if:

Either:

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}''}\) is of the form \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}}\).

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'''}\) is of the form \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}}\).

Or:

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}''}\) is of the form \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}}_1\).

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'''}\) is of the form \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}}_2\).

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'}\) is valid.

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}}_1\) matches the heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'}\).

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'}\) matches the heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}}_2\).

Or:

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}''}\) is of the form \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{eq}}\).

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'''}\) is of the form \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{any}}\).

Or:

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}''}\) is of the form \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{i\scriptstyle31}}\).

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'''}\) is of the form \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{eq}}\).

Or:

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}''}\) is of the form \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{struct}}\).

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'''}\) is of the form \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{eq}}\).

Or:

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}''}\) is of the form \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{array}}\).

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'''}\) is of the form \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{eq}}\).

Or:

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}''}\) is of the form \({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}\).

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'''}\) is of the form \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{struct}}\).

The expansion of the defined type \({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~{{\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}}^\ast})\).

Or:

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}''}\) is of the form \({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}\).

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'''}\) is of the form \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{array}}\).

The expansion of the defined type \({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~{\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}})\).

Or:

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}''}\) is of the form \({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}\).

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'''}\) is of the form \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{func}}\).

The expansion of the defined type \({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{\href{../syntax/types.html#syntax-functype}{\mathit{functype}}})\).

Or:

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}''}\) is of the form \({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_1\).

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'''}\) is of the form \({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_2\).

The defined type \({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_1\) matches the defined type \({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_2\).

Or:

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}''}\) is of the form \({\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}}\).

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'''}\) is of the form \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}}\).

The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[{\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}}]\) exists.

The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[{\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}}]\) matches the heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}}\).

Or:

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}''}\) is of the form \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}}\).

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'''}\) is of the form \({\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}}\).

The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[{\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}}]\) exists.

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}}\) matches the type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[{\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}}]\).

Or:

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}''}\) is of the form \((\href{../syntax/types.html#syntax-heaptype}{\mathsf{rec}}~i)\).

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'''}\) is of the form \({{\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}}^\ast}{}[j]\).

The length of \({{\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}}^\ast}\) is greater than \(j\).

The recursive type \(C{.}\href{../appendix/properties.html#context-ext}{\mathsf{recs}}{}[i]\) exists.

The recursive type \(C{.}\href{../appendix/properties.html#context-ext}{\mathsf{recs}}{}[i]\) is of the form \((\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}})\).

Or:

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}''}\) is of the form \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{none}}\).

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'''}\) is of the form \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}}\).

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}}\) matches the heap type \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{any}}\).

Or:

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}''}\) is of the form \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{nofunc}}\).

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'''}\) is of the form \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}}\).

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}}\) matches the heap type \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{func}}\).

Or:

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}''}\) is of the form \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{noexn}}\).

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'''}\) is of the form \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}}\).

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}}\) matches the heap type \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{exn}}\).

Or:

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}''}\) is of the form \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{noextern}}\).

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'''}\) is of the form \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}}\).

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}}\) matches the heap type \(\href{../syntax/types.html#syntax-heaptype}{\mathsf{extern}}\).

Or:

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}''}\) is of the form \(\href{../valid/conventions.html#syntax-valtype-ext}{\mathsf{bot}}\).

The heap type \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}'''}\) is of the form \({\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}}\).

\[\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}}} \mathrel{\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}}} \mathrel{\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}}} \mathrel{\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{exn}} }{ C \href{../valid/matching.html#match-heaptype}{\vdash} \href{../syntax/types.html#syntax-heaptype}{\mathsf{noexn}} \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¶

The reference type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}^?}~{\mathit{ht}}_1)\) matches the reference type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{{\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}^?}'}~{\mathit{ht}}_2)\) if:

The heap type \({\mathit{ht}}_1\) matches the heap type \({\mathit{ht}}_2\).

Either:

\({\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}^?}\) is absent.

\({{\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}^?}'}\) is absent.

Or:

\({\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}^?}\) is of the form \({\mathsf{null}^?}\).

\({{\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}^?}'}\) is of the form \(\mathsf{null}\).

\[\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}}~{\mathsf{null}^?}~{\mathit{ht}}_1 \href{../valid/matching.html#match-reftype}{\leq} \href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\mathsf{null}~{\mathit{ht}}_2 } \qquad \end{array}\]

Value Types¶

The value type \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}'}\) matches the value type \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}''}\) if:

Either:

The value type \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}'}\) is of the form \({\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}}_1\).

The value type \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}''}\) is of the form \({\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}}_2\).

The number type \({\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}}_1\) matches the number type \({\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}}_2\).

Or:

The value type \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}'}\) is of the form \({\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}}_1\).

The value type \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}''}\) is of the form \({\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}}_2\).

The vector type \({\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}}_1\) matches the vector type \({\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}}_2\).

Or:

The value type \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}'}\) is of the form \({\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}}_1\).

The value type \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}''}\) is of the form \({\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}}_2\).

The reference type \({\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}}_1\) matches the reference type \({\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}}_2\).

Or:

The value type \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}'}\) is of the form \(\href{../valid/conventions.html#syntax-valtype-ext}{\mathsf{bot}}\).

The value type \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}''}\) is of the form \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}\).

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

The result type \({t_1^\ast}\) matches the result type \({t_2^\ast}\) if:

The length of \({t_1^\ast}\) is equal to the length of \({t_2^\ast}\).

For all \(t_1\) in \({t_1^\ast}\), and corresponding \(t_2\) in \({t_2^\ast}\):

The value type \(t_1\) matches the value type \(t_2\).

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

The instruction type \({t_{11}^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x_1^\ast}}\,{t_{12}^\ast}\) matches the instruction type \({t_{21}^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x_2^\ast}}\,{t_{22}^\ast}\) if:

The result type \({t_{21}^\ast}\) matches the result type \({t_{11}^\ast}\).

The result type \({t_{12}^\ast}\) matches the result type \({t_{22}^\ast}\).

The local index sequence \({x^\ast}\) is of the form \({x_2^\ast} \setminus {x_1^\ast}\).

The length of \({t^\ast}\) is equal to the length of \({x^\ast}\).

For all \(x\) in \({x^\ast}\):

The local \(C{.}\href{../valid/conventions.html#context}{\mathsf{locals}}{}[x]\) exists.

For all \(t\) in \({t^\ast}\), and corresponding \(x\) in \({x^\ast}\):

The local \(C{.}\href{../valid/conventions.html#context}{\mathsf{locals}}{}[x]\) is of the form \((\href{../valid/conventions.html#syntax-init}{\mathsf{set}}~t)\).

\[\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. Moreover, 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¶

The function type \({t_{11}^\ast}~\href{../syntax/types.html#syntax-functype}{\rightarrow}~{t_{12}^\ast}\) matches the function type \({t_{21}^\ast}~\href{../syntax/types.html#syntax-functype}{\rightarrow}~{t_{22}^\ast}\) if:

The result type \({t_{21}^\ast}\) matches the result type \({t_{11}^\ast}\).

The result type \({t_{12}^\ast}\) matches the result type \({t_{22}^\ast}\).

\[\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¶

The composite type \({\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}}\) matches the composite type \({\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'}\) if:

Either:

The composite type \({\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}}\) is of the form \((\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~{{\mathit{yt}}_1^\ast}~{{\mathit{yt}'}_1^\ast})\).

The composite type \({\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'}\) is of the form \((\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~{{\mathit{yt}}_2^\ast})\).

The length of \({{\mathit{yt}}_1^\ast}\) is equal to the length of \({{\mathit{yt}}_2^\ast}\).

For all \({\mathit{yt}}_1\) in \({{\mathit{yt}}_1^\ast}\), and corresponding \({\mathit{yt}}_2\) in \({{\mathit{yt}}_2^\ast}\):

The field type \({\mathit{yt}}_1\) matches the field type \({\mathit{yt}}_2\).

Or:

The composite type \({\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}}\) is of the form \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~{\mathit{yt}}_1)\).

The composite type \({\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'}\) is of the form \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~{\mathit{yt}}_2)\).

The field type \({\mathit{yt}}_1\) matches the field type \({\mathit{yt}}_2\).

Or:

The composite type \({\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}}\) is of the form \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{\mathit{ft}}_1)\).

The composite type \({\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'}\) is of the form \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{\mathit{ft}}_2)\).

The function type \({\mathit{ft}}_1\) matches the function type \({\mathit{ft}}_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^\ast}) \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¶

The field type \(({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\mathit{zt}}_1)\) matches the field type \(({{\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}'}~{\mathit{zt}}_2)\) if:

The storage type \({\mathit{zt}}_1\) matches the storage type \({\mathit{zt}}_2\).

Either:

\({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}\) is absent.

\({{\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}'}\) is absent.

Or:

\({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}\) is of the form \(\mathsf{mut}\).

\({{\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}'}\) is of the form \(\mathsf{mut}\).

The storage type \({\mathit{zt}}_2\) matches the storage type \({\mathit{zt}}_1\).

\[\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} \mathsf{mut}~{\mathit{zt}}_1 \href{../valid/matching.html#match-fieldtype}{\leq} \mathsf{mut}~{\mathit{zt}}_2 } \qquad \end{array}\]

The storage type \({\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}}\) matches the storage type \({\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}'}\) if:

Either:

The storage type \({\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}}\) is of the form \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}_1\).

The storage type \({\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}'}\) is of the form \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}_2\).

The value type \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}_1\) matches the value type \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}_2\).

Or:

The storage type \({\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}}\) is of the form \({\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}_1\).

The storage type \({\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}'}\) is of the form \({\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}_2\).

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

The packed type \({\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}\) matches only itself.

\[\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¶

The defined type \({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_1\) matches the defined type \({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_2\) if:

Either:

The defined type \({{\href{../valid/conventions.html#aux-clostype}{\mathsf{clos}}}}_{C}({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_1)\) is of the form \({{\href{../valid/conventions.html#aux-clostype}{\mathsf{clos}}}}_{C}({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_2)\).

Or:

The sub type \({\href{../valid/conventions.html#aux-unroll-deftype}{\mathrm{unroll}}}({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_1)\) is of the form \((\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}})\).

The length of \({{\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}}^\ast}\) is greater than \(i\).

The type use \({{\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}}^\ast}{}[i]\) matches the heap type \({\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¶

The limits range \({}[ n_1 \href{../syntax/types.html#syntax-limits}{\,{..}\,} m_1 ]\) matches the limits range \({}[ n_2 \href{../syntax/types.html#syntax-limits}{\,{..}\,} m_2 ]\) if:

\(n_1\) is greater than or equal to \(n_2\).

\(m_1\) is less 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¶

The table type \(({\href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}}~{\href{../syntax/types.html#syntax-limits}{\mathit{limits}}}_1~{\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}}_1)\) matches the table type \(({\href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}}~{\href{../syntax/types.html#syntax-limits}{\mathit{limits}}}_2~{\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}}_2)\) if:

The limits range \({\href{../syntax/types.html#syntax-limits}{\mathit{limits}}}_1\) matches the limits range \({\href{../syntax/types.html#syntax-limits}{\mathit{limits}}}_2\).

The reference type \({\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}}_1\) matches the reference type \({\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}}_2\).

The reference type \({\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}}_2\) matches the reference type \({\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}}_1\).

\[\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-addrtype}{\mathit{addrtype}}}~{\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-addrtype}{\mathit{addrtype}}}~{\href{../syntax/types.html#syntax-limits}{\mathit{limits}}}_2~{\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}}_2 } \qquad \end{array}\]

Memory Types¶

The memory type \(({\href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}}~{\href{../syntax/types.html#syntax-limits}{\mathit{limits}}}_1~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\) matches the memory type \(({\href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}}~{\href{../syntax/types.html#syntax-limits}{\mathit{limits}}}_2~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}})\) if:

The limits range \({\href{../syntax/types.html#syntax-limits}{\mathit{limits}}}_1\) matches the limits range \({\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-addrtype}{\mathit{addrtype}}}~{\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-addrtype}{\mathit{addrtype}}}~{\href{../syntax/types.html#syntax-limits}{\mathit{limits}}}_2~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}} } \qquad \end{array}\]

Global Types¶

The global type \(({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}_1)\) matches the global type \(({{\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}'}~{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}_2)\) if:

The value type \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}_1\) matches the value type \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}_2\).

Either:

\({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}\) is absent.

\({{\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}'}\) is absent.

Or:

\({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}\) is of the form \(\mathsf{mut}\).

\({{\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}'}\) is of the form \(\mathsf{mut}\).

The value type \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}_2\) matches the value type \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}_1\).

\[\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} \mathsf{mut}~{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}_1 \href{../valid/matching.html#match-globaltype}{\leq} \mathsf{mut}~{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}_2 } \qquad \end{array}\]

Tag Types¶

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

The defined type \({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_1\) matches the defined type \({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_2\).

The defined type \({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_2\) matches the defined type \({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_1\).

\[\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}\]

Note

Although the conclusion of this rule looks identical to its premise, they in fact describe different relations: the premise invokes subtyping on defined types, while the conclusion defines it on tag types that happen to be expressed as defined types.

External Types¶

The external type \((\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_1)\) matches the external type \((\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_2)\) if:

The defined type \({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}_1\) matches the defined type \({\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}\]

The external type \((\href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~{\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}}_1)\) matches the external type \((\href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~{\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}}_2)\) if:

The table type \({\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}}_1\) matches the table type \({\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}\]

The external type \((\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~{\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}}_1)\) matches the external type \((\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~{\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}}_2)\) if:

The memory type \({\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}}_1\) matches the memory type \({\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}\]

The external type \((\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}_1)\) matches the external type \((\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}_2)\) if:

The global type \({\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}_1\) matches the global type \({\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}\]

The external type \((\href{../syntax/types.html#syntax-externtype}{\mathsf{tag}}~{\href{../valid/conventions.html#syntax-tagtype}{\mathit{tagtype}}}_1)\) matches the external type \((\href{../syntax/types.html#syntax-externtype}{\mathsf{tag}}~{\href{../valid/conventions.html#syntax-tagtype}{\mathit{tagtype}}}_2)\) if:

The tag type \({\href{../valid/conventions.html#syntax-tagtype}{\mathit{tagtype}}}_1\) matches the tag type \({\href{../valid/conventions.html#syntax-tagtype}{\mathit{tagtype}}}_2\).

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