Haskellのカインドについて調べてみた

はじめに

この記事ではHaskellのカインドについて、説明させていただきます。
(カインドについて理解に苦しんだので共有させて頂きます。)

カインドとは

カインドとは「型の型」のようなものです。
値が何らかの型に属するように、型は何らかのカインドに属します。
例えば、 "Hello"という値はString型に属しますが、String型は *というカインドに属します。

カインドは型を組み合わせる際のルールを規定することができます。例えば、Maybe型はInt型と組み合わせて Maybe Intという型を生成することができますが、Maybe Maybeのような型は作成できません。

カインドの例

型引数を取らないカインド

GHCiでさまざまな型のカインドを調べると *と表示されます。String型やBool型、Int型はすべて *というカインドになっています。 *という表記は、型引数をとらない型コンストラクタを表しています。

Prelude> :k String
String :: *
Prelude> :k Bool
Bool :: *
Prelude> :k Int
Int :: *

一方で、型引数を取らない型に対して無理やり型引数を与えてあると、エラーが発生します。

Prelude> :k String String
<interactive>:1:1: error:
    • Expected kind ‘* -> k0’, but ‘String’ has kind ‘*’
    • In the type ‘String String’

カインドで規定されていない型同士を組み合わせるとエラーとして検知できるということですね！

型引数をとるカインド

次に型引数をとる型のカインドを調べてみましょう。

Prelude> :k Maybe
Maybe :: * -> *
Prelude> :k []
[] :: * -> *
Prelude> :k IO
IO :: * -> *

StringやBoolなどの型と異なり、 * -> *と表示されています。この * -> *という表記は型引数を１つとる型コンストラクタのカインドを表しています。

ここで、Maybe型に様々な型引数を渡してみましょう。

Prelude> :k Maybe String
Maybe String :: *
Prelude> :k Maybe Bool
Maybe Bool :: *
Prelude> :k Maybe IO

<interactive>:1:7: error:
    • Expecting one more argument to ‘IO’
      Expected a type, but ‘IO’ has kind ‘* -> *’
    • In the first argument of ‘Maybe’, namely ‘IO’
      In the type ‘Maybe IO’

Maybe Stringと Maybe Boolは、*というカインドであり、もうこれ以上型引数を取らないことがわかります。
一方で、 Maybe IOに関しては、 Expecting one more argument to ‘IO’というエラーメッセージが出ており、IO型にもう１つ型引数を渡す旨が伝えられています。

Maybe型は型引数を一つとるようなカインドであるのに対して、IO型も型引数を１つとるようなカインドです。ですので、 Maybe IOは型引数が間違ったものであり、Maybe IOには、カインドが *の型を渡す必要があるということです。以下は、Maybe IOに String型を加えた結果です。

Prelude> :k Maybe (IO String)
Maybe (IO String) :: *

型引数が正常に適用されて、その結果、Maybe(IO String)という型が生成されたことが確認できます。

まとめ

カインドは、型を組み合わせる際のルールを規定するもので、Haskellなどの言語では不正な型の組み合わせをコンパイルエラーとして検知できます。静的型付け言語の場合、コンパイル時に静的に、型引数の整合性をチェックできるという利点があります。

終わりに

乱文失礼しました！カインドについて理解が不十分な状態で無理やり記事を書いたため、全体的に日本語がフワフワしてて、読みづらかったと思います。
もし記事に関する内容でご指摘等あればお願いします。
閲覧ありがとうございました！！