53ningen.com53ningen.com
Loading...

型付きλ計算と単純な拡張

2015/01/15 10:14
2015/01/15 10:14
Programming
ラムダ計算
型
記事「プログラミング言語を形式的に取り扱う」、「ラムダ抽象への型の割りあて」において、変数、ラムダ抽象、関数適用の３つの要素からなるラムダ項に対して、型付け規則を導入しました。
型の導入の仕方にはおおきく２つあります。最初に項を定義して、それらがどうふるまうかどうかを示す評価の部分、意味論を定義し、最後にプログラム的に意味を持たない型システムを導入するスタイルをカリースタイルとよびます。
それに対して、項を定義し、それに対する型付け規則を定義して、正しく片付けされた項にのみ意味付けをするという、型付けが意味論に対して優先されるものをチャーチスタイルとよびます。
これらどちらのスタイルを取るにしても、型付け規則は文字通り、項に対してどう型付けをするかという規則なだけで、型とはどういうものかは定義されていません。一般のプログラミング言語にはあらかじめ定義された基本型、あるいはプリミティブ型などとよばれる型があるのが一般的です。そこで型付きラムダ計算の単純な拡張として、まず基本型を定義するところからはじめていきましょう。

基本型の導入と単純型付きラムダ計算の拡張

一般的なプログラミング言語でのプリミティブ型は数やブール値や文字などで、それらは構造を持たない単純な値の集合と考えることができます。また多くの場合、これらを操作するための適切な演算も定義されている。こうしたものを基本型の集合 A と書くことにします。基本型は型システム的には内部構造を持たないため、原子型ともよばれています。これを型の定義に追加するとすれば、以下のような形になります。
型 T ::= T → T | A (原子型)
基本的な数値を用いて組を作るということは計算をするときによくやります。たとえばほとんどの人は、数学で数字と数字を組み合わせて２次元座標を表現した経験があると思います。より難しい言葉でこの組の構造を表現すると「型 T, U の直積 {t ,u}」とか言ったりします。このときこの組の型は T × U という書き方をします。
直積を導入する際に、第 1 要素と第 2 要素をそれぞれ取り出せないとデータ構造として不便というか使い物になりません。そこでそれぞれを取り出す構文として {t, u}.1 と {t, u}.2 を導入します。これはまた小難しい用語で射影などとよばれていたりします。
さて、単純型付きラムダ計算を拡張してこれを導入するためには追加で以下の構文・評価・型付け規則の導入が必要になります。
[構文形式]
構文 t ::= ... | { t, t } | t.1 | t.2
値　 v ::= ... | { v, v }
型　 T ::= ... | U × V (U, V ⊆ T)

[評価規則] （項:t, u, s 値: v）
{ t, u }.1 => t
{ t, u }.2 => u
t → u => t.1 → u.1
t → u => t.2 → u.2
t → u => { t, s } → { u, s } t → u => { v, t } → { v, u }

[型付け規則]
Γ ├ t: T　Γ ├ u: U => Γ ├ { t, u }: T × U
Γ ├ t: T × U => Γ ├ t.1: T
Γ ├ t: T × U => Γ ├ u.1: U

コンポジットなパターン

さて、もう少し複雑な拡張を考えてみることにしましょう。多くのプログラムでは種類が違う値が混合した集まりを扱う必要性があります。例えばディレクトリ構造を表現するような場合、要素としてフォルダとファイルという異なる種類のものを持てる必要性があります。これはより一般的にいえばこういう構造を木構造とよばれている、葉と枝という違った要素を子として持つような構造を指します。
これまではある要素に対してはこの型の値しか入らないという硬直したシステムを取っていました。しかしこれでは木構造のようなものの表現がなかなか難しくなります。そこで、ざっくり言ってしまうと 「型 T か 型 U のどちらかが入っているような型」というものを定義してしまうことにしましょう。これは数学的に言うと、直和とよばれているもので T + U と書いたりします。
T + U 型の値をつくるためには T の値、 U の値にそれぞれタグ付けをすれば良いです。T + U の表記の順番に従って、左側の型の値を left t として、右側の型の値を right r とします。
また、この T + U 型の値は計算をするときは取り出せなければ困ります。そのためのパターンマッチ的な構文 case(x: T + U) of left t ~> t' | right u ~> u' も導入しておきます。このとき追加すべき構文・評価・型付け規則は以下のようになります。
[構文形式]
構文 t ::= ... | left t | right t | case t of left x ~> t | right x ~> t
値　 v ::= ... | left v | right v
型　 T ::= ... | T + T

[評価規則] （項:t, u, s 値: v）
(1) case left v of left x ~> t | right y ~> u → [x -> v] t
(2) case right v of left x ~> t | right y ~> u → [y -> v] u
(3) t → t' => case t of left x ~> t | right y ~> u → case t' of left x ~> t | right y ~> u
(4) t → t' => left t → left t'
(5) t → t' => right t → right t'

[型付け規則]
(a) Γ ├ t: T => Γ ├ left t: T + U
(b) Γ ├ t: U => Γ ├ right u: T + U
(c) Γ ├ t: T + U　　　Γ, x: T ├ s: S　　　Γ, y: U ├ u: S => Γ ├ case t of left x ~> s | right y ~> u: S
これで晴れて Int + Int や Int + Bool のような型とその値を表現できるようになりました。このような形は実際 Scala や Haskell といった言語では Either という形で実装されています。Java などでは、GoF のコンポジットパターンを用いて実装することができます。
ちなみに直和型 T + U は T と U のすべての要素をどちらの集合出身かというラベリングをした上で保持するため、要素の数は T の要素の数と U の要素の数の和になっています。直積型 T × U は T と U それぞれの要素の数の組み合わせ、つまり掛け算した数だけ要素を持っています。