OCamlから学ぶCoq
| 1 |
逆に、Coqに慣れると、OCamlのプログラムが楽々かけるようになるだろう。
今日は、OCamlの視点からCoqの中身を見てみよう。
基本型
OCamlのint型は、CoqのZ型、などのように、OCamlの基本型に対応する型はだいたいCoqにもある。
| OCaml | Coq |
| int | Z |
| string | string（△） |
| bool | bool |
| unit | unit |
ただし、Coqの数字は上限および下限が無く、整数ならどんな大きな数もZ型の数字として扱うことができる。
本当に整数全体の集合なのだ。
stringに関しては、 Coqでは8bitのアスキー文字のリストで表現されているのでOCamlのそれとは全然違うのに注意しよう。
boolは同じと思ってよいだろう。CoqでもOCamlと同じように、trueとfalseの二つの元を持っている。
unitに関してはCoqでもOCamlと同じようなものだが、その元は()ではなくttで表される。
Coqのunit型に関しては謎が多く、私はまだ何のためにあるか理解していない。OCamlではprint関数などの副作用などを伴う関数の返り値に意味を持たせない場合にunit型を使ったりするが、Coqは純粋関数型言語なので副作用が存在しない。もっというと、任意の型Aから、unit型への関数は、ただ一つしか存在せず、たいした意味をもたない。(そういう意味でunit型はterminal objectである。)
宣言文、無名関数
letやtypeなどの宣言文は、昔いったように、だいたい対応がつく。
| OCaml | Coq |
| let | Definition |
| let rec | Fixpoint |
| type | Inductive |
無名関数に関してはOCamlと非常によく似ている。
ただ、普通の矢印は述語の「ならば」を記述するのに使ってるので、Coqでは二重線矢印を使って次のように書く。
Definition f := (fun (x:nat) => x+1).
マッチ文、イフ文
CoqではOCamlと同様のif文が用意されている。if ブール式 then なになに else ほげほげ のように記述する。ただちょっと違うところは、OCamlのようにelse ほげほげ の部分は省略できないということだろう。ただ、CoqではOCamlほどbool式を使わないので、あまり使わない。
Coqのマッチはたくさん入れ子になる可能性を考えて必ずendでおわるようになっている。また、矢印もOCamlとは違いに二重線の矢印になってることに気をつけよう。よく似てて、違う部分なので、OCamlを知っている人は最初、しょっちゅう書き間違えたりするかもしれない。
組、リスト、配列
組はOCamlと同じように(bunbun, banban)のようにカッコとコンマで表される。そのときの型もOCamlと同じように A * B と記述される。もちろん、OCamlと同じように、カッコを省略することもできる。
タプルの例
Variable b:bool. Fixpoint f (n:nat) := match n, b with | O, true => Bunbun | O, false => Banban | S p, _ => f p end.
CoqでのリストはOCamlのリストと構造は同じであるが、OCamlのように四角カッコを使って [1; 2; 5]などというふうにはかけない。
空リストはnil, コンスは hd :: tl または cons hd tl のように表される。また型の記述もOCamlなら、string list のように左側に型をかくが、Coqではlist string のように右側に書く。Coqではlistなどの型から型を作るものも関数と同じように扱われる。
配列はCoqにはない。
しかし、Coqは非常に表現力が高く、長さnのリスト型や、nこのノードを持つツリー型などを定義できるので、配列みたいなものを厳密に扱うことができる。ただもちろん、値をほかの値で書き換えるなどといったことはできない。あたりまえだ。
