Scala Type Level Programming: The Natural Numbers

type-level-programming-natural-numbers.scala

sealed trait MsbZero extends Nat {
  override type inc = MsbOne
  override type dbl = MsbZero
  override type half = MsbZero
  override type add[That <: Nat] = That
  override type coreT[That <: Nat] = B0[That]
  override type mult[That <: Nat] = MsbZero
  override type exp[That <: Nat] = MsbZero
  override type expflip[That <: Nat] = MsbOne
}

sealed trait MsbOne extends Nat {
  override type inc = B0[MsbOne]
  override type dbl = B0[MsbOne]
  override type half = MsbZero
  override type add[That <: Nat] = That#inc
  override type coreT[That <: Nat] = B1[That]
  override type mult[That <: Nat] = That
  override type exp[That <: Nat] = MsbOne
  override type expflip[That <: Nat] = That
}

sealed trait B0[HigherBits <: Nat] extends Nat {
  override type inc = B1[HigherBits]
  override type dbl = B0[B0[HigherBits]]
  override type half = HigherBits
  override type add[That <: Nat] = That#coreT[That#half#add[HigherBits]]
  override type coreT[That <: Nat] = B0[That]
  override type mult[That <: Nat] = HigherBits#mult[That]#dbl
  override type exp[That <: Nat] = That#expflip[B0[HigherBits]]
  override type expflip[That <: Nat] = HigherBits#expflip[That#mult[That]]
}

sealed trait B1[HigherBits <: Nat] extends Nat {
  override type inc = B0[HigherBits#inc]
  override type dbl = B0[B1[HigherBits]]
  override type half = HigherBits
  override type add[That <: Nat] = That#inc#coreT[That#inc#half#add[HigherBits]]
  override type coreT[That <: Nat] = B1[That]
  override type mult[That <: Nat] = HigherBits#mult[That]#dbl#add[That]
  override type exp[That <: Nat] = That#expflip[B1[HigherBits]]
  override type expflip[That <: Nat] = HigherBits#expflip[That#mult[That]]#mult[That]
}