Scala Type Level Programming: The Natural Numbers: Addition

type-level-programming-natural-numbers-addition.scala

sealed trait Nat {
  type half <: Nat
  type add[That <: Nat] <: Nat
  // TODO: Better name
  type coreT[That <: Nat] <: Nat
}

sealed trait MsbZero extends Nat {
  override type half = MsbZero
  override type add[That <: Nat] = That
  override type coreT[That <: Nat] = B0[That]
}

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

sealed trait B0[HigherBits <: Nat] extends Nat {
  override type half = HigherBits
  override type add[That <: Nat] = That#coreT[That#half#add[HigherBits]]
  override type coreT[That <: Nat] = B0[That]
}

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