カインド（種, kind）とは、

Wikipedia says, "In type theory, a kind is the type of a type constructor or, less commonly, the type of a higher-order type operator. A kind system is essentially a simply typed lambda calculus 'one level up,' endowed with a primitive type, denoted * and called 'type', which is the kind of any (monomorphic) data type."
（https://wiki.haskell.org/Kind（wikipediaを引用しているhaskellwikiの引用））

ここに日本語の説明が。
https://haskell.jp/blog/posts/2017/13-about-kind-system-part2.html（詳しい）
http://walk.northcol.org/haskell/type-classes/#_カインド

私の理解

• kind == 型コンストラクターの型（これは比喩なのか、==で良いのか？）
• 引数を取らずに具体的な型になっている（Intなど）型のカインドは*
• (->)のカインドは* -> * -> *（型定義の時にしか使わない記号だから考えたことがなかったけど確かにそうですね、というかこの記号のカインドを、この記号を使って表現していてなんか再帰的っぽい）
• 型クラスにもカインドがある（？？？）

例

Int, Stringなどの型のカインドは*

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

値のカインドは？

Prelude> :set -XDataKinds
Prelude> :k 1
1 :: GHC.Types.Nat
Prelude> :k "a"
"a" :: GHC.Types.Symbol
Prelude> :k True
True :: Bool

NatやSymbolというのはNumやIsStringなどの型クラスっぽいと思ったけど、調べてみると、データ型として定義されている。。。

Prelude> :i GHC.Types.Nat
data GHC.Types.Nat  -- Defined in ‘GHC.Types’
Prelude> :i GHC.Types.Symbol
data GHC.Types.Symbol   -- Defined in ‘GHC.Types’

型コンストラクターのカインド

Prelude> :k Maybe
Maybe :: * -> *
Prelude> :k IO
IO :: * -> *
Prelude> import Data.Map
Prelude Data.Map> :k Map
Map :: * -> * -> *

型クラスのカインド

Prelude Data.Map> :k Num
Num :: * -> Constraint
Prelude Data.Map> :k Eq
Eq :: * -> Constraint
Prelude Data.Map> :k Ord
Ord :: * -> Constraint

ということは、、、

Prelude Data.Map> :k Num Int
Num Int :: Constraint
Prelude Data.Map> :k Eq String
Eq String :: Constraint
Prelude Data.Map> :k Ord Bool
Ord Bool :: Constraint

Constraintって何だろう？
ここに説明があるからまた今度お勉強しよう。

よくわからないこと

• プログラムを実装する時、どういう場面でこの知識が役に立つ？
• servantでAPIを定義する時によくわからないコンパイルエラーが出るのは、これが関係しているっぽい
• Nat?, Symbol?
• Constraintとは？

でも、コンパイル時にしばしば出てくる"Expected kind ‘* -> *’, but ‘Int’ has kind ‘*’"の意味がわかったので大きな進歩。