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 instruction types for ease of processing.
Number Types
The number type \({\href{../syntax/types.html#syntax-numtype}{\mathit{numtype}}}\) is 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 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}\]
Type Uses
The type use \({\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}}\) is valid if:
\[\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-typeuse}{\vdash} {\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}} : \href{../valid/types.html#valid-typeuse}{\mathsf{ok}}
}
\qquad
\end{array}\]
Heap Types
The heap type \({\href{../syntax/types.html#syntax-absheaptype}{\mathit{absheaptype}}}\) is always 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}\]
The heap type \(({\href{../syntax/types.html#syntax-heaptype}{\mathsf{exact}}^?}~{\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}})\) is valid if:
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
C \href{../valid/types.html#valid-typeuse}{\vdash} {\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}} : \href{../valid/types.html#valid-typeuse}{\mathsf{ok}}
}{
C \href{../valid/types.html#valid-heaptype}{\vdash} {\href{../syntax/types.html#syntax-heaptype}{\mathsf{exact}}^?}~{\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}} : \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:
\[\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 \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}\) is valid if:
Either:
The value type \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}\) is of the form \({\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 \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}\) is of the form \({\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 \({\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}\) is of the form \({\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}}\).
The reference type \({\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}}\) is valid.
Or:
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
}{
C \href{../valid/types.html#valid-valtype}{\vdash} \href{../valid/conventions.html#syntax-valtype-ext}{\mathsf{bot}} : \href{../valid/types.html#valid-valtype}{\mathsf{ok}}
}
\qquad
\end{array}\]
Result Types
The result type \({t^\ast}\) is valid if:
\[\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}\]
Block Types
Block types may be expressed in one of two forms, both of which are converted to instruction types by the following rules.
The block type \({\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}}\) is valid as the instruction type \({t_1^\ast}~\rightarrow~{t_2^\ast}\) if:
The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[{\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}}]\) exists.
The expansion of \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[{\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}}]\) is \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast}~\href{../syntax/types.html#syntax-comptype}{\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}}}] \mathrel{\href{../valid/conventions.html#aux-expand-deftype}{\approx}} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast} \href{../syntax/types.html#syntax-comptype}{\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}\]
The block type \({{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}^?}\) is valid as the instruction type \(\epsilon~\rightarrow~{{\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}}^?}\) if:
\[\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}\]
Instruction Types
The instruction type \({t_1^\ast}~{\mathrel{\href{../valid/conventions.html#syntax-instrtype}{\rightarrow}}}_{{x^\ast}}\,{t_2^\ast}\) is valid if:
\[\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}\]
Composite Types
The composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{struct}}~{{\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}}^\ast})\) is valid if:
\[\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}\]
The composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{array}}~{\href{../syntax/types.html#syntax-fieldtype}{\mathit{fieldtype}}})\) is valid if:
\[\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}\]
The composite type \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast}~\href{../syntax/types.html#syntax-comptype}{\rightarrow}~{t_2^\ast})\) is valid if:
\[\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-comptype}{\vdash} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast} \href{../syntax/types.html#syntax-comptype}{\rightarrow} {t_2^\ast} : \href{../valid/types.html#valid-comptype}{\mathsf{ok}}
}
\qquad
\end{array}\]
The field type \(({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~{\href{../syntax/types.html#syntax-storagetype}{\mathit{storagetype}}})\) is valid if:
\[\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}\]
The packed type \({\href{../syntax/types.html#syntax-packtype}{\mathit{packtype}}}\) is always 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}\]
Descriptor Types
The descriptor type \(({(\href{../syntax/types.html#syntax-desctype}{\mathsf{describes}}~{\mathit{tu}}_1)^?}~{(\href{../syntax/types.html#syntax-desctype}{\mathsf{descriptor}}~{\mathit{tu}}_2)^?}~{\mathit{ct}})\) is valid if:
If \({\mathit{tu}}_1\) is defined, then:
If \({\mathit{tu}}_2\) is defined, then:
The composite type \({\mathit{ct}}\) is valid.
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
(C \href{../valid/types.html#valid-typeuse}{\vdash} {\mathit{tu}}_1 : \href{../valid/types.html#valid-typeuse}{\mathsf{ok}})^?
\qquad
(C \href{../valid/types.html#valid-typeuse}{\vdash} {\mathit{tu}}_2 : \href{../valid/types.html#valid-typeuse}{\mathsf{ok}})^?
\qquad
C \href{../valid/types.html#valid-comptype}{\vdash} {\mathit{ct}} : \href{../valid/types.html#valid-comptype}{\mathsf{ok}}
}{
C \href{../valid/types.html#valid-desctype}{\vdash} {(\href{../syntax/types.html#syntax-desctype}{\mathsf{describes}}~{\mathit{tu}}_1)^?}~{(\href{../syntax/types.html#syntax-desctype}{\mathsf{descriptor}}~{\mathit{tu}}_2)^?}~{\mathit{ct}} : \href{../valid/types.html#valid-desctype}{\mathsf{ok}}
}
\qquad
\end{array}\]
Recursive Types
Recursive types are validated with respect to the first type index defined by the recursive group.
The recursive type \((\href{../syntax/types.html#syntax-rectype}{\mathsf{rec}}~{{\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}^\ast})\) is valid for the type index \(x\) if:
Either:
Or:
The sub type sequence \({{\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}}^\ast}\) is of the form \({\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 for the type index \(x\).
The recursive type \((\href{../syntax/types.html#syntax-rectype}{\mathsf{rec}}~{{\href{../syntax/types.html#syntax-subtype}{\mathit{subtype}}'}^\ast})\) is valid for the type index \(x + 1\).
\[\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}\]
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-desctype}{\mathit{desctype}}})\) is valid for the type index \(x_0\) if:
The length of \({x^\ast}\) is less than or equal to \(1\).
For all \(x\) in \({x^\ast}\):
The index \(x\) is less than \(x_0\).
The type \(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x]\) exists.
The sub type \({\href{../valid/conventions.html#aux-unroll-deftype}{\mathrm{unroll}}}(C{.}\href{../valid/conventions.html#context}{\mathsf{types}}{}[x])\) is of the form \((\href{../syntax/types.html#syntax-subtype}{\mathsf{sub}}~{y^\ast}~{\href{../syntax/types.html#syntax-desctype}{\mathit{desctype}}'})\).
\({{\href{../syntax/types.html#syntax-desctype}{\mathit{desctype}}'}^\ast}\) is the concatenation of all such \({\href{../syntax/types.html#syntax-desctype}{\mathit{desctype}}'}\).
The descriptor type \({\href{../syntax/types.html#syntax-desctype}{\mathit{desctype}}}\) is valid.
For all \({\href{../syntax/types.html#syntax-desctype}{\mathit{desctype}}'}\) in \({{\href{../syntax/types.html#syntax-desctype}{\mathit{desctype}}'}^\ast}\):
\[\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}}~{y^\ast}~{\href{../syntax/types.html#syntax-desctype}{\mathit{desctype}}'})^\ast
\\
C \href{../valid/types.html#valid-desctype}{\vdash} {\href{../syntax/types.html#syntax-desctype}{\mathit{desctype}}} : \href{../valid/types.html#valid-desctype}{\mathsf{ok}}
\qquad
(C \href{../valid/matching.html#match-desctype}{\vdash} {\href{../syntax/types.html#syntax-desctype}{\mathit{desctype}}} \href{../valid/matching.html#match-desctype}{\leq} {\href{../syntax/types.html#syntax-desctype}{\mathit{desctype}}'})^\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-desctype}{\mathit{desctype}}} : {\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.
Limits
Limits must have meaningful bounds that are within a given range.
The limits range \({}[ n \href{../syntax/types.html#syntax-limits}{\,{..}\,} {m^?} ]\) is valid within \(k\) if:
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
n \leq k
\qquad
(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}\]
Tag Types
The tag type \({\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}}\) is valid if:
The type use \({\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}}\) is valid.
The expansion of \(C\) is \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast}~\href{../syntax/types.html#syntax-comptype}{\rightarrow})\).
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
C \href{../valid/types.html#valid-typeuse}{\vdash} {\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}} : \href{../valid/types.html#valid-typeuse}{\mathsf{ok}}
\qquad
{\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}} \mathrel{\href{../valid/conventions.html#aux-expand-typeuse}{\approx}}_{C} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast} \href{../syntax/types.html#syntax-comptype}{\rightarrow} {}[]
}{
C \href{../valid/types.html#valid-tagtype}{\vdash} {\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}} : \href{../valid/types.html#valid-tagtype}{\mathsf{ok}}
}
\qquad
\end{array}\]
Global Types
The global type \(({\href{../syntax/types.html#syntax-mut}{\mathsf{mut}}^?}~t)\) is valid if:
\[\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}\]
Memory Types
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:
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
C \href{../valid/types.html#valid-limits}{\vdash} {\href{../syntax/types.html#syntax-limits}{\mathit{limits}}} : {2^{{|{\href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}}|} - 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}\]
Table Types
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 range \({\href{../syntax/types.html#syntax-limits}{\mathit{limits}}}\) is valid within \({2^{{|{\href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}}|}}} - 1\).
The reference type \({\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}}\) is valid.
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
C \href{../valid/types.html#valid-limits}{\vdash} {\href{../syntax/types.html#syntax-limits}{\mathit{limits}}} : {2^{{|{\href{../syntax/types.html#syntax-addrtype}{\mathit{addrtype}}}|}}} - 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}\]
External Types
The external type \((\href{../syntax/types.html#syntax-externtype}{\mathsf{tag}}~{\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}})\) is valid if:
\[\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-externtype}{\mathsf{tag}}~{\href{../syntax/types.html#syntax-tagtype}{\mathit{tagtype}}} : \href{../valid/types.html#valid-externtype}{\mathsf{ok}}
}
\qquad
\end{array}\]
The external type \((\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~{\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}})\) is valid if:
\[\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}\]
The external type \((\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~{\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}})\) is valid if:
\[\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}\]
The external type \((\href{../syntax/types.html#syntax-externtype}{\mathsf{table}}~{\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}})\) is valid if:
\[\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}\]
The external type \((\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~{\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}})\) is valid if:
The type use \({\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}}\) is valid.
The expansion of \(C\) is \((\href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast}~\href{../syntax/types.html#syntax-comptype}{\rightarrow}~{t_2^\ast})\).
\[\begin{array}{@{}c@{}}\displaystyle
\frac{
C \href{../valid/types.html#valid-typeuse}{\vdash} {\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}} : \href{../valid/types.html#valid-typeuse}{\mathsf{ok}}
\qquad
{\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}} \mathrel{\href{../valid/conventions.html#aux-expand-typeuse}{\approx}}_{C} \href{../syntax/types.html#syntax-comptype}{\mathsf{func}}~{t_1^\ast} \href{../syntax/types.html#syntax-comptype}{\rightarrow} {t_2^\ast}
}{
C \href{../valid/types.html#valid-externtype}{\vdash} \href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~{\href{../syntax/types.html#syntax-typeuse}{\mathit{typeuse}}} : \href{../valid/types.html#valid-externtype}{\mathsf{ok}}
}
\qquad
\end{array}\]
