安全かつ柔軟な依存型 -この記事はTheorem Proving Advent Calendar 2011の1日目の記事です。 今日は Agda2 というプログラミング言語を用いて、依存型を用いることで絶対的な安全性と Haskell や OCaml などでは(通常の方法では)実現できない柔軟さのどちらも持つプログラムを記述できるということについて書きます。 この記事は主に、普段動的型付けのプログラミング言語を使っていて、静的型付きの言語では自分の意図したものを十分に表現できないと考えている人を対象読者としています。 依存型とは 型に依存する型や、値に依存する型を作れる型のことです。 例えば、値に依存する型を用いることで型レベルでサイズが与えられているリストを作ることが可能です。 また、リストの結合関数は長さ a のリストと長さ b のリストを取り、リスト a+b のリストを返すというような型を持つことになります
