交差型と主要型付けについてのメモ

主要型（principal type）のある体系とは、以下の性質を満たすような体系です。

型環境 $\Gamma$ と項 $M$ が与えられた時、 $M$ につく型 $\sigma$ （一般に複数ありうる）は、何らかの型を具体化したものになっている。

一方、主要型付け（principal typing）のある体系とは、以下の性質を満たすような体系です。

項 $M$ が与えられた時、型をつけるための”最小の仮定”になっている型環境 $\Gamma$ があり、その条件下で $M$ につく型 $\sigma$ は、何らかの型を具体化したものになっている。

単純な例

単純型付きラムダ計算は、主要型のある体系で、かつ主要型付けもある体系です。
let多相付きのラムダ計算は、主要型のある体系ですが、主要型付けはない体系です。
rank 2 までに制限したSystem F（全称型のあるラムダ計算）は、主要型のない体系です。主要型付けもありません。
制限のないSystem Fも、同様に主要型のない体系で、主要型付けもありません。
rank 2 までに制限した交差型システムは、主要型があり、主要型付けもある体系です。
制限のない交差型システムも、主要型があり、主要型付けもある体系です。

let多相付きラムダ計算が、主要型のある体系なのに、主要型付けがないのは不思議に思うかもしれません。これは、以下の原因によるようです（微妙に勘違いしているかも？）。

letを使えば、多相的な型を型環境に持ち込める。
しかし、自由変数（ラムダ抽象の引数になるかもしれない）に多相的な型をつけるわけにはいかない（冠頭多相、つまり rank 1 までの制限があるため）。

System F では、（rank 2 までに制限してもしなくても） $(\lambda x. x \ x)$ に型をつけることはできても、それらすべてが何かを具体化したものになっている、という「何か」を表現できません。こういった反例があるため、主要型のない体系となります。当然、主要型付けもありません。

交差型システムなら、主要型もあり、主要型付けもあります。

主要型付けのなにがいいのか

主要型付けがある場合、特定の部分項の要求する最小の仮定が導かれることになります。これにより、（項の外の変数をキャプチャしてたとしても）プログラムを書き換えた時のリビルドが最小限で済むようにできます。

交差型システムは、すべての強正規化可能な項に型をつけられる、について

rank 2 までに制限した System F と、rank 2 までに制限した交差型システムでは、どちらも同じ項の集合に型をつけることができました。

一方、制限なしの交差型システムでは、強正規化可能である項すべてに型をつけられるそうです。制限なしの System F では強正規化可能であるが型をつけられない項が存在するのと対照的です。、

一見これはすごいことのように思えます。強正規化可能、つまり停止するプログラムすべてに対し、その証明である型が存在すると言っているのですから。

しかし、実は驚くべきことではありません。強正規化可能、つまり停止するのですから、ある部分項が評価されるのは高々有限回です。よって、その時々に応じて適切な型というのを決めることができ、それらすべての交差型を持って来れば型付け可能だからです。これは、「このプログラムは10¹⁰⁰ステップで停止するよ」といった証拠に類似で、検証するためにはプログラムを実行するのと大差ない労力がかかってしまいます。

型体系	主要型	主要型付け	型推論（型再構築）	型付けできる項
単純ラムダ計算	あり	あり	できる	少ない
let 多相	あり	なし	DEXPTIME完全	それなり
rank 2 System F	なし	なし	DEXPTIME完全	多め
rank 2 交差型システム	あり	あり	DEXPTIME完全	↑と同じ
System F	なし	なし	決定不能	かなり多め
交差型システム	あり	あり	決定不能	すべての強正規化可能な項