型推論では普通は主要型を求めるように実装される

最も代表的な型

例えばある関数が 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の長さに対して線形の計算量で求まる

参考

龍田『型理論』 2章