契約と型検査

#PL #tech #alcohol

プログラミングの型検査・契約・テストについて書きます。お酒を飲みながら書きました。注意は払ったつもりですが、変なところがあるかもしれません。

契約 (contract) とはプラグラムの関数の入出力に関する規約のことです。例えば整数の割り算をする div 関数は、二つの整数を受け取って商を返す関数だとしましょう。このとき、入力の二つの値は

  1. どちらも整数
  2. 二つ目の整数は0ではない

ことが求められます。また、整数の割り算を行なっているので、div(a,b) の値は例えば

  1. a の絶対値以下であること

が求められます（もっと細かい要求をしても良いでしょうが）。箇条書きで示したような div 関数について求められる性質のことを契約とよぶことが多いです。

ここまでで例を示しました。例のことは忘れて一旦抽象的な定義を試みましょう。契約は関数を呼び出す側と呼ばれる定義の間の約束事です。関数を正しく呼べば正しい結果を返すことを規定します。どんな呼び出しが正しくて、正しい呼び出しをされたと仮定とした上でどんな結果が正しいかを規定するのが契約です。

先ほどの例を考えると、 div 関数の第二引数に0を渡すのは呼び出し側の契約違反で、div(168,4) の結果が42にならないのは関数定義の契約違反です。契約は、関数呼び出しにおける呼び出し側と定義側との間の規約を表明し、検査します。

多くの言語でコードを書く際は、関数の冒頭で引数のチェックをして、呼び出し側の責任を追及するスタイルでコードを書くことになりがちです。言語によっては組み込みの機能でいい感じに契約を書いて、実行時に検査できます。 D言語とかRacketがいい例です。

例えばRacketだと、モジュールでエクスポートする関数を表明する箇所で、関数の契約を書きます。完全に雰囲気ですが、おそらくこんな感じで書くんじゃないかったかと思います。正確にはRacket GuideかRacket Referenceをご覧ください。

#lang racket

(export
  (div (-> (and int (lambda (x) (< 0 x) )) int  int)))

...

(define (div a b)
  (/ a b))

契約を書いておくと何が嬉しいでしょうか。問題の切り分けが楽になることが嬉しいですね。Blame shiftingができます。みなさん人生で一回は Segmentation fault とか Null pointer exception とか car: cannot apply for nil みたなエラーに遭遇したことがあるかと思います。これらのエラーは契約をちゃんと関数に書いていないから起きるはずで、まともなライブラリを使っていればあまりみないはずです。これらのエラーが出たときには割と深く絶望して、どの関数が悪さをしているか探す旅が始まります。

もし真面目に契約を書いていれば関数が許さないnilを受け取った時点で呼び出し側に責任があることを即座にエラーを起こしたり、変な結果を返しそうになったら返す直前に同様にエラーを起こします。

これが契約の嬉しさです。反対に、関数を動かして契約違反で怒られない限り、その契約を実装が遵守していることが保証されます。これもまた契約の嬉しさの一つです。契約はプロダクション環境で生きているドキュメントとして機能します。

テストとの違いは、契約は実行時に検査をすることが大きいでしょう。テストはテストを走らせるときにしか検証を行いませんが、契約は実行時にも検査を行います。プロダクション環境で関数を呼び出すときにも契約は検査されるのです。

契約はいいものであることがわかったと思います。関数定義の性質を保証して、何かあればすぐに検出し、何もなければ、すべてのそれまでの実行で違反したケースがないことを保証します。

この観点で見たときに、型検査はテストよりも契約に近しい存在だと言えるでしょう。型検査は、コンパイルのたびに型制約が満たされていることを検証します。健全な（まともな）型システムでは、型検査をパスしたプログラムは実行時に型エラーを起こさないことが保証されます （この保証がある型システムのことを健全だというので順番は逆ですが）。型検査では、関数の入力として渡される値が、関数が期待する条件を満たすことを検査しますし、関数が返す値が宣言にあっていることも検査します。契約と対比させると、契約は実行時に検査を行う一方で、型検査はコンパイル時に行うという感じです。

逆にいうと、契約は型検査で静的にやろうとする検査を実行時まで遅延したものです。実行時には任意の計算をできるので表現力は契約の方が高いです。例えば引数の値が10と20の間である、みたいなことを検査するのは型検査では大変ですが、契約ならちょちょいのちょいです。

じゃあ契約だけでいいじゃないか、型検査なんてやめてしまえ！という話になるかというと、そういうわけにもいきません。型検査には契約にないよさがあります。

型検査の良さは静的に検証が済むことにあります。つまり、以下の二つを型検査は満たします

  1. 全ての実行について、検証結果が成立する
  2. プログラムを実行しないでも検証を行える

まず一つ目について。契約やテストでは、実行した場合については動作を検証してくれますが、それとは違う値については特に保証をしてくれません。だから境界テストみたいな、人間が上手に動かす技法が使われるのでしょう。型検査では、ある程度検証内容を抽象的にしたり保守的にすることで、全ての実行に対する性質を保証します。 intが返る関数は決してfloatを返さないことを型検査では保証できます。

抽象化や保守的な検査を行う二つ目の恩恵として、実行しないでも検証できることが挙げられます。本番環境で動かさないとわからなかったり、テスト環境をせっせと用意する必要は、型検査では生じません。

型検査や契約の有用性を主張してきましたが、それでもテストは必要です。実際に色々な具体的なケースで動かすことでわかることは多いでしょう。型検査は動かさないでもわかることを検証して、契約は動かしたらわかることを検証します。テストはプログラムを動かしてみて検証します。型や契約だけではプログラムを動かすことはありません。そこが大きな違いなはずです。

それでも全ての異常の検知をテストでまかなう必要もないはずです。契約や型検査は保証をする仕組みとして優秀です。基本的な保証は契約や型検査で済ませて、本当に際どいところをテストでカバーする、みたいな役割分担をすると幸せになれるんじゃないでしょうか。