# 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{../valid/types.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{../valid/types.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{../valid/types.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{../valid/types.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{../valid/types.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{../valid/types.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}} \href{../valid/types.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{../valid/types.html#match-limits}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1 \href{../valid/types.html#match-limits}{\leq} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2 }{ \href{../valid/types.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{../valid/types.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{../valid/types.html#match-limits}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1 \href{../valid/types.html#match-limits}{\leq} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2 }{ \href{../valid/types.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1 \href{../valid/types.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{../valid/types.html#match-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}} \href{../valid/types.html#match-externtype}{\leq} \href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}} }\end{split}$