2025年8月26日火曜日

「カインド（kind）を本来的に“誰かが定義した”」という単独の発明者はいません。

 

型のさらに上の階層で型コンストラクタを分類するという発想は、**高階多相ラムダ計算（System Fω）**の系譜で整備され、PL界隈（特に Haskell）で「kind」という用語が広く定着しました。カインドは「一段上の単純型付きλ計算」として説明されることが多く、*（いまの Type）や k1 -> k2 のような記法で表されます。Wikipedia

歴史をざっくり並べると：

  • System F（第二階ラムダ計算）がまず型への量化を導入（Girard 1972／Reynolds 1974）。これが多相型の理論的基盤。Wikipedia+1

  • そこから型演算子まで扱う System Fω へ拡張され、「型の型」を体系的に扱う枠組み（= 現代的なカインド体系）が確立。標準的な教科書説明では、これを「タイプオペレータとカインディング」として扱います。SdiehlSJTU Computer Science

  • 研究論文としても1990年の Bruce–Meyer–Mitchell が「Constructors and Kinds」という節を立て、T を「すべての型の kind」と定めるなど、カインド付き計算を明確に述べています（用語の実務的定着の早い例）。Tufts Computer Science

  • 実用言語では Haskell 98 Report が「Kinds」という節で * と k1 -> k2 を採用し、以後 Haskell/GHC が PolyKinds などで拡張していきました。Haskell

さらに遡ると、型階層そのものの発想は Russell（1908）や Church（1940）の型理論に見られますが、彼らは「sort」「type」などの語を用いており、今日の「kind」というラベルは後年のPL文献・Haskell文脈で普及した呼び名です。要するに、概念は型理論の流れの中で漸進的に形成され、用語“kind”はPLコミュニティで標準化された、というのが実情です。plato.stanford.edu+1

投稿者