依存型によるプログラミング

ほとんどの静的型付けプログラミングでは、型の世界とプログラミングの世界の間にはハーメチックシール（訳注：気密防水のためのシールのこと）が貼られています。型とプログラミングでは異なる文法が用いられ、異なるタイミングで使用されます。型は通常、コンパイル時に用いられ、プログラムが特定の不変量にしたがうかどうかをチェックします。プログラムは実行時に用いられ、実際に計算を実行します。この2つを相互に作用させる場合、通常は instance-of チェックのような型ケース演算子や、キャスティング演算子などを用いる形で行われます。これらは実行時に検証するために型チェッカに他の方法で得られなかった情報を提供してくれます。言い換えれば、この相互作用は型がプログラムの世界に挿入され、実行時に限定された意味を持つようになるということです。

Leanにおいて、このような厳格な分離は行いません。Leanではプログラムは型を計算し、型はプログラムを含むことができます。プログラムを型の中に置くことで、コンパイル時にその計算能力をフルに使うことができ、関数から型を返す機能により型はプログラミングのプロセスにおいて第一級の参加者となります。

依存型 （dependent type）とは型以外の式を含む型のことです。依存型は関数に与えられる名前付きの引数においてよく見られます。例えば、関数 natOrStringThree は渡された Bool によって自然数か文字列のどちらかを返します：

def natOrStringThree (b : Bool) : if b then Nat else String :=
  match b with
  | true => (3 : Nat)
  | false => "three"

依存型について他にも以下のような例がありました：

• 多相性について導入した節 で定義した posOrNegThree はその引数の値に戻り値の型が依存します。
• OfNat 型クラス はインスタンス化の際に使われた特定の数値リテラルに依存します。
• バリデータの例にて用いられた CheckedInput 構造体 はバリデーション時に渡される年の値に依存します。
• 部分型 は特定の値を参照する命題を含みます。
• 配列の添え字表記 の妥当性決定を含め、本質的に興味深い名地あはすべて値を含む型であり、したがって依存型です。

依存型は型システムの能力を飛躍的に向上させます。引数の値によって戻り値の型を分岐させられる柔軟性により、ほかのシステムでは簡単に与えられないようなプログラムを書くことができます。同時に、依存型は型シグネチャによって関数から返される値を制限することを可能にし、コンパイル時に強力な不変性を強制することを可能にします。

しかし、依存型を使ったプログラミングは非常に複雑であり、関数型プログラミング以上のスキルを必要とします。表現力豊かな仕様を満たすことは複雑であり、それにとらわれすぎてプログラムを完成させることができなくなる危険性があります。その一方で、このプロセスによって新たな理解につながることもあり、それは洗練された型として表現することができます。この章は依存型プログラミングの表層を掬うだけにとどまりますが、このトピックは実に奥が深く、それだけで1冊の本を出版するに値するものです。