依存型と証明としてのプログラム

依存型とは「値に依存する型」

通常の型システムでは、型と値は別の世界にいます。Int という型は、それが 3 か 7 かを知りません。依存型（dependent types）はこの壁を壊し、型が値に依存することを許します。たとえば「長さ n のベクタ」を Vect n a と書けます。ここで n は型ではなく値（自然数）であり、それが型の一部に組み込まれています。Vect 3 Int と Vect 4 Int は異なる型であり、両者を取り違えるとコンパイル時に弾かれます。

この一歩がもたらす効果は大きい。配列アクセスのような、これまで実行時例外でしか守れなかった不変条件を、型のレベルで初めから表現できるようになります。

範囲外参照を型で消す

依存型の威力がもっとも分かりやすいのが、安全な添字アクセスです。要素数を n とすると、有効な添字は 0 以上 n 未満です。この「n 未満」という制約を、型に持つ添字 Fin n（0 から n - 1 までしか値を持たない有限型）で表現します。

-- Idris2 風の擬似コード
index : Fin n -> Vect n a -> a

index は「長さ n のベクタと、n 未満であることが保証された添字」しか受け取りません。Vect 3 a に対して添字 5 を渡そうとすると、5 を Fin 3 に当てはめられず、コンパイルが通りません。範囲チェックを実行時に書く必要も、テストで網羅する必要もない。型検査器が、すべての呼び出しについて範囲内であることを一度に証明してくれます。

Curry-Howard対応の深化：量化子まで

ラムダ計算と型理論で見たCurry-Howard対応は「型＝命題、プログラム＝証明」でした。依存型は、この対応を量化子（全称・存在）まで押し広げます。鍵は2つの型構成子です。

普通の関数型 A -> B は、戻り値の型 B が引数に依存しない特殊な Π 型です。Π 型では戻り値の型が引数の値に依存できる。だから「すべての自然数 n について、n 個の要素を持つベクタを返す」という主張＝型を書け、その型を持つ項を構成することが、その主張の構成的な証明になります。Σ 型は「条件を満たす値が存在する」ことを、実際の値と証拠のペアとして示します。等しさそのものを表す等式型（a = b）も型として存在し、refl（反射律）がその証明項になります。

証明とプログラムの同一視

依存型の言語では、証明とプログラムは同じ言語の項です。両者を分ける境界はありません。型検査が通ることが、対応する命題の証明が完成したことに等しい。たとえば「リスト連結の長さは、各リストの長さの和に等しい」という定理は、次のような型を持つ関数として書けます。

-- Agda 風の擬似コード： ++ の長さは length の和に等しい
length-++ : (xs : Vect m a) -> (ys : Vect n a)
          -> length (xs ++ ys) = m + n

この型を持つ項を、両リストの構造に関する帰納法で構成できれば、定理は証明されたことになります。逆に命題が偽なら、その型を持つ項はどうやっても作れず、コンパイルが通りません。「正しいことしか型付かない」ため、型が成り立つこと自体が安全性の保証になります。これは代数的データ型のパターンマッチ網羅性検査を、任意の不変条件にまで一般化したものと見ることもできます。

Idris / Agda / Lean：三者の立ち位置

依存型を実用する代表が Idris、Agda、Lean です。理論的な核（依存型と Curry-Howard 対応）は共有しつつ、狙いが異なります。

Idris は「依存型をジェネリックな開発で使う」方向で、型が定まると関数の実装候補が絞られる型駆動開発を前面に出します。Agda は証明の対話的構築に重きを置き、未完成箇所を「ホール」として残しながら型に導かれて埋めていきます。Lean は数学の形式化に強く、タクティク（証明を組み立てる命令の連なり）で大規模な証明を構成し、近年の形式数学プロジェクトの基盤になっています。

何にコストを払うのか

依存型は強力ですが、ただ取りではありません。型が値に依存するため、型の等しさを判定するには値を計算（簡約）して比較する必要があり、型検査が一般に決定不能になり得ます。実用言語は全域性や簡約の範囲を制限してこれを御します。また、不変条件を型に載せるほど、その不変条件を維持する証明をプログラマが書くコストが増えます。等式の書き換えや帰納法の手当てが必要になり、記述量は増えます。

まとめ

依存型は、型と値の境界を取り払い、値に依存する型として不変条件をコンパイル時に表現する仕組みです。Curry-Howard 対応を量化子（Π・Σ）まで深めると、型は命題、項は証明となり、Idris・Agda・Lean では証明とプログラムが同じ言語の項として一体化します。型検査が通ること自体が、その仕様が成り立つことの証明である——この見方は、型システムを「制約のチェック」から「仕様の証明」へと読み替える、もっとも先鋭的な到達点です。コストはあるものの、絶対に壊したくない一点を型で封じる道具として、依存型は確かな選択肢になります。