Types¶

Simple types, such as number types are universally valid. However, restrictions apply to most other types, such as reference types, function types, as well as the limits of table types and memory types, which must be checked during validation.

Moreover, block types are converted to instruction types for ease of processing.

Number Types¶

The number type \({\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}}\) is always valid.

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

Vector Types¶

The vector type \({\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}}\) is always valid.

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

Heap Types¶

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

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/types.html#valid-heaptype}{\vdash} {\href{../syntax/types.html#syntax-absheaptype}{\mathit{absheaptype}}} : \href{../valid/types.html#valid-heaptype}{\mathsf{ok}} } \qquad \end{array}\]

The type use \({\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}}\) is valid if:

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

The defined type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[{\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}}]\) is of the form \({\mathit{dt}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[{\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}}] = {\mathit{dt}} }{ C \href{../valid/types.html#valid-typeuse}{\vdash} {\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}} : \href{../valid/types.html#valid-typeuse}{\mathsf{ok}} } \qquad \end{array}\]

Reference Types¶

The reference type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\mathsf{null}^?}~{\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}})\) is valid if:

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

\[\begin{array}{@{}c@{}}\displaystyle \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}} }{ C \href{../valid/types.html#valid-reftype}{\vdash} \href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~{\mathsf{null}^?}~{\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}} : \href{../valid/types.html#valid-reftype}{\mathsf{ok}} } \qquad \end{array}\]

Value Types¶

The value type \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}\) is valid 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}}}\).

The number type \({\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}}\) is valid.

Or:

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

The vector type \({\href{../syntax/types.html#syntax-vectype}{\mathit{vectype}}}\) is valid.

Or:

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

The reference type \({\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}}\) is valid.

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

Block Types¶

Block types may be expressed in one of two forms, both of which are converted to instruction types by the following rules.

The block type \({\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}}\) is valid as the instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\) if:

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

The expansion of the defined type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[{\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}}]\) is the composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast}~\href{../syntax/types.html#syntax-functype}{\rightarrow}~{t_2^\ast})\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[{\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}}] \href{../valid/conventions.html#aux-expand-deftype}{\approx} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~({t_1^\ast} \href{../syntax/types.html#syntax-functype}{\rightarrow} {t_2^\ast}) }{ C \href{../valid/types.html#valid-blocktype}{\vdash} {\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}} : {t_1^\ast} \rightarrow {t_2^\ast} } \qquad \end{array}\]

The block type \({{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}^?}\) is valid as the instruction type \(\epsilon~\rightarrow~{{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}^?}\) if:

If \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}\) is defined, then:

The value type \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}\) is valid.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ (C \href{../valid/types.html#valid-valtype}{\vdash} {\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}} : \href{../valid/types.html#valid-valtype}{\mathsf{ok}})^? }{ C \href{../valid/types.html#valid-blocktype}{\vdash} {{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}^?} : \epsilon \rightarrow {{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}^?} } \qquad \end{array}\]

Result Types¶

The result type \({t^\ast}\) is valid if:

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

The value type \(t\) is valid.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ (C \href{../valid/types.html#valid-valtype}{\vdash} t : \href{../valid/types.html#valid-valtype}{\mathsf{ok}})^\ast }{ C \href{../valid/types.html#valid-resulttype}{\vdash} {t^\ast} : \href{../valid/types.html#valid-resulttype}{\mathsf{ok}} } \qquad \end{array}\]

Instruction Types¶

The instruction type \({t_1^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x^\ast}}\,{t_2^\ast}\) is valid if:

The result type \({t_1^\ast}\) is valid.

The result type \({t_2^\ast}\) is valid.

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

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

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

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

The local type \(C{.}\href{../valid/conventions.html#context}{\mathsf{locals}}{}[x]\) is of the form \({{\mathit{lt}}}\).

Todo

below is the official specification

\(t_1^\ast \rightarrow_{x^\ast} t_2^\ast\)¶

The result type \(t_1^\ast\) must be valid.
The result type \(t_2^\ast\) must be valid.
Each local index \(x_i\) in \(x^\ast\) must be defined in the context.
Then the instruction type is valid.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-resulttype}{\vdash} {t_1^\ast} : \href{../valid/types.html#valid-resulttype}{\mathsf{ok}} \qquad C \href{../valid/types.html#valid-resulttype}{\vdash} {t_2^\ast} : \href{../valid/types.html#valid-resulttype}{\mathsf{ok}} \qquad (C{.}\href{../valid/conventions.html#context}{\mathsf{locals}}{}[x] = {{\mathit{lt}}})^\ast }{ C \href{../valid/types.html#valid-instrtype}{\vdash} {t_1^\ast} \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}_{{x^\ast}} {t_2^\ast} : \href{../valid/types.html#valid-instrtype}{\mathsf{ok}} } \qquad \end{array}\]

Function Types¶

The function type \({t_1^\ast}~\href{../syntax/types.html#syntax-functype}{\rightarrow}~{t_2^\ast}\) is valid if:

The result type \({t_1^\ast}\) is valid.

The result type \({t_2^\ast}\) is valid.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-resulttype}{\vdash} {t_1^\ast} : \href{../valid/types.html#valid-resulttype}{\mathsf{ok}} \qquad C \href{../valid/types.html#valid-resulttype}{\vdash} {t_2^\ast} : \href{../valid/types.html#valid-resulttype}{\mathsf{ok}} }{ C \href{../valid/types.html#valid-functype}{\vdash} {t_1^\ast} \href{../syntax/types.html#syntax-functype}{\rightarrow} {t_2^\ast} : \href{../valid/types.html#valid-functype}{\mathsf{ok}} } \qquad \end{array}\]

Composite Types¶

The composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{\href{../syntax/types.html#syntax-functype}{\mathit{functype}}})\) is valid if:

The function type \({\href{../syntax/types.html#syntax-functype}{\mathit{functype}}}\) is valid.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-functype}{\vdash} {\href{../syntax/types.html#syntax-functype}{\mathit{functype}}} : \href{../valid/types.html#valid-functype}{\mathsf{ok}} }{ C \href{../valid/types.html#valid-comptype}{\vdash} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{\href{../syntax/types.html#syntax-functype}{\mathit{functype}}} : \href{../valid/types.html#valid-comptype}{\mathsf{ok}} } \qquad \end{array}\]

The composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~{{\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}}^\ast})\) is valid if:

For all \({\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}}\) in \({{\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}}^\ast}\):

The field type \({\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}}\) is valid.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ (C \href{../valid/types.html#valid-fieldtype}{\vdash} {\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}} : \href{../valid/types.html#valid-fieldtype}{\mathsf{ok}})^\ast }{ C \href{../valid/types.html#valid-comptype}{\vdash} \href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~{{\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}}^\ast} : \href{../valid/types.html#valid-comptype}{\mathsf{ok}} } \qquad \end{array}\]

The composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~{\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}})\) is valid if:

The field type \({\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}}\) is valid.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-fieldtype}{\vdash} {\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}} : \href{../valid/types.html#valid-fieldtype}{\mathsf{ok}} }{ C \href{../valid/types.html#valid-comptype}{\vdash} \href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~{\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}} : \href{../valid/types.html#valid-comptype}{\mathsf{ok}} } \qquad \end{array}\]

Field Types¶

The field type \(({\mathsf{mut}^?}~{\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}})\) is valid if:

The storage type \({\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}}\) is valid.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-storagetype}{\vdash} {\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}} : \href{../valid/types.html#valid-storagetype}{\mathsf{ok}} }{ C \href{../valid/types.html#valid-fieldtype}{\vdash} {\mathsf{mut}^?}~{\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}} : \href{../valid/types.html#valid-fieldtype}{\mathsf{ok}} } \qquad \end{array}\]

The packed type \({\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}\) is always valid.

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

Recursive Types¶

Recursive types are validated with respect to the first type index defined by the recursive group.

\(\href{../syntax/types.html#syntax-rectype}{\mathsf{rec}}~\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}^\ast\)¶

The recursive type \((\href{../syntax/types.html#syntax-rectype}{\mathsf{rec}}~{{\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}'}^\ast})\) is valid for \(({\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{(x)})\) if:

Either:

The sub type sequence \({{\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}'}^\ast}\) is empty.

Or:

The sub type sequence \({{\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}'}^\ast}\) is of the form \({\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}_1~{{\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}^\ast}\).

The sub type \({\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}_1\) is valid with \(({\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{(x)})\).

The recursive type \((\href{../syntax/types.html#syntax-rectype}{\mathsf{rec}}~{{\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}^\ast})\) is valid for \(({\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{(x + 1)})\).

Todo

below is the official specification

Either the sequence \(\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}^\ast\) is empty.
Or:
- The first sub type of the sequence \(\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}^\ast\) must be valid for the type index \(x\).
- The remaining sequence \(\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}^\ast\) must be valid for the type index \(x + 1\).
Then the recursive type is valid for the type index \(x\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ }{ C \href{../valid/types.html#valid-rectype}{\vdash} \href{../syntax/types.html#syntax-rectype}{\mathsf{rec}}~\epsilon : {\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{((x))} } \qquad \frac{ C \href{../valid/types.html#valid-subtype}{\vdash} {\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}_1 : {\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{((x))} \qquad C \href{../valid/types.html#valid-rectype}{\vdash} \href{../syntax/types.html#syntax-rectype}{\mathsf{rec}}~{{\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}^\ast} : {\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{((x + 1))} }{ C \href{../valid/types.html#valid-rectype}{\vdash} \href{../syntax/types.html#syntax-rectype}{\mathsf{rec}}~({\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}_1~{{\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}^\ast}) : {\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{((x))} } \qquad \end{array}\]

\(\href{../syntax/types.html#syntax-subtype}{\mathsf{sub}}~\href{../syntax/types.html#syntax-subtype}{\mathsf{final}}^?~y^\ast~\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}\)¶

The sub type \((\href{../syntax/types.html#syntax-subtype}{\mathsf{sub}}~{\mathsf{final}^?}~{x^\ast}~{\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}})\) is valid with \(({\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{(x_0)})\) if:

The length of \({x^\ast}\) is less than or equal to \(1\).

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

The index \(x\) is less than \(x_0\).

The length of \({{\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'}^\ast}\) is equal to the length of \({x^\ast}\).

The length of \({{\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'}^\ast}\) is equal to the length of \({{{x'}^\ast}^\ast}\).

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

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

For all \({\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'}\) in \({{\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'}^\ast}\), and corresponding \(x\) in \({x^\ast}\), and corresponding \({{x'}^\ast}\) in \({{{x'}^\ast}^\ast}\):

The sub type \({\href{../valid/conventions.html#aux-unroll-deftype}{\mathrm{unroll}}}(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x])\) is of the form \((\href{../syntax/types.html#syntax-subtype}{\mathsf{sub}}~{{x'}^\ast}~{\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'})\).

The composite type \({\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}}\) is valid.

For all \({\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'}\) in \({{\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'}^\ast}\):

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

Todo

below is the official specification

The composite type \(\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}\) must be valid.
The sequence \(y^\ast\) may be no longer than \(1\).
For every type index \(y_i\) in \(y^\ast\):
- The type index \(y_i\) must be smaller than \(x\).
- The type index \(y_i\) must exist in the context \(C\).
- Let \(\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}_i\) be the unrolling of the defined type \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[y_i]\).
- The sub type \(\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}_i\) must not contain \(\href{../syntax/types.html#syntax-subtype}{\mathsf{final}}\).
- Let \(\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'_i\) be the composite type in \(\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}_i\).
- The composite type \(\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}\) must match \(\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'_i\).
Then the sub type is valid for the type index \(x\).

\[\begin{split}\begin{array}{@{}c@{}}\displaystyle \frac{ \begin{array}{@{}c@{}} {|{x^\ast}|} \leq 1 \qquad (x < x_0)^\ast \qquad ({\href{../valid/conventions.html#aux-unroll-deftype}{\mathrm{unroll}}}(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]) = \href{../syntax/types.html#syntax-subtype}{\mathsf{sub}}~{{x'}^\ast}~{\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'})^\ast \\ C \href{../valid/types.html#valid-comptype}{\vdash} {\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}} : \href{../valid/types.html#valid-comptype}{\mathsf{ok}} \qquad (C \href{../valid/matching.html#match-comptype}{\vdash} {\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}} \href{../valid/matching.html#match-comptype}{\leq} {\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'})^\ast \end{array} }{ C \href{../valid/types.html#valid-subtype}{\vdash} \href{../syntax/types.html#syntax-subtype}{\mathsf{sub}}~{\mathsf{final}^?}~{x^\ast}~{\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}} : {\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{((x_0))} } \qquad \end{array}\end{split}\]

Note

The side condition on the index ensures that a declared supertype is a previously defined types, preventing cyclic subtype hierarchies.

Future versions of WebAssembly may allow more than one supertype.

Defined Types¶

The defined type \(({\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}} {.} i)\) is valid if:

The recursive type \({\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}}\) is valid for \(({\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{(x)})\).

The recursive type \({\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}}\) is of the form \((\href{../syntax/types.html#syntax-rectype}{\mathsf{rec}}~{{\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}^{n}})\).

\(i\) is less than \(n\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-rectype}{\vdash} {\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}} : {\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{((x))} \qquad {\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}} = \href{../syntax/types.html#syntax-rectype}{\mathsf{rec}}~{{\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}^{n}} \qquad i < n }{ C \href{../valid/types.html#valid-deftype}{\vdash} {\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}} {.} i : \href{../valid/types.html#valid-deftype}{\mathsf{ok}} } \qquad \end{array}\]

Limits¶

Limits must have meaningful bounds that are within a given range.

The limits range \({}[ n \href{../syntax/types.html#syntax-limits}{\,{..}\,} m ]\) is valid within \(k\) if:

\(n\) is less than or equal to \(m\).

\(m\) is less than or equal to \(k\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ n \leq m \leq k }{ C \href{../valid/types.html#valid-limits}{\vdash} {}[ n \href{../syntax/types.html#syntax-limits}{\,{..}\,} m ] : k } \qquad \end{array}\]

Table Types¶

The table type \(({\href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}}~{\href{../syntax/types.html#syntax-limits}{\mathit{limits}}}~{\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}})\) is valid if:

The limits range \({\href{../syntax/types.html#syntax-limits}{\mathit{limits}}}\) is valid within \({2^{32}} - 1\).

The reference type \({\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}}\) is valid.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-limits}{\vdash} {\href{../syntax/types.html#syntax-limits}{\mathit{limits}}} : {2^{32}} - 1 \qquad C \href{../valid/types.html#valid-reftype}{\vdash} {\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}} : \href{../valid/types.html#valid-reftype}{\mathsf{ok}} }{ C \href{../valid/types.html#valid-tabletype}{\vdash} {\href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}}~{\href{../syntax/types.html#syntax-limits}{\mathit{limits}}}~{\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}} : \href{../valid/types.html#valid-tabletype}{\mathsf{ok}} } \qquad \end{array}\]

Memory Types¶

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

The limits range \({\href{../syntax/types.html#syntax-limits}{\mathit{limits}}}\) is valid within \({2^{16}}\).

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-limits}{\vdash} {\href{../syntax/types.html#syntax-limits}{\mathit{limits}}} : {2^{16}} }{ C \href{../valid/types.html#valid-memtype}{\vdash} {\href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}}~{\href{../syntax/types.html#syntax-limits}{\mathit{limits}}}~\href{../syntax/types.html#syntax-memtype}{\mathsf{page}} : \href{../valid/types.html#valid-memtype}{\mathsf{ok}} } \qquad \end{array}\]

Tag Types¶

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

The defined type \({\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}}\) is valid.

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

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-deftype}{\vdash} {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}} : \href{../valid/types.html#valid-deftype}{\mathsf{ok}} \qquad {\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/types.html#valid-tagtype}{\vdash} {\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}} : \href{../valid/types.html#valid-tagtype}{\mathsf{ok}} } \qquad \end{array}\]

Note

Tag types do not occur in source programs, so this rule is not needed for validation. It is, however, used in the definition of the embedding interface.

Global Types¶

The global type \(({\mathsf{mut}^?}~t)\) is valid if:

The value type \(t\) is valid.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-valtype}{\vdash} t : \href{../valid/types.html#valid-valtype}{\mathsf{ok}} }{ C \href{../valid/types.html#valid-globaltype}{\vdash} {\mathsf{mut}^?}~t : \href{../valid/types.html#valid-globaltype}{\mathsf{ok}} } \qquad \end{array}\]

External Types¶

The external type \((\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~{\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}})\) is valid if:

The type use \({\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}}\) is valid.

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

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-typeuse}{\vdash} {\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}} : \href{../valid/types.html#valid-typeuse}{\mathsf{ok}} \qquad {\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}} \href{../valid/conventions.html#aux-expand-typeuse}{\approx}_{C} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{\href{../syntax/types.html#syntax-functype}{\mathit{functype}}} }{ C \href{../valid/types.html#valid-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~{\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}} : \href{../valid/types.html#valid-externtype}{\mathsf{ok}} } \qquad \end{array}\]

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

The table type \({\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}}\) is valid.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-tabletype}{\vdash} {\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}} : \href{../valid/types.html#valid-tabletype}{\mathsf{ok}} }{ C \href{../valid/types.html#valid-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~{\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}} : \href{../valid/types.html#valid-externtype}{\mathsf{ok}} } \qquad \end{array}\]

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

The memory type \({\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}}\) is valid.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-memtype}{\vdash} {\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}} : \href{../valid/types.html#valid-memtype}{\mathsf{ok}} }{ C \href{../valid/types.html#valid-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~{\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}} : \href{../valid/types.html#valid-externtype}{\mathsf{ok}} } \qquad \end{array}\]

The external type \((\href{../syntax/types.html#syntax-externtype}{\mathsf{tag}}~{\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}})\) is valid if:

The type use \({\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}}\) is valid.

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

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-typeuse}{\vdash} {\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}} : \href{../valid/types.html#valid-typeuse}{\mathsf{ok}} \qquad {\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}} \href{../valid/conventions.html#aux-expand-typeuse}{\approx}_{C} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{\href{../syntax/types.html#syntax-functype}{\mathit{functype}}} }{ C \href{../valid/types.html#valid-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{tag}}~{\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}} : \href{../valid/types.html#valid-externtype}{\mathsf{ok}} } \qquad \end{array}\]

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

The global type \({\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}}\) is valid.

\[\begin{array}{@{}c@{}}\displaystyle \frac{ C \href{../valid/types.html#valid-globaltype}{\vdash} {\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}} : \href{../valid/types.html#valid-globaltype}{\mathsf{ok}} }{ C \href{../valid/types.html#valid-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}} : \href{../valid/types.html#valid-externtype}{\mathsf{ok}} } \qquad \end{array}\]