依存型

型が値に依存できる型システム。Π（依存関数型, 全称）と Σ（依存ペア型, 存在）を持つ。

プログラマ向けの一言

「長さ3の配列」「正の整数」「ソート済みリスト」を型として表現できる。 普通の型システムでは「number の配列」までしか言えないが、依存型では「長さが n の number の配列」と言える。

コードで理解する

// --- 普通の TypeScript ---
function head(arr: number[]): number {
  return arr[0]; // arr が空だったら？ → undefined が返る → バグ
}

// --- 依存型があれば ---
// 「長さが1以上の配列」を型で表現
// function head(arr: Vec<number, n>): n > 0 ? number : never
// → 空配列を渡すとコンパイルエラー

// TypeScript のタプルで疑似的に:
function safeHead(arr: [number, ...number[]]): number {
  return arr[0]; // 必ず1つ以上ある → 安全
}
safeHead([1, 2, 3]); // OK
// safeHead([]);       // コンパイルエラー

依存型の核心: 型の中に値が入る

// 普通の型: 型と値は別の世界
type NumberArray = number[];  // 「number の配列」としか言えない

// 依存型: 型が値をパラメータに取れる
// Vec<number, 3>   ← 型の中に「3」という値が入っている
// Vec<number, n>   ← 型の中に変数 n が入っている

// Idris（依存型言語）での例:
// append : Vec n a -> Vec m a -> Vec (n + m) a
// ↑ 長さ n のベクタと長さ m のベクタを結合すると長さ n+m のベクタ
// → 型レベルで長さの計算をしている

// TypeScript で無理やり近いことをすると:
type Vec<T, N extends number> = N extends 0 ? [] : [T, ...Vec<T, Subtract<N, 1>>];
// ↑ 実際にはこの Subtract は標準で使えないので限界がある

何が嬉しいか

// 1. 行列の掛け算で次元ミスをコンパイル時に防ぐ
// multiply : Matrix<m, n> -> Matrix<n, p> -> Matrix<m, p>
// → n が一致しないとコンパイルエラー

// 2. printf の書式文字列と引数の一致をチェック
// printf "%d is %s" : Int -> String -> IO ()
// → 引数の型と個数を書式文字列から導出

// 3. ソート済みリストを型で表現
// insert : (x : Int) -> SortedList -> SortedList
// → 結果が本当にソート済みであることを型が保証

Π と Σ: カリー=ハワードの ∀ / ∃ 対応

依存型の中核は2つの型構築子。単純型の A -> B と A × B を「右側が左の値に依存できる」よう一般化したもの:

型	読み	単純型での退化形	論理での対応
`Π(x:A). B(x)` 依存関数型	「各 `x:A` に対し `B(x)` の値を返す関数」	`B` が `x` に依存しなければ `A -> B`	全称 `∀x. P(x)`
`Σ(x:A). B(x)` 依存ペア型	「ある `x:A` と、それに対する `B(x)` の値の組」	`B` が `x` に依存しなければ `A × B`	存在 `∃x. P(x)`

これがカリー=ハワードの真価: 型 = 命題、プログラム = その証明。Π(n:Nat). Vec n a -> a（長さ n の非空ベクタから要素を取れる）という型を持つ関数を書けたこと自体が ∀n. ... の証明になる。Σ(n:Nat). Vec n a（「ある長さを持つベクタ」= 長さを隠した存在）は存在量化。Σ(p : SortedList). ... のように「証拠付きの値」を返すのにも使う。

-- Agda: ∀(全称)と∃(存在)が Π/Σ そのもの
filter : (A → Bool) → List A → Σ[ n ∈ ℕ ] Vec A n
--                                  ↑ 「ある長さ n が存在して、長さ n の Vec を返す」= ∃
replicate : (n : ℕ) → A → Vec A n
--          ↑ 「すべての n に対して長さ n の Vec を作れる」= ∀

依存型固有の難しさ

表現力の代償として、単純型・篩型にはない本質的な困難がある:

型検査の決定不能性 — 型が値の計算を含むため、型の等価判定 Vec (2+2) a ≟ Vec 4 a は項を評価して比べる必要がある（definitional equality / 型変換規則 conversion rule）。任意計算を許すと停止性に帰着し、型検査が一般に決定不能になる。実用言語はこれを 停止性チェッカで関数を全域(total)に制限して回避する（Agda/Idris の termination checker、Coq の guardedness condition）。全域性が崩れると loop : A のような「何でも証明できる」項ができ、論理が矛盾する。
証明義務 (proof obligation) — 「長さが一致する」「結果はソート済み」を型で要求した瞬間、その証拠を構築する責務がコードに乗る。n + 0 = n のような自明な等式すら、型レベルでは明示的な証明項（rewrite, cong, tactic）で埋める必要がある。これが依存型プログラミングの体感コストの大半。
型推論の喪失 — 単純型の Hindley-Milner のような完全な推論はもう効かない。型は基本的に人間が宣言し、処理系は検査するだけ（暗黙引数の単一化はあるが部分的）。
証明とコードの絡まり — アルゴリズム本体と正しさの証明が同じ項に同居し、書き換えが波及する。dependent pattern match で型が局所的に書き換わる（依存マッチの coverage）など、認知負荷が高い。

単純型 vs 篩型 vs 依存型

軸	単純型	篩型	依存型
型に載るもの	構造のみ	基底型 + decidable 述語	任意の値・計算
例	`Int -> Int`	`{v:Int \| v > 0}`	`Π(n).Vec n a`
検証	構文的一致	SMT が自動放電	人手 / tactic で証明構築
型推論	完全 (HM)	述語は宣言、基底は推論	ほぼ不可、宣言が基本
決定可能性	決定可能	述語を制限すれば決定可能	一般に決定不能（全域性で回避）
表現力	低	中（範囲・整合性）	高（任意の仕様・定理）
コスト	最小	注釈	注釈 + 証明
代表	Java, Go	Liquid Haskell, F*	Idris, Agda, Coq, Lean

→ 三段階の連続体。篩型は依存型から「型の中の計算」を削って自動化を得た中間点（篩型の比較表と対）。

トレードオフ

得るもの — テストでは届かない「すべての入力で正しい」を型が保証。仕様がコードに内在し、型が通れば（全域性の前提下で）その性質は成り立つ。次元安全性・プロトコル遵守・アルゴリズム正当性まで表現可能。
失うもの — 推論の自動性、軽快な書き換え、学習の平易さ。証明義務が開発速度を直撃する。
使いどころ — 数学の形式化、安全臨界、クリティカルなコア部分。アプリ全体を依存型で書くのは通常過剰で、篩型や幽霊型で十分なことが多い。「証明したい性質の重要度 × 失敗コスト」が注釈・証明コストを上回るときに引く札。

代表的な言語

Idris — 汎用の依存型プログラミング言語。実行効率も意識し、QTT（量的型理論）で消去/線形性も型に載せる
Agda — 依存型 + 定理証明。dependent pattern match が強力
Coq — 定理証明が主目的だが、検証済みコードを OCaml/Haskell へ抽出できる
Lean — 数学の形式化 + プログラミング。mathlib が巨大

押さえどころ（カード化候補）

依存型とは → 型が値に依存できる型システム。Π(依存関数=∀)と Σ(依存ペア=∃)を持ち、「長さ n の配列」「ソート済みリスト」を型で表現できる。
Π/Σ と ∀/∃ → カリー=ハワードで Π(x:A).B(x) = 全称 ∀x.P(x)、Σ(x:A).B(x) = 存在 ∃x.P(x)。型 = 命題、その型の項を書けたこと = 証明。
決定不能性 → 型が値の計算を含むため型の等価判定が項評価に帰着し、型検査が一般に決定不能。実用言語は全域性(total)制限で回避。全域性が崩れると論理が矛盾する。
証明義務 → 「長さ一致」「ソート済み」を型で要求した瞬間、証拠を構築する責務がコードに乗る。n+0=n すら明示証明が要る。これが体感コストの大半。
三段階の連続体 → 単純型(構造のみ・推論完全) ⊂ 篩型(述語・SMT 自動) ⊂ 依存型(任意計算・証明手動)。表現力↑ と引き換えに自動化↓・コスト↑。篩型は依存型から計算を削った中間点。

依存型