Kind (type theory)

ウィキペディア

カインド (型理論)

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/05/04 23:59 UTC 版)

数理論理学や計算機科学の型理論として知られる分野において、カインドは型コンストラクタの型、もしくはより一般的ではないが高階型演算子の型である。カインドシステムは本質的には、基本型という $*$で表記され「型」と呼ばれる型を持っている「一階上の」単純型付きラムダ計算で、基本型とは型パラメータを必要としない任意のデータ型のカインドである。

カインドは「（データ）型の型」という紛らわしい説明がされることもあるが、実際にはアリティ指定子である。文法的には、多相型を型コンストラクタと見なすのが自然で、従って多相でない型は零項の型コンストラクタと見なせる。しかし全ての零項の型コンストラクタ、従って全ての単相的な型は、同一の最も単純なカインドすなわち $*$を持つ。

高階型演算子はプログラミング言語にはほとんどないので、ほとんどのプログラミング言語では実際には、カインドはデータ型とパラメータ多相を実装するのに使われるコンストラクタの型を区別するために使われる。HaskellやScalaのような、プログラム的にアクセス可能な方法でパラメータ多相の情報を提供する型システムを持つ言語において、明示的もしくは暗黙的にカインドは現れる。

例

• 「型」と発音される $*$は全てのデータ型のカインドで、零項の型コンストラクタと見ることができ、この文脈において真の型とも呼ばれる。これは通常関数型言語の関数の型を含む。
• $*\rightarrow *$は単項の型コンストラクタのカインドであり、例えばリスト型のコンストラクタのカインドである。
• $*\rightarrow *\rightarrow *$は（カリー化により）二項の型コンストラクタのカインドであり、例えばペア型のコンストラクタや関数の型のコンストラクタのカインドである。（混乱しないように注意しておくと、その適用の結果自身は関数の型であり、従って $*$カインドの型である）
• $(*\rightarrow *)\rightarrow *$は、単項の型コンストラクタから真の型へ変換する高階型演算子のカインドである。応用についてはPierce (2002) 32章を参照のこと。

Haskell のカインド

(注記: Haskellのドキュメントでは関数の型とカインドの両方で同じ矢印を使っている。)

Haskellのカインドシステムには2つの規則だけがある。

• 「型」と発音される $*$は全てのデータ型のカインドである。
• $k_{1}\rightarrow k_{2}$は単項の型コンストラクタで、 $k_{1}$カインドの型を取り $k_{2}$カインドの型を生成する。

具体型（Haskellでの真の型の呼び名）は値が存在する型である。例えば、状況を複雑にする型クラスは無視して、4はInt型の値であり、その一方[1, 2, 3]は[Int]型（Intのリスト）の値である。従って、Intと[Int]はカインド $*$を持つが、任意の関数の型、例えばInt -> BoolやInt -> Int -> Boolでさえ、同じカインド $*$を持つ。

型コンストラクタは1つ以上の型引数を取り、十分な引数が与えられたときデータ型を生成する。すなわち、型コンストラクタはカリー化により部分適用をサポートしする。これがHaskellが多相型を獲得した方式である。例えば、型[]（リスト）は型コンストラクタで、リストの要素の型を指定するために1つの引数を取ります。従って、[Int]（Intのリスト）や[Float]（Floatのリスト）や[[Int]]（Intのリストのリスト）でさえ、型コンストラクタ[]の妥当な適用である。それゆえに、[]は $*\rightarrow *$カインドの型である。Intは $*$というカインドを持つため、これを[]に適用すると $*$カインドの[Int]になる。2-tupleのコンストラクタ(,)はカインド $*\rightarrow *\rightarrow *$を持ち、3-tupleのコンストラクタ(,,)はカインド $*\rightarrow *\rightarrow *\rightarrow *$(以下同様) を持つ。

カインド推論

標準のHaskellでは多相カインドは使えない。これはHaskellでサポートされている、型におけるパラメータ多相とは対称的である。例えば、次の例:

data Tree z  = Leaf | Fork (Tree z) (Tree z)

では、zのカインドは $*$だけでなく $*\rightarrow *$など何でも構わない。Haskellはデフォルトでは、型が他のもの（以下を参照のこと）を明示的に指定しない限り、常にカインドを $*$と推論する。従って型チェッカは次のようなTreeの使い方を受け付けない:

type FunnyTree = Tree []     -- invalid

というのは、[]のカインドの $*\rightarrow *$は、常に $*$となるzの期待されるカインドと適合しない。

しかし高階型演算子は使える。例えば:

data App unt z = Z (unt z)

はカインド $(*\rightarrow *)\rightarrow *\rightarrow *$を持つ。つまりuntは単項のデータコンストラクタだと期待され、それを適用する引数は型でなければならず、そして型を返す。

GHCにはPolyKinds拡張があり、KindSignaturesと一緒に使うことで多相カインドが使えるようになる。例えば:

data Tree (z :: k) = Leaf | Fork (Tree z) (Tree z)
type FunnyTree = Tree []     -- OK

関連項目

• System F-omega
• 純粋型システム

出典

• Pierce, Benjamin (2002). Types and Programming Languages. MIT Press. ISBN 0-262-16209-1 , chapter 29, "Type Operators and Kinding"