Proof with Scala

※今回はScala2.10.0-M3を使います。

ある型クラスのインスタンスを定義するとき、何らかの規則を満たす必要があるときがあります。

例えばMonadだとモナド則。
bind,returnを定義するときに、以下のものが満たされないといけません。

bind (return a) f = f a
bind m return = m
bind (bind m f) g = bind m (fun x => bind (f x) g)

しかし、Scalazの型クラスなどはモナド則を満たしているかどうかを検査してくれるわけではありません。

そこで、コンパイル時に規則を満たしているかどうかを検査するように型クラスを定義してみます。

Monoidを例に考えます。


ScalazのMonoidの定義と違うところは、ある型のサブクラスも許容しているところです。

Monoidは以下のものを満たす必要があります。

append zero a = a
append a zero = a
append a (append b c) = append (append a b) c

これをScalaで記述すると


となります。

型が命題でプログラムが証明になります。
つまり、leftIdentity,rightIdentity,associativityを定義出来れば証明できたことになります。
カリー=ハワード同型対応！

自然数を定義します。


自然数をMonoidのインスタンスにします。


コンパイル通ったー！

通らない例を作ってみましょう。

正の整数を定義して、Monoidのインスタンスを考えてみます。


この定義では当然コンパイルは通りませんね。

コンパイルが通るように定義することも多分できないと思われます。（asInstanceOfは使っちゃダメですよ。）

これらのコードを書いてる中で疑問が現れました。
NatInstanceのrightIdentityとassociativityです。
このコード、コンパイルは通らないと思っていたのですが、implicitを付けると通りました。
・・・・・なぜ？

※追記

@halcat0x15a こういうこと？ gist.github.com/2908064

— Kenji Yoshidaさん (@xuwei_k) 6月 11, 2012

なんだか型推論に失敗してNothingを入れられちゃってるみたい？
下限境界は制限しようがないし、やはりScalaで証明は難しいということですね・・・・・
結論：Coqとか使いましょう。