Types

Most types are universally valid. However, restrictions apply to exception tag types and 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}} }\]

Tag Types

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

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

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

  • Then the tag type is valid.

\[\frac{ }{ \href{../valid/types.html#valid-tagtype}{\vdash} [t^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [] \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-tagtype}{\mathsf{tag}}~\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}\)

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

  • Then the external type is valid.

\[\frac{ \href{../valid/types.html#valid-tagtype}{\vdash} \href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}} \mathrel{\mbox{ok}} }{ \href{../valid/types.html#valid-externtype}{\vdash} \href{../syntax/types.html#syntax-tagtype}{\mathsf{tag}}~\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}} \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 }\]

Tags

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

  • Both \(\href{../syntax/types.html#syntax-tagtype}{\mathsf{tag}}~\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}_1\) and \(\href{../syntax/types.html#syntax-tagtype}{\mathsf{tag}}~\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}_2\) are the same.

\[\frac{ }{ \href{../exec/modules.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-tagtype}{\mathsf{tag}}~\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}} \href{../exec/modules.html#match-externtype}{\leq} \href{../syntax/types.html#syntax-tagtype}{\mathsf{tag}}~\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}} }\]

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