OCamlとCoqを連携してIO処理をモナディックに扱う

この記事は OCaml Advent Calendar の5日目の記事です。

OCamlと連携して、CoqでもIO処理ができるようにするためのライブラリを作った。
http://github.com/yoshihiro503/coqio

このライブラリを使えば、例えば次のようなコードを書くことができる。

Require Import Monad IO.
Open Scope string_scope.

Definition main : IO unit :=
  do _ <- print "Hello"
  ; println ", world!".

Haskell風のdo式みたいな記法が便利だね。print関数には文字列だけでなく、Showクラスのインスタンスとなる型を持つ式ならばなんでも与えることができる*1。

このコードを次のコマンドでExtractすればcoq.mlというOCamlのソースを得ることができる。

Require Import ExtrOcamlBasic ExtrOcamlString ExtrOcamlIO Hello.

Extraction "coq.ml" main.

これで、あとはOCamlでコンパイルすれば実行できる。

  $ ocamlc coq.ml
  $ ./a.out
Hello, world!

*1:Showクラスの実装についてはhttp://qiita.com/items/a6fe93ae0d867129f7b1