53ningen.com53ningen.com
Loading...

ラムダ抽象への型の割りあて

2015/01/08 10:16
2015/01/08 10:16
Programming
ラムダ計算
型
ブール値と単純なラムダ計算を組み合わせた言語を考えてみましょう。このとき例えば以下のような項の正確な型解析は困難です。
if <<とても長く複雑な計算>> then true else (λx.x)
これは実際に条件の項を評価するまで、ブール値を返すのか、関数を返すのか判断がつきません。しかしながら、ブール値も関数も両方ともラムダ抽象として表現することができます。つまり、true は λx.true と読み替え、λx.x は λx.y.y と読み替えるということです。
そこでラムダ抽象自体に 型 → を割り当てる型付け規則 λx.t: → を追加すると先ほどの if 文は → と型付けすることができます。まあでもちょっとこれは無理がありますね。then 節と else 節で返すものをむりやり → として同一視しましたが、結局は違うものなので、あまり意味がないのです。
つまりただ単に関数が返されるというだけでなく、その関数がどんな型を返すのかということがわからなければ有用でないということになります。さらに関数が呼び出されたときに正しく振る舞うことを保証するために、引数の型がどうあるべきかということも分からなければ困ります。

ラムダ抽象に型を割り当てる

もう一度、λx.t のようなラムダ抽象に型を割り当てることについて考えてみましょう。これまでにわかったようにラムダ抽象が引数に適用するとどんな型を返すのかということと、引数に期待されている型が何かという情報が必要そうです。
引数に期待されている型がわかるようにラムダ抽象 λx.t を λx:T. t と書くようにしましょう。このときこのラムダ抽象における引数 x は 型 T の値となることが期待されることを意味します。
さて次にラムダ抽象 λx.t の返す型についてですが、正しい型の引数 x が与えられれば、 t の型になるのは明らかです。t の型を U としておきましょう。そうするとこのラムダ抽象は型 T の引数を受け取り、型 U の値を返すという特徴を持った関数であると言えます。
これを直感的に T → U と書くとわかりやすいのではないでしょうか。さらにこれは冒頭で定義したラムダ抽象への型付け → で不足していた情報が補われた形となっています。さて、それではこういったものを型の体系に組み込むために型 Bool 上の単純型の集合を次のように定義しておきます。
[型 Bool 上の単純型の集合]
T ::= T → T | Bool
こうするとラムダ抽象への型付け規則を以下のように定義することができます（推論式の上段 => 推論式の下段という書き方をしています）。
x: T ├ t: U => ├ λx: T.t: T → U
またラムダ抽象は入れ子になり得るために、自由変数がどんな型を持つかという情報が必要になります。したがって型付け関係は t: T の二項関係ではなく、Γ ├ t:T という三項関係になり、ちょっと複雑になります。Γ は型付け文脈や型環境と呼ばれたりします。文脈を持たない場合は Φ ├ t:T または省略して ├ t:T などと書きます。
ラムダ抽象への型付け規則のより一般的なものは以下のようになります。
Γ, x: T ├ t: U => Γ ├ λx: T.t: T → U

ラムダ計算への単純な型付け

ラムダ計算は変数・ラムダ抽象・関数適用からなるというものでした。うちラムダ抽象に対して型付け規則を定義しました。ここでは残りの変数と、関数適用についても型付け規則を定義してみましょう。
まとめると以下のような形になります。
[構文]
項 t ::= x | λx:T. t | t t
値 v ::= λx:T. t
型 T ::= T → T
文脈 Γ ::= Φ | Γ, x:T

[型付け Γ ├ t:T ]
(a) x:T ∈ Γ => Γ ├ x:T
(b) Γ, x:T ├ t:U => Γ ├ λx:T. u: T → U
(c) Γ ├ t:T → U, Γ ├ t':T => Γ ├ t u: U

[評価 t → t']
(1) t → t' => t u → t' u
(2) u → u' => t u → t u'
(3) => (λx:T. t). v → [x → v] t
このように規定される計算を単純型付きラムダ計算とよびます。