カインド推論
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/05/04 23:59 UTC 版)
「カインド (型理論)」の記事における「カインド推論」の解説
標準のHaskellでは多相カインドは使えない。これはHaskellでサポートされている、型におけるパラメータ多相とは対称的である。例えば、次の例: data Tree z = Leaf | Fork (Tree z) (Tree z) では、zのカインドは ∗ {\displaystyle *} だけでなく ∗ → ∗ {\displaystyle *\rightarrow *} など何でも構わない。Haskellはデフォルトでは、型が他のもの（以下を参照のこと）を明示的に指定しない限り、常にカインドを ∗ {\displaystyle *} と推論する。従って型チェッカは次のようなTreeの使い方を受け付けない: type FunnyTree = Tree [] -- invalid というのは、[]のカインドの ∗ → ∗ {\displaystyle *\rightarrow *} は、常に ∗ {\displaystyle *} となるzの期待されるカインドと適合しない。 しかし高階型演算子は使える。例えば: data App unt z = Z (unt z) はカインド ( ∗ → ∗ ) → ∗ → ∗ {\displaystyle (*\rightarrow *)\rightarrow *\rightarrow *} を持つ。つまりuntは単項のデータコンストラクタだと期待され、それを適用する引数は型でなければならず、そして型を返す。 GHCにはPolyKinds拡張があり、KindSignaturesと一緒に使うことで多相カインドが使えるようになる。例えば: data Tree (z :: k) = Leaf | Fork (Tree z) (Tree z)type FunnyTree = Tree [] -- OK
※この「カインド推論」の解説は、「カインド (型理論)」の解説の一部です。
「カインド推論」を含む「カインド (型理論)」の記事については、「カインド (型理論)」の概要を参照ください。
- カインド推論のページへのリンク
