Playing with propositional equality in Scala (+inductive proof)

gistfile1.scala

import scala.language.higherKinds

/*
 * The usual peano numbers with addtion and multiplication  
 */
sealed trait Nat {
  type Plus[N <: Nat] <: Nat
  type Mult[N <: Nat] <: Nat
}

sealed trait Z extends Nat {
  type Plus[N <: Nat] = N
  type Mult[N <: Nat] = Z
}

sealed trait S[N <: Nat] extends Nat {
  type Plus[M <: Nat] = S[N#Plus[M]]
  type Mult[M <: Nat] = M#Plus[N#Mult[M]]
}

/*
 * Equality with an upper bound to tackle subtyping 
 */
sealed trait Eq[Up, A <: Up, B <: Up] {
  def cong[F[_ <: Up] <: Up] : Eq[Up, F[A], F[B]]
}

final case class refl[Up, A <: Up]() extends Eq[Up, A, A] {
  def cong[F[_ <: Up] <: Up]: Eq[Up, F[A], F[A]] = refl() 
}

/*
 * Prove that n + 0 = 0 + n 
 */
sealed trait Plus0[N <: Nat] {
  type Prop = Eq[Nat, N#Plus[Z], Z#Plus[N]]
  
  val proof: Prop
}

// case: 0
final case object Plus0_0 extends Plus0[Z] {
  val proof: Prop = refl()
}

//case: n + 1
final case class Plus0_S[N <: Nat](p: Plus0[N]) extends Plus0[S[N]] {
  val proof: Prop = p.proof.cong[S]
} 

Very nice!

I think you don't need the apply method in refl. It seems to just create a new instance with the same type parameters. Also, in method cong, you don't need the new.

I know, it's just my style to use new in that context ^^. The code is not meant to be perfect, it's just a demonstration. ;)

You are right about the apply method. I think I forgot to get rid of it after some experiments.

By the way, is it intentional that Eq doesn't have the following method (note the absence of the second <: Up)?

def subst[F[_ <: Up]]: F[A] => F[B]

Its implementation for refl is just Predef.identity, and the cong method can be derived from it like so:

final def cong[F[_ <: Up] <: Up]: Eq[Up, F[A], F[B]] = subst[({type l[a <: Up] = Eq[Up, F[A], F[a]]})#l](refl[Up, F[A]]())

You probably know this stuff, but I wanted to post it here anyway in case anybody is interested :)

Naturally, scalaz also has this sort of equality :)