型ファミリーと総和と総積

次は同義語

1. 多相型
2. 総称型
3. 型構成子
4. パラメータ付き型
5. インデックス付き型
6. 型ファミリー

適切な言葉は型値関数、使うのは型ファミリーにする。

型ファミリーとは、Xを集合として、F:X → |C| という写像。Cの対象を型と呼べば、型値関数。X⊆|C| のときが総称型。X∈|C| のときがパラメータ付き型。

型ファミリーFから総和型 Σ(F) と総積型 Π(F) を作れるが、Π(F) の構成には「型バンドルとガンマ・オペレーター」が必要。型バンドルとガンマ・オペレーターを導入しないで説明しても分かりにくい！

型バンドルとは、型のあいだの全射のこと。小さい型と大きい型の区別が必要。小さい型＝型、大きいかも知れない型＝型カインド。総称型は型カインドを域とする型ファミリー。

Seq:N×C → C に対して、左カリー化 ^∩Seq と右カリー化 Seq^∩ を考えると、左カリー化がList、右カリー化がArray。