MiniML3,4 のための型推論 (1): Prelude

関数に関する型付け規則

次に，fun式と関数適用式

  e  ::=  ... | fun x -> e | e_1 e_2

で型推論アルゴリズムを拡張しよう．「$\tau_1$の値を受け取って（計算が停止すれば）$\tau_2$の値を返す関数」の型を$\tau_1 \rightarrow \tau_2$ とすると，型の定義は以下のように変更される． $\tau ::= \mathbf{int} \mid \mathbf{bool} \mid \tau_1 \rightarrow \tau_2.$

これらの式に関する型付け規則を，背後の直観とともに説明する．

`fun`式に関する規則

\[\begin{array}{c} \Gamma, x:\tau_1 \vdash e : \tau_2\\ \rule{10cm}{1pt}\\ \Gamma \vdash \mathbf{fun}\ x \rightarrow e : \tau_1 \rightarrow \tau_2 \end{array} \textrm{T-Fun}\]

引数 $x$ が $\tau_1$ を持つという仮定の下で関数本体 $e$ が $\tau_2$ 型を持つならば，$\mathbf{fun}\ x \rightarrow e$ が $\tau_1 \rightarrow \tau_2$ 型を持つことを導いて良い．$\mathbf{fun}\ x \rightarrow e$ が $x$ を受け取って $e$ を返す関数であることを考えれば納得できるであろう．

関数適用式に関する規則

\[\begin{array}{c} \Gamma \vdash e_1 : \tau_1 \rightarrow \tau_2 \quad \Gamma \vdash e_2 : \tau_1\\ \rule{10cm}{1pt}\\ \Gamma \vdash e_1 \; e_2 : \tau_2 \end{array} \textrm{T-App}\]

$e_1$の型が関数型$\tau_1 \rightarrow \tau_2$であり，かつ，その引数の型$\tau_1$と$e_2$の型が一致している場合に，適用式全体に$e_1$の返り値型$\tau_2$がつくことを導いて良い．これも関数型の直観と関数適用のセマンティクスから納得できるだろう．

型推論アルゴリズムの設計に伴うちょっとした困難

次は型推論アルゴリズムの設計である．これらの規則を含めても型付け規則は構文主導なので，前節の「規則を下から上に読む」という戦略を使ってみよう．入力として型環境$\Gamma$と式$e$が与えられ，式$e$が$\mathbf{fun}\ x \rightarrow e_1$という形をしていたとしよう．そうすると，$\textrm{T-Fun}$を下から上に読んで，以下のように型推論ができそうである．

型環境$\Gamma,x:\tau_1$と式$e_1$を入力として型推論アルゴリズムを再帰的に呼び出し型$\tau_2$を得る．
型$\tau_1 \rightarrow \tau_2$を$e$の型として返す．

ところが，これではうまくいかない．問題は，最初のステップで$e_1$の型を調べる際に作る型環境$\Gamma,x:\tau_1$である．ここで$x$の型として$\tau_1$を取っているが，この型をどのように取るべきかは，一般には$e_1$の中での$x$の使われ方と，この関数$\mathbf{fun}\ x \rightarrow e_1$がどのように使われうるかに依存するので，このタイミングで$\tau_1$を容易に決めることはできない．

簡単な例として，$\mathbf{fun}\ x \rightarrow x+1$という式を考えてみよう．これは，$\mathbf{int} \rightarrow \mathbf{int}$型の関数であることは「一目で」わかるので，一見，$x$の型を $\mathbf{int}$として推論を続ければよさそうだが，問題は，本体式である$x+1$を見ること無しには，$x$ の型が$\mathbf{int}$であることは分からないということにある．

型変数，型代入と型推論アルゴリズムの仕様

今回のように，「今の所わからない情報があるために問題が解けない」という困難を，我々はどのように解決してきただろうか．よくやる戦略は， (1) 未知の情報をとりあえず変数において (2) その変数が満たすべき制約を生成し (3) その制約を満足する変数の値を求める，という方法である．（例えば，鶴亀算にしても，線形計画法のような数値最適化にしても，大体こういう感じのことをやっている．）

この戦略を使ってみよう．「$\tau_1$の適切な取り方が後にならないとわからない」という問題を解決するために「今のところ正体がわからない未知の型」を表す 型変数 (type variable) を導入する．型の文法を

\[\tau ::= \alpha \mid \mathbf{int} \mid \mathbf{bool} \mid \tau_1\rightarrow\tau_2\]

のように拡張する．$\alpha$が新しく導入された型変数で，今の所どの型にすればよいかよくわからない型を表す．

そして，型推論アルゴリズムの出力として，型環境中に現れる型変数の「正体が何か」を返すことにする．上の例だと，とりあえず $x$ の型は $\alpha$ などと置いて，型推論を続ける．推論の結果，$x+1$ の型は $\mathbf{int}$ である，という情報に加え $\alpha = \mathbf{int}$という「型推論の結果$\alpha$は$\mathbf{int}$であることが判明しました」という情報が返ってくることになる．最終的に$\textrm{T-Fun}$より，全体の型は$\alpha \rightarrow \mathbf{int}$，つまり，$\mathbf{int} \rightarrow \mathbf{int}$ であることがわかる．

また，$\mathbf{fun}\ x \rightarrow \mathbf{fun}\ y \rightarrow x\; y$のような式を考えると，以下のような手順で型推論がすすむ．

新しい（つまり，他の型変数とカブらない）型変数$\alpha$を生成し，$x$の型を$\alpha$と置いて，本体，つまり $\mathbf{fun}\ y \rightarrow x\; y$の型推論を行う．
新しい型変数$\beta$を生成し，$y$の型を$\beta$と置いて，本体，つまり $x\; y$ の型推論を行う．
$x\;y$ の型推論の結果，この式の型が別の新しい型変数 $\gamma$ を使って$\beta \rightarrow \gamma$と書け，$\alpha = \beta \rightarrow \gamma$であることが判明する．

さらに詳しい型推論アルゴリズムの中身については後述するが，ここで大事なことは，とりあえず未知の型として用意した型変数の正体が，推論の過程で徐々に明らかになっていくことである．

型変数と多相型: OCaml の 多相型 (polymorphic type) とここで導入する型変数を含む型とを混同してはならない．OCaml においては，例えば fun x -> x が型 'a -> 'a を持ち，ここで表示される 'a を「型変数」ということがある．しかし，この 'a は上記の型変数とは異なる．この'a は「何の型にでも置き換えてよい」変数であるが，上記の型変数は「特定の型を表す」記号である．「任意の型で置き換え可能」な型変数は多相型の節で扱う．

TODO: 多相型へのリンクをはる．

大まかな方針がわかったところで，次節では具体的な実装を見ていこう．

IoPLMaterials