実は、前回書いたtype class in coqの記事、ちょっと怖いことがある。 このコードを実行すると、メモリを消費したあげくに落ちる。 Check (Compile (CEConst 1)).もちろんEval computeやEval simplでも同様。 なぜかはよくわからないが、まともにCompileの計…

これから、本当にほとんどの人には興味が向かないような、その上わけがわからない記事を書く。 なので、CoqやHaskellが好きな方以外はあまり見ないことをお勧めしておきたい。 ・・・などと、こんな記事を書いて自分も何をしたいのやら。

なぜ一度で出来なかったか？ 計画性がないからさ。 さて、ではType classで先ほどの流れをもう一度作ろう。 しかし、先ほどの定義とは、様々な点で異なるので注意。 Class Exp := { Eval : nat }. Instance EConst (n : nat) : Exp := { Eval := n }. Instan…

Coq8.2からType classが導入された。 もともとType classはHaskellにあったものである。 よって、Expression problemもHaskellからやり始めるのが楽である。 だが、私は残念ながらHaskellの世界の住人ではないので、Haskellによる解決に関しては私がこれをや…