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 plain function types for ease of processing.

Number Types

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

Todo

below is the official specification

Number types are 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 valid.

Todo

below is the official specification

Vector types are 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

Concrete heap types are only valid when the type index is, while abstract ones are vacuously valid.

\(\href{../syntax/types.html#syntax-absheaptype}{\mathit{absheaptype}}\)

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

Todo

below is the official specification

  • The heap type is 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}\]

\(\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}\)

The heap type \({\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 equal to \({\mathit{dt}}\).

Todo

below is the official specification

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

  • Then the heap type is valid.

\[\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-heaptype}{\vdash} {\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}} : \href{../valid/types.html#valid-heaptype}{\mathsf{ok}} } \qquad \end{array}\]

Reference Types

The reference type \((\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~(\href{../syntax/types.html#syntax-reftype}{\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.

Todo

below is the official specification

Reference types are valid when the referenced heap type is.

\(\href{../syntax/types.html#syntax-reftype}{\mathsf{ref}}~\href{../syntax/types.html#syntax-reftype}{\mathsf{null}}^?~\href{../syntax/types.html#syntax-heaptype}{\mathit{heaptype}}\)

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

  • Then the reference type 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}}~{\href{../syntax/types.html#syntax-reftype}{\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 \(t_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is valid if:

  • Either:

    • The value type \(t_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is equal to \({\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 \(t_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is equal to \({\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 \(t_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is equal to \({\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 \(t_{\mathit{u{\kern-0.1em\scriptstyle 1}}}\) is equal to \(\href{../valid/conventions.html#syntax-valtype-ext}{\mathsf{bot}}\).

Todo

below is the official specification

Valid value types are either valid number types, valid vector types, or valid reference types.

Block Types

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

\(\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}\)

The block type \({\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}}\) is valid with 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})\).

Todo

below is the official specification

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

  • The expansion of \(C.\href{../valid/conventions.html#context}{\mathsf{funcs}}[\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}]\) must be a function type \(\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~[t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\).

  • Then the block type is valid as instruction type \([t_1^\ast] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\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}\]

\([\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}^?]\)

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

Todo

below is the official specification

  • The value type \(\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}\) must either be absent, or valid.

  • Then the block type is valid as instruction type \([] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}^?]\).

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

\([t^\ast]\)

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

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

    • The value type \(t\) is valid.

Todo

below is the official specification

  • Each value type \(t_i\) in the type sequence \(t^\ast\) must be valid.

  • Then the result type 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 value type sequence \({t_1^\ast}\) is valid.

  • The value type sequence \({t_2^\ast}\) is valid.

  • \({|{\mathit{x*}}|}\) is equal to \({|{\mathit{lct*}}|}\).

  • 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 \(x\) in \({x^\ast}\):

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

Todo

below is the official specification

\([t_1^\ast] \rightarrow_{x^\ast} [t_2^\ast]\)

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

\([t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast]\)

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

  • The value type sequence \({t_1^\ast}\) is valid.

  • The value type sequence \({t_2^\ast}\) is valid.

Todo

below is the official specification

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

\(\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\)

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.

Todo

below is the official specification

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

  • Then the composite type 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}\]

\(\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}^\ast\)

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.

Todo

below is the official specification

  • For each field type \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}_i\) in \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}^\ast\):

    • The field type \(\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}_i\) must be valid.

  • Then the composite type 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}\]

\(\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}\)

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.

Todo

below is the official specification

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

  • Then the composite type 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

\(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}\)

The field type \(((\href{../syntax/types.html#syntax-mut}{\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.

Todo

below is the official specification

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

  • Then the field type 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} {\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}} : \href{../valid/types.html#valid-fieldtype}{\mathsf{ok}} } \qquad \end{array}\]

\(\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}\)

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

Todo

below is the official specification

  • The packed type is 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 for a specific type index that denotes the index of the type 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}}~{{\mathit{st}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast})\) is valid with \(({\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{x})\) if:

  • Either:

    • The sub type sequence \({{\mathit{st}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}\) is equal to \(\epsilon\).

  • Or:

    • The sub type sequence \({{\mathit{st}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}\) is equal to \({\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 with \(({\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{x + 1})\).

  • Or:

    • The sub type sequence \({{\mathit{st}}_{\mathit{u{\kern-0.1em\scriptstyle 1}}}^\ast}\) is equal to \({{\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}^\ast}\).

    • Let \({C'}\) be the same context as \(C\), but with the sub type sequence \({{\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}^\ast}\) prepended to the field \(\href{../appendix/properties.html#context-ext}{\mathsf{recs}}\).

    • Under the context \({C'}\), the recursive type \((\href{../syntax/types.html#syntax-rectype}{\mathsf{rec}}~{{\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}^\ast})\) is valid with \(({\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{(x, 0)})\).

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}}~(\href{../syntax/types.html#syntax-subtype}{\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:

  • \({|{x^\ast}|}\) is less than or equal to \(1\).

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

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

  • \({|{\mathit{x*}}|}\) is equal to \({|{\mathit{comptype'*}}|}\).

  • \({|{\mathit{x'**}}|}\) is equal to \({|{\mathit{comptype'*}}|}\).

  • 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 \(x\) in \({x^\ast}\) and \({\mathit{x'*}}\) in \({{\mathit{x'*}}^\ast}\):

    • The sub type \({\href{../valid/conventions.html#aux-unroll-deftype}{\mathrm{unroll}}}(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x])\) is equal to \((\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}}~{\href{../syntax/types.html#syntax-subtype}{\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

\(\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}.i\)

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 with \(({\href{../valid/types.html#valid-subtype}{\mathsf{ok}}}{x})\).

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

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

Todo

below is the official specification

  • The recursive type \(\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}\) must be valid for some type index \(x\).

  • Let \(\href{../syntax/types.html#syntax-rectype}{\mathsf{rec}}~\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}^\ast\) be the defined type \(\href{../syntax/types.html#syntax-rectype}{\mathit{rectype}}\).

  • The number \(i\) must be smaller than the length of the sequence \(\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}^\ast\) of sub types.

  • Then the defined type is valid.

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

\(\{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^? \}\)

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

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

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

Todo

below is the official specification

  • The value of \(n\) must not be larger than \(k\).

  • If the maximum \(m^?\) is not empty, then:

    • Its value must not be larger than \(k\).

    • Its value must not be smaller than \(n\).

  • Then the limit is valid within range \(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

\(\href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}\)

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 \({\href{../syntax/types.html#syntax-limits}{\mathit{limits}}}\) is valid with \({2^{32}} - 1\).

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

Todo

below is the official specification

  • The limits \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) must be valid within range \(2^{|\href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}|}-1\).

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

  • Then the table type 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

\(\href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\)

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 \({\href{../syntax/types.html#syntax-limits}{\mathit{limits}}}\) is valid with \({2^{16}}\).

Todo

below is the official specification

  • The limits \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) must be valid within range \(2^{|\href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}|-16}\).

  • Then the memory type is valid.

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

\([t_1^n] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t_2^m]\)

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

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

  • The expansion of the tag 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}}})\).

Todo

below is the official specification

  • The function type \([t_1^n] \mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}} [t_2^m]\) must be valid.

  • The type sequence \(t_2^m\) must be empty.

  • Then the tag type is valid.

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

Global Types

\(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}\)

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

  • The value type \(t\) is valid.

Todo

below is the official specification

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

  • Then the global type 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} {\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~t : \href{../valid/types.html#valid-globaltype}{\mathsf{ok}} } \qquad \end{array}\]

External Types

\(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}\)

The external type \((\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~{\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}}})\).

Todo

below is the official specification

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

  • The defined type \(\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}\) must be a function type.

  • Then the external type is valid.

\[\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-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~{\href{../valid/conventions.html#syntax-deftype}{\mathit{deftype}}} : \href{../valid/types.html#valid-externtype}{\mathsf{ok}} } \qquad \end{array}\]

\(\href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\)

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.

Todo

below is the official specification

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

  • Then the external type 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}\]

\(\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\)

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.

Todo

below is the official specification

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

  • Then the external type 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}\]

\(\href{../syntax/types.html#syntax-tagtype}{\mathsf{tag}}~\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}\)

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

  • The tag type \({\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}}\) is valid.

Todo

below is the official specification

  • The tag type \(\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}\) must be valid.

  • Then the external type is valid.

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

\(\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\)

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.

Todo

below is the official specification

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

  • Then the external type 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}\]

Defaultable Types

A type is defaultable if it has a default value for initialization.

Value Types

The value type \(t\) is defaultable if:

  • The value \({{\href{../exec/runtime.html#default-val}{\mathrm{default}}}}_{t}\) is not absent.

Todo

below is the official specification

\[\begin{array}{@{}c@{}}\displaystyle \frac{ {{\href{../exec/runtime.html#default-val}{\mathrm{default}}}}_{t} \neq \epsilon }{ {{\href{../exec/runtime.html#default-val}{\mathrm{default}}}}_{t} \neq \epsilon } \qquad \end{array}\]