高階型と種（カインド）システム

型にも「型」がある：種（カインド）とは何か

値に型があるように、型にも分類があります。それが 種（kind, カインド） で、「型の型」と呼ばれます。値の世界で 5 :: Int（5 の型は Int）と書くのと並行して、型の世界では Int :: *（Int の種は *）と書きます。*（star, 単に「型」と読む）は それ自体で値を持てる完成した型 の種です。Int、Bool、String、Maybe Int はすべて種 * を持ちます。これらは「具体型」で、その型の値を実際に作れます。

一方、Maybe や List を単独で見ると、これらは値を直接持てません。Maybe という値は存在せず、Maybe Int まで埋めて初めて Just 3 のような値が作れます。Maybe は 型を1つ受け取って型を返す関数のような型 で、これを 型コンストラクタ（type constructor） と呼びます。その種は * -> * です。

Int        :: *           -- 具体型（値を持てる）
Maybe      :: * -> *       -- 型を1つ取って具体型を返す
Maybe Int  :: *           -- 適用済みなので具体型
Either     :: * -> * -> *  -- 型を2つ取る
Either e   :: * -> *       -- 1つ部分適用すると * -> *

種は値の関数の型とちょうど相似形です。Maybe :: * -> * は「種 * の型を1つ与えると種 * の型が返る」と読み、Maybe Int :: * はその「型レベルの適用」の結果です。種が表しているのは本質的に その型コンストラクタが受け取る型引数の数（アリティ） です。

高階型：型コンストラクタを型引数に取る

ここからが核心です。高階型（higher-kinded type, HKT） とは、* -> * のような「それ自体が引数を取る型コンストラクタ」を、さらに別の型の型引数として受け取れる ことを指します。普通のジェネリクス（ジェネリクス）は * の型を引数に取ります。List<T> の T は Int や String、つまり種 * の具体型です。高階型はその一段上で、T の位置に List や Maybe そのもの（種 * -> *）を入れられます。

なぜこれが要るのか。Functor（写像可能なもの）を考えます。Maybe a にも List a にも map 相当の操作があり、「箱の中身だけを関数で変換し、箱の構造は保つ」という同じ性質を持ちます。これを 箱の種類 f を抽象したまま一度だけ 書きたい。それには f を型引数に取りつつ、f a のように f をさらに型に適用できる必要があります。

class Functor f where           -- f は箱（型コンストラクタ）
  fmap :: (a -> b) -> f a -> f b

instance Functor Maybe where
  fmap g (Just x) = Just (g x)
  fmap _ Nothing  = Nothing

instance Functor [] where        -- [] は List の型コンストラクタ
  fmap = map

ここで f は * -> * の種を持つ高階の型変数です。fmap のシグネチャに f a と f b が現れる時点で、f は「型に適用される側」、つまり型コンストラクタでなければなりません。これが高階型抽象です。HKT を持たない言語（Java、Go、TypeScript など）では f を「中身を埋めない箱のまま」型引数にできないため、Functor を真に汎用な一つの宣言として書けません。

種検査：種が合わない型は無意味

型に種があるということは、型の世界にも「型エラー」に相当する 種検査（kind checking） があるということです。Functor f の f は種 * -> * を要求します。ここに種の合わない型を入れると、型レベルで弾かれます。

Either は種 * -> * -> * で穴が2つあります。Functor が要求する * -> * に直接は合いませんが、Either String のように 1つ型を部分適用 すると種が * -> * になり、入れられます。実際 instance Functor (Either e) は、左の型 e を固定して右側だけを写す Functor になります。この「部分適用で種を合わせる」操作は、値レベルでの関数の部分適用（カリー化）と完全に並行します。型エラーが「Int 型のところに String を渡した」なら、種エラーは「* -> * のところに種 * の Int を渡した」に相当します。

Monad：高階型抽象の代表例

Functor の上に積み上がるのが Applicative と Monad です。Monad m も m :: * -> * を要求する高階抽象で、「計算を順に連鎖する」構造を箱の種類 m から独立に記述します。

class Applicative m => Monad m where
  return :: a -> m a                  -- 値を箱に入れる
  (>>=)  :: m a -> (a -> m b) -> m b  -- 中身を取り出し次の計算へ繋ぐ（bind）

m が Maybe なら「途中で Nothing が出たら以降を打ち切る」失敗の連鎖、[] なら「全組み合わせを展開する」非決定計算、IO なら「副作用付き計算の逐次合成」になります。箱ごとに >>= の中身は違うのに、Monad m という一つの抽象がそれらを束ねられる のは、m を高階型変数として持てるからです。HKT がなければ「任意のモナドに対して動く関数」（例えば sequence :: Monad m => [m a] -> m [a]）を一度だけ書くことはできません。

これらの抽象は数学の圏論（category theory）に由来し、Functor/Applicative/Monad は満たすべき法則（恒等律・結合律など）を持ちます。法則自体は種検査では強制されませんが、種システムは「そもそも法則を語れる正しい形をしているか」という骨格を保証します。多相の正体（トレイト/型クラスと辞書渡し）と組み合わせると、Monad m => という制約は実行時には m ごとの辞書として渡され、HKT はその辞書が「どんな箱に対するものか」を型レベルで整合させる役割を担います。

型理論の中での位置づけ

種システムは突然現れた仕掛けではなく、型理論 の自然な延長です。値を型で分類するのと同じ営みを、型を種で分類することへ持ち上げたものです。System Fω は多相ラムダ計算（System F）に「型を作る型（型コンストラクタ）」と種の概念を足した体系で、まさに高階型の数理的土台です。種 * -> * は型レベルの関数型に他ならず、型コンストラクタの適用は型レベルのβ簡約に対応します。

まとめ

種（カインド）は型を分類する「型の型」で、* が値を持てる具体型、* -> * が型を1つ取る型コンストラクタを表し、矢印の数が引数のアリティに対応します。高階型は * -> * のような型コンストラクタ自体を型引数として受け取れる能力で、これがあるからこそ Functor f・Monad m を箱の種類 f/m を抽象したまま一度だけ定義でき、Maybe・List・IO といった異なる構造を一つの抽象で束ねられます。種が合わなければ型は無意味になり（種検査）、Either のような穴の多い型は部分適用で種を * -> * に揃えます。値・型・種という三層は、ラムダ計算から続く同じ階層構造の延長であり、代数的データ型 で組み立てた箱を高階に抽象する力こそが、関数型プログラミングの再利用性の源泉です。