Scala Type Level Programming: The Natural Numbers: First Definitions

type-level-programming-natural-numbers-first-definitions.scala

sealed trait Nat {
  type inc <: Nat
  type dbl <: Nat
}

sealed trait MsbZero extends Nat {
  override type inc = MsbOne
  override type dbl = MsbZero
}

sealed trait MsbOne extends Nat {
  override type inc = B0[MsbOne]
  override type dbl = B0[MsbOne]
}

sealed trait B0[HigherBits <: Nat] extends Nat {
  override type inc = B1[HigherBits]
  override type dbl = B0[B0[HigherBits]]
}

sealed trait B1[HigherBits <: Nat] extends Nat {
  override type inc = B0[HigherBits#inc]
  override type dbl = B0[B1[HigherBits]]
}