カインド (型理論)のソースを表示

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

カインドは「[[データ型|（データ）型]]の型」という紛らわしい説明がされることもある{{誰によって|date=2018年10月23日 (火) 12:39 (UTC)}}が、実際には[[アリティ]]指定子である。文法的には、多相型を型コンストラクタと見なすのが自然で、従って多相でない型は[[零項]]の型コンストラクタと見なせる。しかし全ての零項の型コンストラクタ、従って全ての単相的な型は、同一の最も単純なカインドすなわち<math>*</math>を持つ。

高階型演算子は[[プログラミング言語]]にはほとんどないので、ほとんどのプログラミング言語では実際には、カインドはデータ型と[[パラメータ多相]]を実装するのに使われるコンストラクタの型を区別するために使われる。[[Haskell]]や[[Scala]]のような、プログラム的にアクセス可能な方法でパラメータ多相の情報を提供する型システムを持つ言語において、明示的もしくは暗黙的にカインドは現れる。<ref name="higherkinds">[http://adriaanm.github.com/files/higher.pdf Generics of a Higher Kind]</ref>

== 例 ==

* 「型」と発音される<math>*</math>は全ての[[データ型]]のカインドで、[[零項]]の型コンストラクタと見ることができ、この文脈において真の型とも呼ばれる。これは通常[[関数型言語]]の関数の型を含む。
* <math>* \rightarrow *</math>は[[単項]]の[[型コンストラクタ]]のカインドであり、例えば[[リスト (抽象データ型)|リスト型]]のコンストラクタのカインドである。
* <math>* \rightarrow * \rightarrow *</math>は（[[カリー化]]により）[[wiktionary:binary|二項]]の型コンストラクタのカインドであり、例えば[[ペア型]]のコンストラクタや[[関数の型]]のコンストラクタのカインドである。（混乱しないように注意しておくと、その適用の結果自身は関数の型であり、従って<math>*</math>カインドの型である）
* <math>(* \rightarrow *) \rightarrow *</math>は、単項の型コンストラクタから真の型へ変換する高階型演算子のカインドである。応用についてはPierce (2002) 32章{{要出典|date=2018年10月23日 (火) 12:39 (UTC)}}を参照のこと。

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

[[Haskell]]のカインドシステム<ref name="haskell98">[http://www.haskell.org/onlinereport/decls.html#sect4.1.1 Kinds - The Haskell 98 Report]</ref>には2つの規則だけがある。

* 「型」と発音される<math>*</math>は全ての[[データ型]]のカインドである。
* <math>k_1 \rightarrow k_2</math>は[[単項]]の[[型コンストラクタ]]で、<math>k_1</math>カインドの型を取り<math>k_2</math>カインドの型を生成する。

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

型コンストラクタは1つ以上の型引数を取り、十分な引数が与えられたときデータ型を生成する。すなわち、型コンストラクタはカリー化により[[部分適用]]をサポートしする。<ref name=haskell-2010>{{cite web|title=Chapter 4 Declarations and Binding|url=http://www.haskell.org/onlinereport/haskell2010/haskellch4.html#x10-65017x3|work=Haskell 2010 Language Report|accessdate=23 July 2012}}</ref><ref>{{cite web|last=Miran|first=Lipovača|title=Learn You a Haskell for Great Good!|url=http://learnyouahaskell.com/making-our-own-types-and-typeclasses|work=Making Our Own Types and Typeclasses|accessdate=23 July 2012}}</ref>これがHaskellが多相型を獲得した方式である。例えば、型<code>[]</code>（リスト）は型コンストラクタで、リストの要素の型を指定するために1つの引数を取ります。従って、<code>[Int]</code>（Intのリスト）や<code>[Float]</code>（Floatのリスト）や<code>[&#91;Int&#93;]</code>（Intのリストのリスト）でさえ、型コンストラクタ<code>[]</code>の妥当な適用である。それゆえに、<code>[]</code>は<math>* \rightarrow *</math>カインドの型である。<code>Int</code>は<math>*</math>というカインドを持つため、これを<code>[]</code>に適用すると<math>*</math>カインドの<code>[Int]</code>になる。2-[[タプル|tuple]]のコンストラクタ<code>(,)</code>はカインド<math>* \rightarrow * \rightarrow *</math>を持ち、3-tupleのコンストラクタ<code>(,,)</code>はカインド<math>* \rightarrow * \rightarrow * \rightarrow *</math>(以下同様) を持つ。

== カインド推論 ==

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

<syntaxhighlight lang=haskell>
data Tree z  = Leaf | Fork (Tree z) (Tree z)
</syntaxhighlight>

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

<syntaxhighlight lang=haskell>
type FunnyTree = Tree []     -- invalid
</syntaxhighlight>

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

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

<syntaxhighlight lang=haskell>
data App unt z = Z (unt z)
</syntaxhighlight>

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

[[Glasgow Haskell Compiler|GHC]]には<code>PolyKinds</code>拡張があり、<code>KindSignatures</code>と一緒に使うことで多相カインドが使えるようになる。例えば:

<syntaxhighlight lang=haskell>
data Tree (z :: k) = Leaf | Fork (Tree z) (Tree z)
type FunnyTree = Tree []     -- OK
</syntaxhighlight>

== 関連項目 ==
* [[System F-omega]]
* [[純粋型システム]]

== 出典 ==
{{Refbegin}}
* {{cite book|last=Pierce|first=Benjamin|title=[[Types and Programming Languages]]|publisher=MIT Press|date=2002|id=ISBN 0-262-16209-1}}, chapter 29, "Type Operators and Kinding"
{{Refend}}
{{Reflist}}

{{DEFAULTSORT:かいんと}}
[[Category:型理論]]