型システムの勉強の続き。
有界量化を持つ体系 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 にも）それは入れていない。