Coqで依存型

最近Agdaがはやっているみたいなので、Coqでも依存型（dependent type）を使ってみた。 実装したのは長さ n のベクトル型だ。このベクトル型を使うと、空でないとか、長さが等しいとかを型の段階で保証できるので、より安全なプログラムを書くことができるのだ。

Variable A:Set.
Inductive Vec : nat -> Set :=
  | VNil : Vec O
  | VCons : forall n, A -> Vec n -> Vec (S n).

このベクトル型を使えば、コンパイル時に長さの整合性もチェックしてくれて、間違いがある場所を教えてくれる。コンパイルさえ通れば、OutOfBoundsExceptionのような実行時エラーは起こりえないことが保証される。
例えば、一般的にリストのhead関数は、引数が1以上の長さのときのみ定義でき、空リストの場合には値を返すことができない。しかし、このベクトル型を使えば、1以上の長さのリストのみで定義される安全なhead関数を作ることができる。

Definition head n : Vec (S n) -> A.
 intros n H; inversion H as [| m x _]. exact x.
Defined.

*1
さらに、ベクトルの内積は同じ長さのベクトル同士でしか定義できないが、このような場合もベクトル型は便利だ。内積関数(inner_prod)を次のように実装することができる。

  Definition inner_prod n : Vec Z n -> Vec Z n -> Z.
   intro n; induction n; intros v w.
    exact 0.
    exact (head _ v * head _ w + IHn (tail _ v) (tail _ w)).
  Defined.

*2
また、ベクトルのベクトルとしてm行n列の行列型を作ることができる。

Definition Matrix m n : Set := Vec (Vec Z m) n.

行列のかけ算は一方の行数ともう一方の列数が等しいときのみに定義されるが、それは次のように実装できる。

  Definition mult_aux k m : Matrix k m -> Vec Z m -> Vec Z k.
   intros k m vs w; induction k.
    exact VNil.
    exact (VCons (inner_prod (map (head _) vs) w)
             (IHk (map (tail _) vs))).
  Defined.

  Definition mult k m n (vs:Matrix k m) (ws:Matrix m n) : Matrix k n :=
    map (mult_aux vs) ws.

OutOfBoundsExceptionやInvalid_argumentエラーなどの仕組みをうれしいと思う人はいないだろう。依存型のような強力な型システムを使うことによって、実行時のエラーを防ぐだけでなく、開発者がプログラムの本質の部分だけを考えることができるようになるのである。

依存型はCoqやAgdaの便利な性質の一部であり、他にもいろいろできるのだが、依存型に関しては、Agdaは非常にうまくできている気がした。

Agdaは楽しいのでもっと触ってみよう。

ソースコード

• vec.html
• vec.v

*1:このようにCoqでは、型だけまず宣言して、あとからtacticを使いながら関数を構成することができる。しかし、Agdaはもっとすごくて、
head : Vec A (succ p) -> A
head x::xs = x
のように、Haskellっぽく書くことができる。コンパイラが自動的に空リストの場合が必要ないことを証明しているようだ。Coqでもこんなかんじに関数っぽく書きたいのだが、今のところどうやるのかわからない。

*2:ここも、Agdaなら
inner_prod nil nil = 0
inner_prod (x::xs) (y::ys) = x*y + inner_prod xs ys
のようなかんじにできる！Agdaすごい!