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を例に考えます。

	trait Monoid[M] {
	type Zero <: M
	type Append[A <: M, B <: M] <: M
	def zero: Zero
	def append[A <: M, B <: M](a1: A, a2: B): Append[A, B]
	}

view raw monoid1.scala hosted with ❤ by GitHub

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

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

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

これをScalaで記述すると

	trait Monoid[M] extends MonoidLow[M] {
	type Zero <: M
	type Append[A <: M, B <: M] <: M
	def zero: Zero
	def append[A <: M, B <: M](a1: A, a2: B): Append[A, B]
	}
	trait MonoidLow[M] { self: Monoid[M] =>
	def leftIdentity[A <: M](a: Append[Zero, A]): A
	def rightIdentity[A <: M](a: Append[A, Zero]): A
	def associativity[A <: M, B <: M, C <: M](a: Append[A, Append[B, C]]): Append[Append[A, B], C]
	}

view raw monoid2.scala hosted with ❤ by GitHub

となります。

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

自然数を定義します。

	sealed trait Nat {
	type +[N <: Nat] <: Nat
	def +[N <: Nat](n: N): +[N]
	}
	sealed trait _0 extends Nat {
	type +[N <: Nat] = N
	def +[N <: Nat](n: N) = n
	}
	case object _0 extends _0
	case class S[N <: Nat](n: N) extends Nat {
	type +[M <: Nat] = S[N# + [M]]
	def +[M <: Nat](m: M) = S(n + m)
	}

view raw monoid3.scala hosted with ❤ by GitHub

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

	object NatInstance extends Monoid[Nat] {
	type Zero = _0
	type Append[A <: Nat, B <: Nat] = A# + [B]
	def zero = _0
	def append[A <: Nat, B <: Nat](a: A, b: B) = a + b
	def leftIdentity[A <: Nat](a: Append[Zero, A]) = a
	implicit def rightIdentity[A <: Nat](a: Append[A, Zero]) = a
	implicit def associativity[A <: Nat, B <: Nat, C <: Nat](a: Append[A, Append[B, C]]) = a
	}

view raw monoid4.scala hosted with ❤ by GitHub

コンパイル通ったー！

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

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

	sealed trait Pos {
	type +[P <: Pos] <: Pos
	def +[P <: Pos](p: P): +[P]
	}
	sealed trait _1 extends Pos {
	type +[P <: Pos] = S[P]
	def +[P <: Pos](p: P) = S(p)
	}
	case object _1 extends _1
	case class S[P <: Pos](p: P) extends Pos {
	type +[Q <: Pos] = S[P# + [Q]]
	def +[Q <: Pos](q: Q) = S(p + q)
	}
	object PosInstance extends Monoid[Pos] {
	type Zero = _1
	type Append[A <: Pos, B <: Pos] = A# + [B]
	def zero = _1
	def append[A <: Pos, B <: Pos](a: A, b: B) = a + b
	def leftIdentity[A <: Pos](a: Append[Zero, A]) = a
	implicit def rightIdentity[A <: Pos](a: Append[A, Zero]) = a
	implicit def associativity[A <: Pos, B <: Pos, C <: Pos](a: Append[A, Append[B, C]]) = a
	}

view raw monoid5.scala hosted with ❤ by GitHub

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

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

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

※追記

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

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

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