Types#

Most types are universally valid. However, restrictions apply to limits, which must be checked during validation. Moreover, block types are converted to plain function types for ease of processing.

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

\[\frac{ n \leq k \qquad (m \leq k)^? \qquad (n \leq m)^? }{ \href{../valid/types.html#valid-limits}{\vdash} \{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^? \} : k }\]

Block Types#

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

\(\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}}]\) must be defined in the context.
Then the block type is valid as function type \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}]\).

\[\frac{ C.\href{../valid/conventions.html#context}{\mathsf{types}}[\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}] = \href{../syntax/types.html#syntax-functype}{\mathit{functype}} }{ C \href{../valid/types.html#valid-blocktype}{\vdash} \href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}} : \href{../syntax/types.html#syntax-functype}{\mathit{functype}} }\]

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

The block type is valid as function type \([] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}^?]\).

\[\frac{ }{ C \href{../valid/types.html#valid-blocktype}{\vdash} [\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}^?] : [] \href{../syntax/types.html#syntax-functype}{\rightarrow} [\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}^?] }\]

Function Types#

Function types are always valid.

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

The function type is valid.

\[\frac{ }{ \href{../valid/types.html#valid-functype}{\vdash} [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] \mathrel{\mbox{ok}} }\]

Table Types#

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

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

\[\frac{ \href{../valid/types.html#valid-limits}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}} : 2^{32} - 1 }{ \href{../valid/types.html#valid-tabletype}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}~\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}} \mathrel{\mbox{ok}} }\]

Memory Types#

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

The limits \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) must be valid within range \(2^{16}\).
Then the memory type is valid.

\[\frac{ \href{../valid/types.html#valid-limits}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}} : 2^{16} }{ \href{../valid/types.html#valid-memtype}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}} \mathrel{\mbox{ok}} }\]

Global Types#

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

The global type is valid.

\[\frac{ }{ \href{../valid/types.html#valid-globaltype}{\vdash} \href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}} \mathrel{\mbox{ok}} }\]

External Types#

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

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

\[\frac{ \href{../valid/types.html#valid-functype}{\vdash} \href{../syntax/types.html#syntax-functype}{\mathit{functype}} \mathrel{\mbox{ok}} }{ \href{../valid/types.html#valid-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}} \mathrel{\mbox{ok}} }\]

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

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

\[\frac{ \href{../valid/types.html#valid-tabletype}{\vdash} \href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}} \mathrel{\mbox{ok}} }{ \href{../valid/types.html#valid-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}} \mathrel{\mbox{ok}} }\]

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

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

\[\frac{ \href{../valid/types.html#valid-memtype}{\vdash} \href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} \mathrel{\mbox{ok}} }{ \href{../valid/types.html#valid-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}} \mathrel{\mbox{ok}} }\]

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

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

\[\frac{ \href{../valid/types.html#valid-globaltype}{\vdash} \href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}} \mathrel{\mbox{ok}} }{ \href{../valid/types.html#valid-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}} \mathrel{\mbox{ok}} }\]

Import Subtyping#

When instantiating a module, external values must be provided whose types are matched against the respective external types classifying each import. In some cases, this allows for a simple form of subtyping (written “\(\href{../exec/modules.html#match-externtype}{\leq}\)” formally), as defined here.

Limits#

Limits \(\{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_1, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m_1^? \}\) match limits \(\{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_2, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m_2^? \}\) if and only if:

\(n_1\) is larger than or equal to \(n_2\).
Either:
- \(m_2^?\) is empty.
Or:
- Both \(m_1^?\) and \(m_2^?\) are non-empty.
- \(m_1\) is smaller than or equal to \(m_2\).

\[\begin{split}~\\[-1ex] \frac{ n_1 \geq n_2 }{ \href{../exec/modules.html#match-limits}{\vdash} \{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_1, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m_1^? \} \href{../exec/modules.html#match-limits}{\leq} \{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_2, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~\epsilon \} } \quad \frac{ n_1 \geq n_2 \qquad m_1 \leq m_2 }{ \href{../exec/modules.html#match-limits}{\vdash} \{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_1, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m_1 \} \href{../exec/modules.html#match-limits}{\leq} \{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_2, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m_2 \} }\end{split}\]

Functions#

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

Both \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_1\) and \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_2\) are the same.

\[\begin{split}~\\[-1ex] \frac{ }{ \href{../exec/modules.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}} \href{../exec/modules.html#match-externtype}{\leq} \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}} }\end{split}\]

Tables#

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

Limits \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1\) match \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2\).
Both \(\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}_1\) and \(\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}_2\) are the same.

\[\frac{ \href{../exec/modules.html#match-limits}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1 \href{../exec/modules.html#match-limits}{\leq} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2 }{ \href{../exec/modules.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1~\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}) \href{../exec/modules.html#match-externtype}{\leq} \href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2~\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}) }\]

Memories#

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

Limits \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1\) match \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2\).

\[\frac{ \href{../exec/modules.html#match-limits}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1 \href{../exec/modules.html#match-limits}{\leq} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2 }{ \href{../exec/modules.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1 \href{../exec/modules.html#match-externtype}{\leq} \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2 }\]

Globals#

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

Both \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_1\) and \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_2\) are the same.

\[\begin{split}~\\[-1ex] \frac{ }{ \href{../exec/modules.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}} \href{../exec/modules.html#match-externtype}{\leq} \href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}} }\end{split}\]