カインド (型理論)
From Wikipedia, the free encyclopedia
数理論理学や計算機科学の型理論として知られる分野において、カインドは型コンストラクタの型、もしくはより一般的ではないが高階型演算子の型である。カインドシステムは本質的には、基本型というで表記され「型」と呼ばれる型を持っている「一階上の」単純型付きラムダ計算で、基本型とは型パラメータを必要としない任意のデータ型のカインドである。
カインドは「（データ）型の型」という紛らわしい説明がされることもある[誰によって?]が、実際にはアリティ指定子である。文法的には、多相型を型コンストラクタと見なすのが自然で、従って多相でない型は零項の型コンストラクタと見なせる。しかし全ての零項の型コンストラクタ、従って全ての単相的な型は、同一の最も単純なカインドすなわちを持つ。
高階型演算子はプログラミング言語にはほとんどないので、ほとんどのプログラミング言語では実際には、カインドはデータ型とパラメータ多相を実装するのに使われるコンストラクタの型を区別するために使われる。HaskellやScalaのような、プログラム的にアクセス可能な方法でパラメータ多相の情報を提供する型システムを持つ言語において、明示的もしくは暗黙的にカインドは現れる。[1]
- 「型」と発音されるは全てのデータ型のカインドで、零項の型コンストラクタと見ることができ、この文脈において真の型とも呼ばれる。これは通常関数型言語の関数の型を含む。
- は単項の型コンストラクタのカインドであり、例えばリスト型のコンストラクタのカインドである。
- は（カリー化により）二項の型コンストラクタのカインドであり、例えばペア型のコンストラクタや関数の型のコンストラクタのカインドである。（混乱しないように注意しておくと、その適用の結果自身は関数の型であり、従ってカインドの型である）
- は、単項の型コンストラクタから真の型へ変換する高階型演算子のカインドである。応用についてはPierce (2002) 32章[要出典]を参照のこと。
Haskell のカインド
(注記: Haskellのドキュメントでは関数の型とカインドの両方で同じ矢印を使っている。)
Haskellのカインドシステム[2]には2つの規則だけがある。
具体型（Haskellでの真の型の呼び名）は値が存在する型である。例えば、状況を複雑にする型クラスは無視して、4はInt型の値であり、その一方[1, 2, 3]は[Int]型（Intのリスト）の値である。従って、Intと[Int]はカインドを持つが、任意の関数の型、例えばInt -> BoolやInt -> Int -> Boolでさえ、同じカインドを持つ。
型コンストラクタは1つ以上の型引数を取り、十分な引数が与えられたときデータ型を生成する。すなわち、型コンストラクタはカリー化により部分適用をサポートしする。[3][4]これがHaskellが多相型を獲得した方式である。例えば、型[]（リスト）は型コンストラクタで、リストの要素の型を指定するために1つの引数を取ります。従って、[Int]（Intのリスト）や[Float]（Floatのリスト）や[[Int]]（Intのリストのリスト）でさえ、型コンストラクタ[]の妥当な適用である。それゆえに、[]はカインドの型である。Intはというカインドを持つため、これを[]に適用するとカインドの[Int]になる。2-tupleのコンストラクタ(,)はカインドを持ち、3-tupleのコンストラクタ(,,)はカインド(以下同様) を持つ。
