交差型 (intersection types)

型システムの勉強の続き。

有界量化を持つ体系 System F<: (Fsub) に続いて、交差型を持つ体系 F (Finter) を実装する。

作ったものは、前と同じ GitHub に置いてある:

https://github.com/minoki/LambdaQuest

TaPL でも交差型について言及されているが、あまり詳しく書いてあるとは言えない。そこで、B. C. Pierce の Programming with Intersection Types and Bounded Polymorphism (1991) という論文を参考にした。著者のサイトにPDFが置いてある。似たようなトピックの論文が他にもあるようだが、それらとの関係は確認していない。

論文の Finter では有界量化の上界に関して反変な部分型関係を入れているが、それをやると(TaPLにもあるように)部分型関係が決定手続きでなくなるらしいので、今回実装した Finter には(前回実装した Fsub にも)それは入れていない。

目次

型の正規化(標準形)

交差型を持つ体系では、α同値ではないが部分型関係に関して同値な型が大量に発生する。例えば、 A → (B ∧ C) と (A → B) ∧ (A → C) という2つの型はα同値ではないが、部分型関係に関して同値である。

部分型関係を判定する際に、同値な型が複数の表し方をされていると困るので、型の表し方を正規化する必要がある。つまり、交差型の ∧ がなるべく外に出るようにする(ただし、関数の引数と有界量化の上界の ∧ は外に出せないのでそこ止まり)。

ゼロ個の型に関する交差型と、型付けできないはずの項

2個の型に関する交差型は、容易に、 \(n\) 個の型に関する交差型へと一般化できる。さて、ここで \(n=0\) の場合を許すべきだろうか?(以下、ゼロ個の型に関する交差型を ⊤ と書く)

\(n\) 個の型に関する交差型は、\(n\) が大きくなるほど「狭く」なる。逆に、\(n\) が小さくなるほど「広く」なり、 \(n=0\) の場合はどんな項にも型を付けられるようになる。(集合のアナロジーで言えば、ゼロ個の集合に関する共通部分は全体集合)

この型 ⊤ は、任意の型に対する上位型 Top と似ているが、微妙に違いがある。どういうことかというと、 Top は型付けできる (well-typed) 項に対してしかつかないが、⊤ は型付けできないはずの項(例えば、関数でないものに関数適用する: 0 1 )にもつけることができる。

なぜか。

ある項 t に型 Top をつけるには、ある型 A について型付け t : A をチェックしてから部分型関係 A <: Top および部分型関係に関する型付け規則を使う。

一方、交差型の場合はどうか。ある項 t に交差型 A ∧ B をつけるには、型付け t : A と t : B をチェックすれば良い。同様に、 t に \(n\) 個の型に関する交差型 \(\bigwedge_{i} A_i\) をつけるには、 \(n\) 個の型付け \(t : A_i\) をチェックすれば良い。\(n=0\) の場合はこれは、何の仮定もなしに t に交差型 ⊤ をつけることができる、ということになる。

これではあまりよろしくない(そもそも型をつける意義とは何だったかという話になる)ので、ゼロ個の型に関する交差型は禁止した方が良さそうである。

交差型のついた関数を定義する

組み込みの関数 (add: Int → Int → Int ∧ Real → Real → Real) や演算子に交差型がついているのとは別に、自分で定義した関数に交差型を持たせることができると便利である。

例えば、与えられた数を2倍する関数で、次のような型を持つものを書きたい:

double : Int → Int ∧ Real → Real

ラムダ項としては λx. add x x なのだが、 x の型をどのようにすれば良いか困る。 λx: Int. add x x だと Int → Int となってしまうし、λx: Real. add x x だと Real → Real になってしまう。型抽象を使って Λa. λx: a. add x x とすると「x の型が Int か Real である」という情報がないので型がつかない。

というわけで、新しい構文が必要である。Reynolds による Forsythe という言語では λx: Int, Real. という感じでラムダ抽象の引数の型を複数書けるようにしたらしい。これを使うと double 関数は次のように書ける:

double = λx: Int, Real. add x x

ちなみに、この引数のところに、本体の型付けに失敗するような型を加えても、全体の型付けが失敗するわけではない(型は変わらない):

(λx: Int, Real, Unit. add x x) : Int → Int ∧ Real → Real

一方、 Pierce の論文では(それが初出かは知らないが)、もう少し一般化した for 構文というものを導入している。これを使うと「有限集合 {Int, Real} を動く」型変数を導入でき、 double 関数は次のように書ける:

double = for a in Int, Real. λx: a. add x x

ラムダ抽象を拡張する方法と比べ、型変数なので、型適用にも使えることが特長か。

これで、よくある関数オーバーロードと同じように、 Int → Int ∧ Real → Real という型を持つ関数を作れたが、あくまで、関数の本体の記述は1つしかない。仮に型ごとに本体を別々に書けるようにすると、整合性 (coherence) が容易に破れるようになってしまう。

意味論

意味論は面倒くさそうである。

最終的に型なしのスクリプト言語等に落とし込む場合は、型というのはおまけに過ぎず消去される運命にあるので、交差型だろうが何だろうが関係ない。

しかし、型が命令の種類やバイナリ表現を規定するタイプの処理系では、交差型の表現を考える必要が出てくる。典型的には、タプルを使って実装するのだろう。あるいは、関数の引数に交差型が出現するのを禁止すれば交差型の表現は考えなくていいかもしれない。