# 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-elemtype}{\mathit{elemtype}}$$¶

• The limits $$\href{../syntax/types.html#syntax-limits}{\mathit{limits}}$$ must be valid within range $$2^{32}$$.

• Then the table type is valid.

$\frac{ \href{../valid/types.html#valid-limits}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}} : 2^{32} }{ \href{../valid/types.html#valid-tabletype}{\vdash} \href{../syntax/types.html#syntax-limits}{\mathit{limits}}~\href{../syntax/types.html#syntax-elemtype}{\mathit{elemtype}} \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}} }$