CoqのType classでExpression problemに挑戦する その2
なぜ一度で出来なかったか？
計画性がないからさ。
さて、ではType classで先ほどの流れをもう一度作ろう。
しかし、先ほどの定義とは、様々な点で異なるので注意。
Class Exp := { Eval : nat }.
Instance EConst (n : nat) : Exp := { Eval := n }.
Instance EAdd (e1 e2 : Exp) : Exp :=
{ Eval := let (n1) := e1 in let (n2) := e2 in n2 + n1 }.式の定義がEvalによって特徴付けられている。
つまり、式とはある種のインターフェースでしかない。
では次に、スタックマシンの定義に入る。
Require Import List.
Class Word := { Exe : list nat -> option (list nat) }.
Instance WPush (n : nat) : Word := { Exe s := Some (n :: s) }.
Instance WPlus : Word :=
{ Exe s := match s with
| n1 :: n2 :: s' => Some (n2 + n1 :: s')
| _ => None
end }.
Fixpoint Execute (p : list Word) s :=
match p with
| nil => match s with | n :: nil => Some n | _ => None end
| w :: p' =>
match Exe s with
| None => None
| Some s' => Execute p' s'
end
end.命令はExeという名前のスタックマシンの状態遷移で定義されている。
また、Executeは再び関数として定義されている。
ではコンパイラの定義に・・・といいたいところだが、ここで少しばかり問題が生じる。
コンパイラは、どうしてもEConstやEAddの引数が見えなければ作れない。
しかし、Expを扱う関数からはこれらの引数が見えない。
このままでは、作れないことになる。
これは、CoqのType classとHaskellのType classの大きな差である。
Haskellの関数定義は元々開いている。
開いている、とはここでは定義のなかにデータ型の展開を直接書かないという意味だが、これは新たなインスタンスが出来た場合でも、そのインスタンス用の関数として定義すればいいことを意味している。
簡単に言えば、どんなときに関数を定義するときでもいつでも引数が見えている、ということだ。
一方、Coqの関数定義は閉じている。
関数の定義中に引数が必要になれば、必ず型を展開するように記述しなければならないため、結果としてインターフェースだけしかないType classでは新たな関数が定義できない。
このため、CoqのType classは演算子の追加などには強いものの、関数の追加に弱いわけである*1。
これを解決することが出来ないのか、と言えば一応別の策がある。
Classを継承するように使えばいいわけである。
次のコードがそんな感じのもの。
Class CompExp := { E :> Exp ; Compile : list Word }.
Instance CEConst n : CompExp := { E := EConst n ; Compile := WPush n :: nil }.さて、新たに作ったCompile付きの式は、内部にExpを持っている。
これを使えば今までの定義も使いまわせる、というわけである。
・・・え？足し算はどこに消えたのか？
そんなに見たいのですか、そうですか・・・
私が書いたコードは、次のようになっている。
Instance CEAdd (e1 e2 : CompExp) : CompExp. destruct e1; destruct e2; constructor. destruct E0; destruct E1; constructor. apply (plus Eval0 Eval1). apply (app Compile0 (app Compile1 (WPlus :: nil))). Defined.
なぜProofモードで作っているか、と？
それはこのインスタンスの定義が何度も展開を繰り返すからだ*2。
今度は証明をしなければならないが、証明はEvalの結果とCompileの結果出てくる命令列を用いなければ出来ない。
つまり、また継承である。
もう面倒なので定数までにしておく。
Class CertCompExp := { CE :> CompExp ; Verify : forall p s, Execute (Compile++p) s = Execute p (Eval :: s) }.
Instance CCEConst (n : nat) : CertCompExp := { CE := CEConst n }.
auto.
Qed.
では、通常のデータ型で難しかった演算子の追加をやってみる。
ここでは掛け算だが、いたって簡単である。
Instance EMult (e1 e2 : Exp) : Exp :=
{ Eval := let (n1) := e1 in let (n2) := e2 in n1 * n2 }.
Instance WTimes : Word :=
{ Exe s := match s with
| n1 :: n2 :: s' => Some (n2 * n1 :: s')
| _ => None
end }.
Instance CEMult (e1 e2 : CompExp) : CompExp.
...というわけで、後は足し算同様に行えば出来るわけである。
たしかに元々あるコードに何もしていないので、その意味ではうまくいっている。
関数を追加するのも、確かに元のコードには一切手を出してない。
なんとも七面倒なコードであるわけだが。
HaskellのType classについて、ボイラープレートが多いという記述をmaoeさんがしていたが、Coqはその比じゃないような・・・
まあ、Coqに以前からあった要素で構築したものなので、かなり無理やりで仕方ないといえば仕方ないのだが。
今回のように検証に用いる場合に、最も困る点はそこではなくて・・・
全ての構成要素について継承で列挙しなおさないと検証にならないし、誰も全ての式について保証してくれないことである。
各インスタンスでは確かに正しいのだが、ほしい式全体は正しくそこにエンコードされたのだろうか？誰か追加したものを忘れてはいないだろうか？
そんな疑心暗鬼に陥りそうな、CoqのType classでありましたとさ。
あー長かった。
