カインド (型理論)

数理論理学や計算機科学の型理論として知られる分野において、カインドは型コンストラクタの型、もしくはより一般的ではないが高階型演算子の型である。カインドシステムは本質的には、基本型というformula_1で表記され「型」と呼ばれる型を持っている「一階上の」単純型付きラムダ計算で、基本型とは型パラメータを必要としない任意のデータ型のカインドである。
カインドは「（データ）型の型」という紛らわしい説明がされることもあるが、実際にはアリティ指定子である。文法的には、多相型を型コンストラクタと見なすのが自然で、従って多相でない型は零項の型コンストラクタと見なせる。しかし全ての零項の型コンストラクタ、従って全ての単相的な型は、同一の最も単純なカインドすなわちformula_1を持つ。
高階型演算子はプログラミング言語にはほとんどないので、ほとんどのプログラミング言語では実際には、カインドはデータ型とパラメータ多相を実装するのに使われるコンストラクタの型を区別するために使われる。HaskellやScalaのような、プログラム的にアクセス可能な方法でパラメータ多相の情報を提供する型システムを持つ言語において、明示的もしくは暗黙的にカインドは現れる。
Haskell のカインド.
Haskellのカインドシステムには2つの規則だけがある。
具体型（Haskellでの真の型の呼び名）は値が存在する型である。例えば、状況を複雑にする型クラスは無視して、codice_1はcodice_2型の値であり、その一方codice_3はcodice_4型（Intのリスト）の値である。従って、codice_2とcodice_4はカインドformula_1を持つが、任意の関数の型、例えばcodice_7やcodice_8でさえ、同じカインドformula_1を持つ。
型コンストラクタは1つ以上の型引数を取り、十分な引数が与えられたときデータ型を生成する。すなわち、型コンストラクタはカリー化により部分適用をサポートしする。これがHaskellが多相型を獲得した方式である。例えば、型codice_9（リスト）は型コンストラクタで、リストの要素の型を指定するために1つの引数を取ります。従って、codice_4（Intのリスト）やcodice_11（Floatのリスト）やcodice_12（Intのリストのリスト）でさえ、型コンストラクタcodice_9の妥当な適用である。それゆえに、codice_9はformula_4カインドの型である。codice_2はformula_1というカインドを持つため、これをcodice_9に適用するとformula_1カインドのcodice_4になる。2-tupleのコンストラクタcodice_18はカインドformula_5を持ち、3-tupleのコンストラクタcodice_19はカインドformula_18(以下同様) を持つ。
カインド推論.
標準のHaskellでは多相カインドは使えない。これはHaskellでサポートされている、型におけるパラメータ多相とは対称的である。例えば、次の例:
data Tree z = Leaf | Fork (Tree z) (Tree z)
では、codice_20のカインドはformula_1だけでなくformula_4など何でも構わない。Haskellはデフォルトでは、型が他のもの（以下を参照のこと）を明示的に指定しない限り、常にカインドをformula_1と推論する。従って型チェッカは次のようなcodice_21の使い方を受け付けない:
type FunnyTree = Tree [] -- invalid
というのは、codice_9のカインドのformula_4は、常にformula_1となるcodice_20の期待されるカインドと適合しない。
しかし高階型演算子は使える。例えば:
data App unt z = Z (unt z)
はカインドformula_24を持つ。つまりcodice_24は単項のデータコンストラクタだと期待され、それを適用する引数は型でなければならず、そして型を返す。
GHCにはcodice_25拡張があり、codice_26と一緒に使うことで多相カインドが使えるようになる。例えば:
data Tree (z :: k) = Leaf | Fork (Tree z) (Tree z)
type FunnyTree = Tree [] -- OK