Even/odd addition proof in scala

evenodd.scala

// See https://brianmckenna.org/blog/evenodd_agda_idris_haskell_scala

sealed trait Nat
trait Z extends Nat
case object Z extends Z
case class S[N <: Nat](n: N) extends Nat

sealed trait Even[N <: Nat]
trait EvenZ extends Even[Z]
case object EvenZ extends EvenZ
case class EvenS[N <: Nat](n: Even[N]) extends Even[S[S[N]]]

object Even {
  implicit val evenZ = EvenZ
  implicit def evenS[N <: Nat](implicit even: Even[N]) = EvenS[N](even)
}

sealed trait Odd[N <: Nat]
trait Odd1 extends Odd[S[Z]]
case object Odd1 extends Odd1
case class OddS[N <: Nat](n: Odd[N]) extends Odd[S[S[N]]]

object Odd {
  implicit val odd1 = Odd1
  implicit def oddS[N <: Nat](implicit odd: Odd[N]) = OddS[N](odd)
}

sealed trait Plus[N <: Nat, M <: Nat] {
  type Result <: Nat
}

object Plus {
  type Aux[N <: Nat, M <: Nat, R <: Nat] = Plus[M, N] {
    type Result = R
  }

  implicit def plusZ[M <: Nat] = new Plus[Z, M] {
    type Result = M
  }

  implicit def plusS[N <: Nat, M <: Nat](implicit plus: Plus[N, S[M]]) = new Plus[S[N], M] {
    type Result = plus.Result
  }
}

trait Show[A] {
  def show(a: A): String
}

object Show {
  implicit def showToInt[A](implicit toIntA: ToInt[A]): Show[A] = new Show[A] {
    def show(a: A): String = toIntA.toInt.toString
  }
}

trait ToInt[A] {
  def toInt: Int
}

object ToInt {
  implicit object ToIntZ extends ToInt[Z] {
    val toInt = 0
  }

  implicit def toIntS[N <: Nat](implicit in: ToInt[N]): ToInt[S[N]] = new ToInt[S[N]] {
    val toInt = 1 + in.toInt
  }

  implicit def toIntEven[N <: Nat](implicit in: ToInt[N]): ToInt[Even[N]] = new ToInt[Even[N]] {
    val toInt = in.toInt
  }

  implicit def toIntOdd[N <: Nat](implicit in: ToInt[N]): ToInt[Odd[N]] = new ToInt[Odd[N]] {
    val toInt = in.toInt
  }
}

trait ToNat[A] {
  def toNat(a: A): Nat
}

object ToNat {
  implicit object ToNatInt extends ToNat[Int] {
    def toNat(i: Int): Nat =
      if (i < 1) Z else S(toNat(i - 1))
  }
}

object ee {
  def apply[N <: Nat, M <: Nat, R <: Nat](n: Even[N], m: Even[M])(implicit sum: Plus.Aux[N, M, R], re: Even[R]) = re
}

object oo {
  def apply[N <: Nat, M <: Nat, R <: Nat](n: Odd[N], m: Odd[M])(implicit sum: Plus.Aux[N, M, R], re: Even[R]) = re
}

object eo {
  def apply[N <: Nat, M <: Nat, R <: Nat](n: Even[N], m: Odd[M])(implicit sum: Plus.Aux[N, M, R], re: Odd[R]) = re
}

object oe {
  def apply[N <: Nat, M <: Nat, R <: Nat](n: Odd[N], m: Even[M])(implicit sum: Plus.Aux[N, M, R], re: Odd[R]) = re
}

object Main {
  def putStrLn[A](a: A)(implicit show: Show[A]): Unit =
    println(show.show(a))

  def main(args: Array[String]): Unit = {
    putStrLn(oo(Odd1, Odd1))
    putStrLn(ee(EvenZ, EvenS(EvenS(EvenZ))))
    putStrLn(oe(OddS(Odd1), EvenZ))
    putStrLn(eo(EvenS(EvenZ), Odd1))
  }
}