MiniML3,4 のための型推論 (3): 型推論アルゴリズムの実装
ここまでの話を総合すると,MiniML3 のための型推論アルゴリズムが得られる.例えば,$e_1 + e_2$ 式に対する型推論は,$\textrm{T-Plus}$ 規則を下から上に読むと,
- $\Gamma, e_1$ を入力として型推論を行い,$\theta_1$,$\tau_1$ を得る.
- $\Gamma, e_2$ を入力として型推論を行い,$\theta_2$,$\tau_2$ を得る.
- 型代入 $\theta_1, \theta_2$ を $\alpha = \tau$ という形の方程式の集まりとみなして, $\theta_1 \cup \theta_2 \cup \{\tau_1 = \mathbf{int}, \tau_2 = \mathbf{int}\}$ を単一化し,型代入$\theta_3$を得る.
- $\theta_3$ と $\mathbf{int}$ を出力として返す.
となる.部分式の型推論で得られた型代入を方程式とみなして,再び単一化を行うのは,ひとつの部分式から $[\alpha \mapsto \tau_1]$,もうひとつからは $[\alpha \mapsto \tau_2]$ という代入が得られた時に$\tau_1$ と$\tau_2$ の整合性が取れているか(単一化できるか)を検査するためである.
Exercise 4.3.5 [必修]
他の型付け規則に関しても同様に型推論の手続きを与えよ(レポートの一部としてまとめよ).そして,以下の typing.ml
に加えるべき変更の解説を参考にして,型推論アルゴリズムの実装を完成させよ.
Exercise 4.3.6 [**]
再帰的定義のための let rec
式の型付け規則は以下のように与えられる.
\[\begin{array}{c}
\Gamma, f: \tau_1 \rightarrow \tau_2, x: \tau_1 \vdash e_1 : \tau_2 \quad
\Gamma, f:\tau_1 \rightarrow \tau_2 \vdash e_2 : \tau\\
\rule{13cm}{1pt}\\
\Gamma \vdash \mathbf{let\ rec}\ f = \mathbf{fun}\ x\ \rightarrow e_1\ \mathbf{in}\ e_2 : \tau
\end{array}
\textrm{T-LetRec}\]
型推論アルゴリズムが let rec
式を扱えるように拡張せよ.
Exercise 4.3.7 [**]
以下は,リスト操作に関する式の型付け規則である.リストには要素の型を $\tau$ として $\tau\ \mathbf{list}$ という型を与える.型推論アルゴリズムがこれらの式を扱えるように拡張せよ.
T-Nil
\[\begin{array}{c}
\rule{6cm}{1pt}\\
\Gamma \vdash [] : \tau\ \mathbf{list}
\end{array}
\textrm{T-Nil}\]
T-Cons
\[\begin{array}{c}
\Gamma \vdash e_1 : \tau \quad
\Gamma \vdash e_2 : \tau\ \mathbf{list}\\
\rule{6cm}{1pt}\\
\Gamma \vdash e_1 :: e_2 : \tau\ \mathbf{list}
\end{array}
\textrm{T-Cons}\]
T-Match
\[\begin{array}{c}
\Gamma \vdash e : \tau_1\ \mathbf{list} \quad
\Gamma \vdash e_1 : \tau_2 \quad
\Gamma, x : \tau_1, y : \tau_1\ \mathbf{list} \vdash e_2 : \tau_2\\
\rule{20cm}{1pt}\\
\Gamma \vdash \mathbf{match}\ e\ \mathbf{with}\ [] \rightarrow e_1 \mid x :: y \rightarrow e_2 : \tau_2
\end{array}
\textrm{T-Cons}\]