椿の日記

たぶんプログラムの話をします

類(Kind)

「ふつうのHaskellプログラミング」の269ページに次のように書かれていました。

 ちなみに、このように型変数が正しく使われているかどうかチェックするときには類(Kind)という概念が使われています。
 類は型の型のようなものです(型クラスともまた違います)。

どうにもよく分からない。よく分からないので、色々やってみて自分なりに理解してみました…。

実験

うっかり括弧を忘れてしまいがちな次の定義。

    data Hoge = IO Maybe Int

これをコンパイルすると、エラーメッセージとして次のようなものが出てきます。

    `Maybe' is not applied to enough type arguments
    Expected kind `?', but `Maybe' has kind `* -> *'
    In the type `Maybe'
    In the definition of data constructor `IO'
    In the data type declaration for `Hoge'

推測

どうやら Maybe というのは「* -> *」類であるようです。同様に Either を調べると「* -> * -> *」類であると言ってきます。だったら Int とか String とかは「*」類なんでしょう。

また、エラーの表現から IO や Maybe は「型の関数」と言っても良いんだと思います。とすると、このエラーは、型の関数 IO の仮引数(類「*」)に、Maybe(類「* -> *」) という実引数を与えていて、類が不一致していてコンパイルエラーとなっている、と説明できます。

それから、Either が「* -> * -> *」で Maybe が「* -> *」なら「Either Maybe」を評価すると「*」類じゃねーか、とか血迷ったことを一瞬考えてしまったけれど、Either は「(* -> *) -> *」という関数ではないから、そこは問題なし。

感想

ひとまず感覚的にはこんな感じで理解…

どうせ、このKindの型とかもあるんだと思うんですけど、きっと3階4階のテンソルの物理的意味だとか、4次元5次元の図形を想像するのと一緒で、到底、直感的に理解できるような代物ではない気がします…