compiler
型推論
adventcalendar2017

これは何?

  • この記事は、最近 Hindley Milner (Algorithm W) 型推論を理解したばかりの私が、型推論のことをなるべくわかりやすく解説するものです。
  • 簡略化したOCamlのようなコードが登場します。
  • わかりやすさ重視で書いていくつもりなので、専門用語(自由変数とか)はあまり出てきません。 間違いなどあったらコメントしていただけると幸いです。

まずは単相から

ここからは図を使って説明していきます。(ビジュアルなほうがわかりやすいハズ)

とても簡単な例

以下にとても簡単なコードを示します。
ad_base.jpg

見ればわかりますが、xの型はintですね。
ですが、どのようにしてintだとわかったのでしょうか。

ad_01.jpg

すでにわかっていることを書き出しだしてみました。リテラルの右肩を見てください。
1の型は当然ながらintxの型はとりあえず0というidをつけておきました。このidが重要な役割を果たします。

let x = y という式があったとき、xyの型は当然ながら等しくなります。
したがって、先ほどのidが0xの型はintということになります。
以下のT(id)はidがidの変数の型を表しています。

ad_02.jpg

T(0) = intとなりました。
print_intの引数にxがありますが、xのidは0なので、T(0) = intよりxの型はintだとわかります。

関数

以下の画像を見てください。

ad_03.jpg

先ほどの例よりも少し難しくなりました。先に言っておくと、fの型はint -> intxは当然ながらintですね。
まずは先ほどと同じようにわかることを書き出してみます。

ad_04.jpg

let f x y = x + yという式があったとき、fの型はxの型 -> yの型 -> x + yの型と等しくなります。
let式の中身を見てみると、x + 1とあります。これはxの型は1の型、すなわちintと等しいということになります。

ad_05.jpg

x + 1の型はintだとわかりました。するとfの型はint -> intだとわかります。
xの型 -> x + 1の型ということですね

ad_06.jpg

関数2

もうちょっとややこしく。
ad_07.jpg

わかっていることを書いて。
ad_08.jpg

letの式の中身を評価していきます。

gの中のx + yint
よってgxの型 -> x + yの型int -> int
ad_09.jpg

fの中はlet g x = x + y in g xですが、結局はg xです。
gint -> intなのでgの引数のxintg xintとわかります。
結果的にfの型はxの型 -> yの型 -> g xの型int -> int -> intとわかります。
ad_10.jpg

以上、単相型推論の簡単な解説でした。

そして多相へ

さて、多相になるとちょっと難しくなります。

一番最初の例ですが、ちょっと複雑なコードを示します:
ad_0_0.png

わかることを書き出します:
ad_0_1.png

続いて、単相のときと同じように型を推論してみます。
ad_0_2.png

一見正しく型推論できているようですが、
このままだとf 1 2を評価したときに T(0)int -> int -> boolとなってしまい、以降fが呼び出された時に多相性が失われてしまいます。f'a -> 'a -> boolだったはずなのに、'aintで上書きされてしまいます。
f 1.2 3.4などとすると型エラーになるわけです。これではいけません。

ここからは多相型推論の手順を説明します。
下の図のT(2) -> boolの右下をみてください。
ad_0_3.png
何か{}という物がついていますね。ここにはその型に含まれるidから, その型環境に含まれるすべての型のそれぞれに含まれるidからそのそれぞれの型の{}に含まれるidを取り除いたもの, を取り除いたものが含まれます。

... 多分今の説明で理解できた人は少ないと思います ...
ここからは、多相型推論を理解する上で知っておかなくてはならないことをまとめます。

まず型環境というのは、簡単に言えば、ある型を推論する時点ですでに存在が知られている型の集合です。
上の図で3行目までを読み込んでgの型を推論する場合なら、f, x [id=1のやつ], yがそうです。gの型を推論するのですから、gx [id=4のやつ]は含まれません。

そして肝心の {} の役割ですが、ある{}を持つ型は、instantiateされるときにその{}に含まれるidと同じidの型を新しいidの型に変えます。instantiateというのは、ある変数が使われるときに、型の多相性を実現するために、その変数の型に今説明した手順を実行することです。図に示すと次のようになります:
ad_0_4.png

T(0) -> T(0) -> T(0)という型があったとして、{0}がくっついているなら、その中のT(0)を全て新しいT(1)で置換します。T(1)というのは、まだ使われていないidならなんでも良いはずです。

そして、先ほどの長くて難しい文章、{}に含ませるidを決定する操作のことをgeneralizeといいます。汎用的になるんですね。すべての変数はgeneralizeされて{}を持つことになります。

さて、ここまでで一応、多相型推論はできるようになったはずです。やってみましょう。
もう一度先ほどの画像です:
ad_0_3.png

ここまででgの型がわかっています。次はfですね。
画像内のコードの4行目でx [id=1]の型が決定されます。
letでgが定義されているのでgの型には{}が付き、gにxが適用されるのでgがinstantiateされます。
{}の中身を表で計算してみましょう。

集合名 中身
型環境に含まれるすべての型 T(0), T(1), T(2), int, bool
型環境に含まれるすべての型のid 0, 1, 2
型環境に含まれる型の{}に含まれるもの
型環境に含まれるすべての型のidから{}に含まれるものを除いたもの 0, 1, 2
gの型に含まれるid 2
gに含まれるidから, その型環境に含まれるすべての型のそれぞれに含まれるidからそのそれぞれの型の{}に含まれるidを取り除いたもの, を取り除いたもの

よって、{}の中身には何も入りません。

ad_0_5.png
gがinstantiateされましたが、{}の中身が空なのでこの場合特に変化はありません。
fの返却型はg xよりboolです。
このままだと、fの型はT(2) -> T(2) -> boolですが、{}のことを思い出してみましょう。
あのgeneralizeの長い難しい文章通りに手順を踏めば、{2}という結果が得られるはずです。
やってみましょう。

集合名 中身
型環境に含まれるすべての型 int, bool
型環境に含まれるすべての型のid
型環境に含まれる型の{}に含まれるもの
型環境に含まれるすべての型のidから{}に含まれるものを除いたもの
fの型に含まれるid 2
fに含まれるidから, その型環境に含まれるすべての型のそれぞれに含まれるidからそのそれぞれの型の{}に含まれるidを取り除いたもの, を取り除いたもの 2

正しく{2}という結果が得られました。
ad_0_6.png
こうすれば、f 1 2を評価した時にはfの型はT(5) -> T(5) -> boolと評価されて多相性が実現されます。intで上書きされないんですね。

以上が多相型推論の説明でした。この記事自体、急いで書いたので(ただいま 12/19 20:00)わかりづらいところや間違っている部分もあると思います。
コメントお待ちしております。