カインド (型理論)
数理論理学や計算機科学の型理論として知られる分野において、カインドは型コンストラクタの型、もしくはより一般的ではないが高階型演算子の型である。カインドシステムは本質的には、基本型という ∗ {\displaystyle *} で表記され「型」と呼ばれる型を持っている「一階上の」単純型付きラムダ計算で、基本型とは型パラメータを必要としない任意のデータ型のカインドである。
カインドは「(データ)型の型」という紛らわしい説明がされることもあるが、実際にはアリティ指定子である。文法的には、多相型を型コンストラクタと見なすのが自然で、従って多相でない型は零項の型コンストラクタと見なせる。しかし全ての零項の型コンストラクタ、従って全ての単相的な型は、同一の最も単純なカインドすなわち ∗ {\displaystyle *} を持つ。
高階型演算子はプログラミング言語にはほとんどないので、ほとんどのプログラミング言語では実際には、カインドはデータ型とパラメータ多相を実装するのに使われるコンストラクタの型を区別するために使われる。HaskellやScalaのような、プログラム的にアクセス可能な方法でパラメータ多相の情報を提供する型システムを持つ言語において、明示的もしくは暗黙的にカインドは現れる。
標準のHaskellでは多相カインドは使えない。これはHaskellでサポートされている、型におけるパラメータ多相とは対称的である。例えば、次の例:
では、zのカインドは ∗ {\displaystyle *} だけでなく ∗ → ∗ {\displaystyle *\rightarrow *} など何でも構わない。Haskellはデフォルトでは、型が他のもの(以下を参照のこと)を明示的に指定しない限り、常にカインドを ∗ {\displaystyle *} と推論する。従って型チェッカは次のようなTreeの使い方を受け付けない:
というのは、[]のカインドの ∗ → ∗ {\displaystyle *\rightarrow *} は、常に ∗ {\displaystyle *} となるzの期待されるカインドと適合しない。
しかし高階型演算子は使える。例えば:
はカインド ( ∗ → ∗ ) → ∗ → ∗ {\displaystyle (*\rightarrow *)\rightarrow *\rightarrow *} を持つ。つまりuntは単項のデータコンストラクタだと期待され、それを適用する引数は型でなければならず、そして型を返す。
GHCにはPolyKinds拡張があり、KindSignaturesと一緒に使うことで多相カインドが使えるようになる。例えば:
(注記: Haskellのドキュメントでは関数の型とカインドの両方で同じ矢印を使っている。)
Haskellのカインドシステムには2つの規則だけがある。
「型」と発音される ∗ {\displaystyle *} は全てのデータ型のカインドである。
k 1 → k 2 {\displaystyle k_{1}\rightarrow k_{2}} は単項の型コンストラクタで、 k 1 {\displaystyle k_{1}} カインドの型を取り k 2 {\displaystyle k_{2}} カインドの型を生成する。
具体型(Haskellでの真の型の呼び名)は値が存在する型である。例えば、状況を複雑にする型クラスは無視して、4はInt型の値であり、その一方[1, 2, 3]は[Int]型(Intのリスト)の値である。従って、Intと[Int]はカインド ∗ {\displaystyle *} を持つが、任意の関数の型、例えばInt -> BoolやInt -> Int -> Boolでさえ、同じカインド ∗ {\displaystyle *} を持つ。
型コンストラクタは1つ以上の型引数を取り、十分な引数が与えられたときデータ型を生成する。