类型¶

大多数类型都是普遍有效的。但是，对限制适用限制，这些限制必须在验证期间进行检查。此外，块类型会转换为普通的函数类型，以方便处理。

限制¶

限制必须具有有意义的边界，这些边界必须在给定范围内。

\(\{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m^? \}\)¶

\(n\) 的值不得大于 \(k\)。
如果最大值 \(m^?\) 不为空，则
- 其值不得大于 \(k\)。
- 其值不得小于 \(n\)。
则该限制在范围 \(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 }\]

块类型¶

块类型可以用两种形式之一表示，这两种形式都通过以下规则转换为普通的函数类型。

\(\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}\)¶

类型 \(C.\href{../valid/conventions.html#context}{\mathsf{types}}[\href{../syntax/modules.html#syntax-typeidx}{\mathit{typeidx}}]\) 必须在上下文中定义。
则块类型作为函数类型 \(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}}^?]\)¶

块类型作为函数类型 \([] \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}}^?] }\]

函数类型¶

函数类型始终有效。

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

函数类型有效。

\[\frac{ }{ \href{../valid/types.html#valid-functype}{\vdash} [t_1^\ast] \href{../syntax/types.html#syntax-functype}{\rightarrow} [t_2^\ast] \mathrel{\mbox{ok}} }\]

表类型¶

\(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}~\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}\)¶

限制 \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) 必须在范围 \(2^{32}-1\) 内有效。
则表类型有效。

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

内存类型¶

\(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\)¶

限制 \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}\) 必须在范围 \(2^{16}\) 内有效。
则内存类型有效。

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

全局类型¶

\(\href{../syntax/types.html#syntax-mut}{\mathit{mut}}~\href{../syntax/types.html#syntax-valtype}{\mathit{valtype}}\)¶

全局类型有效。

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

外部类型¶

\(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\)¶

函数类型 \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}\) 必须有效。
则外部类型有效。

\[\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}}\)¶

表类型 \(\href{../syntax/types.html#syntax-tabletype}{\mathit{tabletype}}\) 必须有效。
则外部类型有效。

\[\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}}\)¶

内存类型 \(\href{../syntax/types.html#syntax-memtype}{\mathit{memtype}}\) 必须有效。
则外部类型有效。

\[\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}}\)¶

全局类型 \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}\) 必须有效。
则外部类型有效。

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

导入子类型化¶

当实例化模块时，必须提供外部值，其类型与对每个导入进行分类的相应外部类型匹配。在某些情况下，这允许使用简单的子类型化形式（正式写为“\(\href{../valid/types.html#match-externtype}{\leq}\)”），如此处定义。

限制¶

限制 \(\{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_1, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m_1^? \}\) 匹配限制 \(\{ \href{../syntax/types.html#syntax-limits}{\mathsf{min}}~n_2, \href{../syntax/types.html#syntax-limits}{\mathsf{max}}~m_2^? \}\) 当且仅当

\(n_1\) 大于或等于 \(n_2\)。
或者
- \(m_2^?\) 为空。
或者
- \(m_1^?\) 和 \(m_2^?\) 均不为空。
- \(m_1\) 小于或等于 \(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}\]

函数¶

外部类型 \(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_1\) 匹配 \(\href{../syntax/types.html#syntax-externtype}{\mathsf{func}}~\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_2\) 当且仅当

\(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_1\) 和 \(\href{../syntax/types.html#syntax-functype}{\mathit{functype}}_2\) 相同。

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

表¶

外部类型 \(\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)\) 匹配 \(\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)\) 当且仅当

限制 \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1\) 与匹配 \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2\)。
两者 \(\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}_1\) 和 \(\href{../syntax/types.html#syntax-reftype}{\mathit{reftype}}_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{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}}) }\]

内存¶

一个外部类型 \(\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1\) 与 \(\href{../syntax/types.html#syntax-externtype}{\mathsf{mem}}~\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_2\) 匹配当且仅当

限制 \(\href{../syntax/types.html#syntax-limits}{\mathit{limits}}_1\) 与匹配 \(\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 }\]

全局变量¶

一个外部类型 \(\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_1\) 与 \(\href{../syntax/types.html#syntax-externtype}{\mathsf{global}}~\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_2\) 匹配当且仅当

两者 \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_1\) 和 \(\href{../syntax/types.html#syntax-globaltype}{\mathit{globaltype}}_2\) 都相同。

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