主要型
最も代表的な型
例えばある関数がf :: a -> b -> aだったとき、
このfの型を規則に基づき推論するとき
a :: c -> d、b :: e -> gとしても同じ推論が成り立つ
こうすると、a、bは任意の型を持つことになるが、いずれにしてもa->b->aとすれば、fの型に適合する
この様な最もprincipalな型のことを主要型という
主要型は一意に定まる
定義
型$ Aが項$ tの主要型であるとは以下が成り立つことを言う
$ \vdash t:Aが成り立つ
$ \vdash t:Bが成り立つなら、$ A中の型変数に対する型代入$ Sが存在して、$ B\equiv SAとなる 型環境を考慮した定義
型環境$ \Gammaと項$ tに対する主要型とは、以下を満たす型代入$ Sと型$ Tの組である
$ S\Gamma\vdash t:T
任意の$ S'\Gamma\vdash t:T'なる$ S',T'について、
ある$ S''が存在し、
$ S''(S\Gamma)\equiv S'\Gammaかつ$ S''T\equiv T'
定理
項$ tが型を持つなら、$ tは主要型を持つ
つまり、$ tが主要型を持つならそれを返し、持たないなら持たない旨を知らせる
この計算は$ tの長さに対して線形の計算量で求まる
参考