Subscribed unsubscribe Subscribe Subscribe

プログラミングCoqの2章をHaskellに翻訳してみた

Haskell Coq

皆さん、小悪魔CoqチュートリアルことプログラミングCoq読んでいますか?僕は大変楽しく読ませていただいています。今日第2章にあたるProof-editing mode であそぼうが公開されました。今回はCoqの証明支援の側面がよくわかる章になっていて興味深いのですが、扱っている命題はまだ簡単で、Haskellでも十分表現できそうです。

というわけでHaskellに翻訳してみました。

今回、Haskellの拡張をいくつか使っています。

  • Coqの表記と対応関係を取るためにExplicitForAll(Rank2Typesで自動的に有効になる)
  • prop1で、forall付きの型を引数に取る関数の型を表現するためにRank2Types
  • orとandを表す型を演算子で表すためにTypeOperators

こうしてみてみると、Coqが自動的に作った仮定がHaskellにおける仮引数に対応づけられていることがよくわかります。面白いですね。今後はHaskell(というかGHC)の型システムで表現できない命題が出てくると思われます。楽しみです。