System F
二階ラムダ計算 や 多相ラムダ計算 として知られる｡またこれを型システムに埋め込むことで強力な型を表現できる｡
簡単な例として､よくある id 関数をSystem Fで表すとこのようになる｡
\mathit{id} = \Lambda a. \lambda x : a. x \rightarrow x
xの[* 型をaでパラメタライズ] することで多相性 を獲得している｡
しかし二階ラムダ計算なので型パラメータに二階の型を取ることができない｡では三階ラムダ計算はあるのかと言われると(多分)無い｡
三階以上はもはや青天井と見なしてよいので､[* System F\omega] という無限階のラムダ計算になる｡
System Fを利用した型システムの型推論は(アノテーションが無いと)決定不能になる｡
アノテーションが無いと型推論が決定不能なのはユーザにとってだいぶ面倒なので､もう少し制限することで決定可能にしたい｡
System F制限を加えてアノテーションがなくても決定可能な型推論ができる型システムがHindley-Milner型システムである｡HM型システムはML方言やHaskellなどの型システムの基礎となっている｡
references