ソフトウェアの基礎、継続中

ソフトウェアの基礎、115ページまで。

演習問題はoptional,recommendedであるものはやってません。

多相性の部分はXをどこに置くのかはっきり理解しておらず、コンパイルエラーが起きているので後回しに。先に高階関数のほうに進みます。

いずれは証明駆動開発をしてみたいので、ためしにExtractionコマンドを使ってみた。
fanc関数をHaskellに変換する場合は、

Extraction Language Haskell.
Extract Inductive list => "()" ["" "(:)"].
Extract Inductive bool => "Bool" ["True" "False"].
Extract Inductive nat => Int ["0" "succ"] "(\fO fS n -> if n == 0 then fO () else fS (n-1))".

Extraction "foo.hs" fanc

しかし、
Extract Inductive nat => Int ["0" "succ"] "(\fO fS n -> if n == 0 then fO () else fS (n-1))".
の部分でなぜかコンパイルが通らない。謎。

ググってみても、CoqからHaskellへのに関する日本語のページが少なすぎる。英語読まなきゃだめか？

この部分をコメントアウトすると変換は一応できるが、HaskellのInt型ではなくて(Coqのような)Nat型になってしまう。

時間ばかり食うので、Haskellへの変換は後回しにすることにした。

TAPL
まったく進んでない...

明日からサークルの合宿です。移動時間が片道2時間だから、TAPL持っていって読もうかな