类型检查

When dealing with expressions like $x = a + b$：

$$ \begin{aligned}

&\textrm{\textbf{if} two type expressions are \red{equivalent}} \\ &\textrm{\textbf{then} return a given type} \\ &\textrm{\textbf{else} return \texttt{type\_error}}

\end{aligned} $$

类型转换

When dealing with expressions like $x = 2 \times 3.14$:

$$ \gdef\and{\textbf{and}} \begin{aligned}

&\textrm{\textbf{if} ($E_1.type=integer$ \and~$E_2.type = integer$)} \\ & \quad\quad E.type=integer \\ &\textrm{\textbf{else if} ($E_1.type=float$ \and~$E_2.type = integer$)} \\ & \quad\quad … \\ &…

\end{aligned} $$

类型综合

根据子表达式的类型确定表达式的类型。

$$ \gdef\type{\mathrm{type}} \begin{aligned}

&\textrm{\textbf{if}} \quad \type(f) = s \rightarrow t~\wedge~ \type(x) = s \\ &\textrm{\textbf{then}}\quad \type(f(x)) = t

\end{aligned} $$

类型推导:

根据某语言结构的使用方式确定表达式的类型。

$$ \gdef\type{\mathrm{type}} \begin{aligned}

&\textrm{\textbf{if}}\quad \textrm{$f(x)$ is an expression.} \\ &\textrm{\textbf{then}}\quad \exists \alpha,\beta \in \mathbf{Types}.~ \type(f) = \alpha \rightarrow \beta ~\wedge~ \type(x) = \alpha

\end{aligned} $$