第 6 章型の解析と型推論

型代入の考え方

6.5.3項での説明の通り，型推論アルゴリズム ${\cal W}$ は与えられた型環境 $\Gamma$ と式 $e$ を受け取り，型 $\tau$ と型代入 $S$ の組を返す

{\cal W}(\Gamma,e)=(S,\tau)

の形の関数である．この ${\cal W}$ の内部構造を理解し，さらに，新たな式の定義を考える上での鍵は，型代入 $S$ の役割の理解にある．型代入が複数でてきて分かりにくいと思えたら，

型代入の作成は，型の制約が成り立つ「新しい世界」を作る操作

と考えるてみよう．前の世界の型 $\tau$ や型環境 $\Gamma$ は，新しい世界では $S(\tau)$ および $S(\Gamma)$ となる．この考え方の下では，関数適用のケース

{\cal W}(\Gamma,e_{1}\ e_{2})=

let

(S_{1},\tau_{1})={\cal W}(\Gamma,e_{1})

(S_{2},\tau_{2})={\cal W}(S_{1}(\Gamma),e_{2})

S_{3}={\cal U}(\{(S_{2}(\tau_{1}),\tau_{2}\rightarrow t)\})

(

t

fresh)

(S_{3}S_{2}S_{1},S_{3}(t))

は以下の計算を行っている，と理解できる．

1.

式 $e_{1}$ $e_{2}$ の制約解消されていない世界の $\Gamma$ が与えられている．
2.

$e_{1}$ の制約を満たす世界を表す型代入 $S_{1}$ とその世界での $\Gamma$ つまり（ $S_{1}(\Gamma)$ ）の下での $e$ の型 $\tau_{1}$ を求める．

$(S_{1},\tau_{1})={\cal W}(\Gamma,e_{1})$
3.

さらに， $e_{2}$ の制約を満たす新しい世界を表す $S_{2}$ と，その世界での型環境 $S_{1}(\Gamma)$ の下での $e_{2}$ の型 $\tau_{2}$ を求める．

$(S_{2},\tau_{2})={\cal W}(S_{1}(\Gamma),e_{2})$
4.

この世界で， $e_{1}\ e_{2}$ の型を表す新しい型変数 $t$ を作る．この世界では， $\tau_{1}$ は $S_{2}(\tau_{1})$ であるから，型規則が要求する等式は

$S_{2}(\tau_{1})=\tau_{2}\rightarrow t$

である．この等式を満たす世界を表す型代入 $S_{3}$ を求める．

$S_{3}={\cal U}(\{(S_{2}(\tau_{1}),\tau_{2}\rightarrow t)\})$

この新しい世界では $t$ は $S_{3}(t)$ である．
5.

最初に与えられた世界の型をこの世界に送る型代入は $S_{3}S_{2}S_{1}$ であるから，返すべき値は $(S_{3}S_{2}S_{1},S_{3}(t))$ である．

この考え方を会得すれば，種々の新しい構文に対する型推論手順を書くことができるはずである．例として，7.3節で解説するfix式の型規則
(fix) $\Gamma\{f:\tau_{1}\rightarrow\tau_{2},x:\tau_{1}\}\vdash e:\tau_{2}$ $\Gamma\vdash\mbox{{\tt fix $f$($x$) => $e$}}:\tau_{1}\rightarrow\tau_{2}$
の定義を書いてみよう．考え方を以下の通りである．

1.

式fix $f$ ( $x$ ) => $e$ の制約が解消されていない世界の $\Gamma$ が与えられている．
2.

$f$ と $x$ の型を表現するために，この世界で新しい型変数 $t_{1}$ と $t_{2}$ を作成し， $e$ の制約を満たす世界を表す $S_{1}$ と，その世界での型環境 $\Gamma\{f:t_{1}\rightarrow t_{2},x:t_{1}\}$ の下での $e$ の型 $\tau$ を求める．

$(S_{1},\tau)={\cal W}(\Gamma\{f:t_{1}\rightarrow t_{2},x:t_{1}\},e)$
3.

この新しい世界では， $t_{2}$ は $S_{1}(t_{2})$ であるから，型規則の制約を表す等式は

$S_{1}(t_{2})=\tau$

である．この等式を満たす世界を表す型代入 $S_{2}$ を求める．

$S_{2}={\cal U}(\{(S(t_{2}),\tau)\})$
4.

この世界では， $t_{1}\rightarrow t_{2}$ は $S_{2}S_{1}(t_{1}\rightarrow t_{2})$ であり，もとの世界をこの世界に移す代入は $S_{2}S_{1}$ であるから，求める解は

$(S_{2}S_{1},S_{2}S_{1}(t_{1}\rightarrow t_{2}))$

である．

以上から， ${\cal W}$ の定義は，

{\cal W}(\Gamma,\mbox{{\tt fix $f$($x$) => $e$}})=

let

(S_{1},\tau)={\cal W}(\Gamma\{f:t_{1}\rightarrow t_{2},x:t_{1}\},e)

(

t_{1}

t_{2}

fresh)

S_{2}={\cal U}(\{(S_{1}(t_{2}),\tau)\})

(S_{2}S_{1},S_{2}S_{1}(t_{1}\rightarrow t_{2}))

となる．

第 6 章 型の解析と型推論

型代入の考え方

第 6 章型の解析と型推論