表明から証明へ
表明とテスト
バグの原因のひとつとして、プログラム実行時に守るべき条件が守られていないことが挙げられるだろう。プログラムが一体どのような場合に正常に動作し、どのような場合に望まない結果をもたらすのかが分かっていなければ、バグのないプログラムは作れない。
言語の中には、表明という形でプログラムの条件を記述できるものがある。表明はプログラムの仕様をより明確にするし、誤った形でプログラムが使われた場合、バグはプログラムが不可解な挙動を引き起こす前に検出できるだろう。
表明という手法には限界がある。条件が満たされているかを調べるだけなので、すべての条件が決まるまではプログラムの正しさが確認できないのだ。結局、実行時まで決定できない条件がある場合には、プログラムの正しさを保証するために多くのテストケースを用意し、テストを行わなければならない。
証明
単にプログラム実行時に守るべき条件を記すだけではなく、それが実行時には必ず守られていることを証明することができれば、テストを行わずともプログラムの正しさを保証できるだろう。しかし、どのように証明を行えば良いのだろうか? 実は、カリー゠ハワード同型対応というものがあって、計算モデルと証明の間には対応関係があることが知られている。噛み砕いて言えば、今まで「型」だと思っていたものを「命題」、「プログラム」だと思っていたものを「証明」と読み替えることができる。
全域函数
多くの言語で「函数」と呼ばれるものは、実際には部分函数であることが多い。そういう言語では、引数に正しい型の値を渡していても、結果が定まっていない場合があって、例えば不適切な値を返したり、無限ループに陥ったり、例外を投げたりする。全域函数であれば、正しい型の値を渡せば、必ず正しい値がひとつ返ってくる。
Idrisでは、函数が全域函数であるかどうかを調べることができる。
foo : a -> Maybe a foo x = Just x bar : Maybe a -> a bar (Just x) = x baz : Bool -> () baz False = () baz True = baz True
函数 foo, bar, baz はどれも型チェックが通る。しかし、 bar と baz は全域函数ではない。
idris total.idr を実行して、REPLからコマンドを入力することで、全域函数ではないことを確認できる。
*total> :total foo Total *total> :total bar not total as there are missing cases *total> :total baz possibly not total due to recursive path baz --> baz
bar では、足りないケースがあることによって全域函数ではなくなっている。baz では、再帰的な呼び出しのせいで全域函数ではなくなっている。
全域函数であるか、部分函数であるかは、明示的に宣言できる。
total foo : a -> Maybe a foo x = Just x partial bar : Maybe a -> a bar (Just x) = x partial baz : Bool -> () baz False = () baz True = baz True
totalという宣言にも関わらず部分函数である場合には、エラーとなる。
なにも指定しない場合はデフォルトで partial だが、%default totalという行を先に書くことで、デフォルトを total にできる。
