Janek Bogucki janekdb

## type-level-programming-natural-numbers-exponentiation-assertions.scala
// 1^0
implicitly[T1#exp[T0] =:= T1]
// 1^1
implicitly[T1#exp[T1] =:= T1]
// 1^2
implicitly[T1#exp[T2] =:= T1]
// 1^3
implicitly[T1#exp[T3] =:= T1]

// 2^0

## type-level-programming-natural-numbers-exponentiation.scala
sealed trait Nat {
  type exp[That <: Nat] <: Nat
  type expflip[That <: Nat] <: Nat
}

sealed trait MsbZero extends Nat {
  override type exp[That <: Nat] = MsbZero
  override type expflip[That <: Nat] = MsbOne
}

## type-level-programming-natural-numbers-addition-assertions.scala
  // 0 + 0, 0 + 1
  implicitly[MsbZero#add[MsbZero] =:= MsbZero]
  implicitly[MsbZero#add[MsbOne] =:= MsbOne]

  // 1 + 0, 1 + 1
  implicitly[MsbOne#add[MsbZero] =:= MsbOne]
  implicitly[MsbOne#add[MsbOne] =:= B0[MsbOne]]

  // 2 + 0, 2 + 1, 2 + 2
  implicitly[B0[MsbOne]#add[MsbZero] =:= B0[MsbOne]]

## 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

## type-level-programming-natural-numbers-high-hex.scala
sealed trait Nat {
  type inc <: Nat
  type dbl <: Nat

  type A = this.type#dbl#inc#dbl#dbl#inc#dbl
  type B = this.type#dbl#inc#dbl#dbl#inc#dbl#inc
  type C = this.type#dbl#inc#dbl#inc#dbl#dbl
  type D = this.type#dbl#inc#dbl#inc#dbl#dbl#inc
  type E = this.type#dbl#inc#dbl#inc#dbl#inc#dbl
  type F = this.type#dbl#inc#dbl#inc#dbl#inc#dbl#inc

## type-level-programming-natural-numbers-first-assertions.scala
  // 1 = O + 1
  implicitly[MsbOne =:= MsbZero#inc]

  // 2 = O + 1 + 1
  implicitly[B0[MsbOne] =:= MsbZero#inc#inc]

  // 3 = O + 1 + 1 + 1
  implicitly[B1[MsbOne] =:= MsbZero#inc#inc#inc]

  // 4 = O + 1 + 1 + 1 +

## 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
}

## type-level-programming-natural-numbers-mult-example.scala
// 2 x 3 5 x 7 x 11 x 13 x 17 = 510510

type T510 = T5#mult[T10]#add[T1]#mult[T10]

type T510510 = T510#mult[T1000]#add[T510]

implicitly[T2#mult[T3]#mult[T5]#mult[T7]#mult[T11]#mult[T13]#mult[T17] =:= T510510]

## type-level-programming-natural-numbers-mult-assert.scala
  implicitly[MsbZero#mult[MsbZero] =:= MsbZero]
  implicitly[MsbZero#mult[MsbOne] =:= MsbZero]
  implicitly[MsbOne#mult[MsbZero] =:= MsbZero]
  implicitly[MsbOne#mult[MsbOne] =:= MsbOne]

  implicitly[T0#mult[T0] =:= T0]
  implicitly[T0#mult[T2] =:= T0]
  implicitly[T0#mult[T4] =:= T0]

  implicitly[T1#mult[T0] =:= T0]

## type-level-programming-natural-numbers-mult.scala
sealed trait Nat {
  type mult[That <: Nat] <: Nat
}

sealed trait MsbZero extends Nat {
  override type mult[That <: Nat] = MsbZero
}

sealed trait MsbOne extends Nat {
  override type mult[That <: Nat] = That
	// 1^0
	implicitly[T1#exp[T0] =:= T1]
	// 1^1
	implicitly[T1#exp[T1] =:= T1]
	// 1^2
	implicitly[T1#exp[T2] =:= T1]
	// 1^3
	implicitly[T1#exp[T3] =:= T1]

	// 2^0
	sealed trait Nat {
	type exp[That <: Nat] <: Nat
	type expflip[That <: Nat] <: Nat
	}

	sealed trait MsbZero extends Nat {
	override type exp[That <: Nat] = MsbZero
	override type expflip[That <: Nat] = MsbOne
	}
	// 0 + 0, 0 + 1
	implicitly[MsbZero#add[MsbZero] =:= MsbZero]
	implicitly[MsbZero#add[MsbOne] =:= MsbOne]

	// 1 + 0, 1 + 1
	implicitly[MsbOne#add[MsbZero] =:= MsbOne]
	implicitly[MsbOne#add[MsbOne] =:= B0[MsbOne]]

	// 2 + 0, 2 + 1, 2 + 2
	implicitly[B0[MsbOne]#add[MsbZero] =:= B0[MsbOne]]
	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
	sealed trait Nat {
	type inc <: Nat
	type dbl <: Nat

	type A = this.type#dbl#inc#dbl#dbl#inc#dbl
	type B = this.type#dbl#inc#dbl#dbl#inc#dbl#inc
	type C = this.type#dbl#inc#dbl#inc#dbl#dbl
	type D = this.type#dbl#inc#dbl#inc#dbl#dbl#inc
	type E = this.type#dbl#inc#dbl#inc#dbl#inc#dbl
	type F = this.type#dbl#inc#dbl#inc#dbl#inc#dbl#inc
	// 1 = O + 1
	implicitly[MsbOne =:= MsbZero#inc]

	// 2 = O + 1 + 1
	implicitly[B0[MsbOne] =:= MsbZero#inc#inc]

	// 3 = O + 1 + 1 + 1
	implicitly[B1[MsbOne] =:= MsbZero#inc#inc#inc]

	// 4 = O + 1 + 1 + 1 +
	// 2 x 3 5 x 7 x 11 x 13 x 17 = 510510

	type T510 = T5#mult[T10]#add[T1]#mult[T10]

	type T510510 = T510#mult[T1000]#add[T510]

	implicitly[T2#mult[T3]#mult[T5]#mult[T7]#mult[T11]#mult[T13]#mult[T17] =:= T510510]
	implicitly[MsbZero#mult[MsbZero] =:= MsbZero]
	implicitly[MsbZero#mult[MsbOne] =:= MsbZero]
	implicitly[MsbOne#mult[MsbZero] =:= MsbZero]
	implicitly[MsbOne#mult[MsbOne] =:= MsbOne]

	implicitly[T0#mult[T0] =:= T0]
	implicitly[T0#mult[T2] =:= T0]
	implicitly[T0#mult[T4] =:= T0]

	implicitly[T1#mult[T0] =:= T0]
	sealed trait Nat {
	type mult[That <: Nat] <: Nat
	}

	sealed trait MsbZero extends Nat {
	override type mult[That <: Nat] = MsbZero
	}

	sealed trait MsbOne extends Nat {
	override type mult[That <: Nat] = That