Haskell の型システム

Haskell/Polymorphism - Wikibooks, open books for an open world


型システムはその表現力に関して、rank-1, rank-2, rank-n として分類されるのだそうだ。一般に rank-n type とは、少なくともひとつのrank-(n-1の引数を持ちかつそのランクより高い引数は持たない「函数」のことである。

高階型の理論基礎ははSystem Fであり、これは二階のラムダ計算(The second-order lambda calculus)としても知られている。

Haskell98は、Hindley-Miler 型システムに基づいている。Hindley-Miler 型システムはSystem Fの制限系であり、量子記号(Forall)とrank-2 types 以上の高階型はサポートしていない。System Fのフルパワーの使うためには、RnakNtypes をEnable にしてHaskellを使えばよい。

しかし、もちろん、Haskell98 が高階型システムを採用していないもっともな理由もある。それは、Full なSystem Fの型推論は非決定(Undecidable)であるからである。つまり、プログラマ型推論がなければ、すべての方を書き下さなければいけない。初期のバージョンのHaskell はHindley-Milner 型システムを採用した。それは簡単なポリモルフィック函数であるが、しかしその代わりに完全な型推論を備えている。

最近の研究では、型署名を書く負担を減らし、かつ実践的なrank-nの型システムをHaskell コンパイラに組み込む取り組みがなされている。