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}\]
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}\]
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-comptype}{\mathit{comptype}}})\) 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-comptype}{\mathit{comptype}}'})\).
\({{\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'}^\ast}\) is the concatenation of all such \({\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'}\).
The composite type \({\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}}\) is valid.
For all \({\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'}\) in \({{\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'}^\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-comptype}{\mathit{comptype}}'})^\ast
\\
C \href{../valid/types.html#valid-comptype}{\vdash} {\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}} : \href{../valid/types.html#valid-comptype}{\mathsf{ok}}
\qquad
(C \href{../valid/matching.html#match-comptype}{\vdash} {\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}} \href{../valid/matching.html#match-comptype}{\leq} {\href{../syntax/types.html#syntax-comptype}{\mathit{comptype}}'})^\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-comptype}{\mathit{comptype}}} : {\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}\]
