Implementation of typelevel booleans and integers using type projections

baccata.scala

/**
 * Contains the cool alias for the operations
 */ 
package object baccata {

  type +[L <: Integer, R <: Integer] = L#add[R]
  type -[L <: Integer, R <: Integer] = L#sub[R]
  type *[L <: Integer, R <: Integer] = L#prod[R]
  type /[L <: Integer, R <: NonZeroInt] = L#div[R]
  type <[L <: Integer, R <: Integer] = L#lt[R]
  type <=[L <: Integer, R <: Integer] = L#lteq[R]
  type >[L <: Integer, R <: Integer] = R#lt[L]
  type >=[L <: Integer, R <: Integer] = R#lteq[L]
  type ==[L <: Integer, R <: Integer] = L#eq[R]
  type min[L <: Integer, R <: Integer] = (L < R)#branch[Integer, L, R]
  type minp[L <: NonNegInt, R <: NonNegInt] = (L < R)#branch[NonNegInt, L, R]

  type p1 = _0#succ
  type p2 = p1#succ
  type p3 = p2#succ
  type p4 = p3#succ
  type p5 = p4#succ
  type p6 = p5#succ
  type p7 = p6#succ
  type p8 = p7#succ
  type p9 = p8#succ

  type n1 = _0#pred
  type n2 = n1#pred
  type n3 = n2#pred
  type n4 = n3#pred
  type n5 = n4#pred
  type n6 = n5#pred
  type n7 = n6#pred
  type n8 = n7#pred
  type n9 = n8#pred

  // BoolOps:
  type ||[L <: Bool, R <: Bool] = L#or[R]
  type &&[L <: Bool, R <: Bool] = L#and[R]

}

Bool.scala

package baccata

/**
 * Inspired from Grant Beaty's Scunits
 */
trait Bool {
  type branch[B,T <: B, E <: B] <: B // typelevel if-then-else
  type not <: Bool
  type or[R <: Bool] <: Bool
  type and[R <: Bool] <: Bool
  type Xor[R <: Bool] <: Bool
}
trait True extends Bool {
  type not = False
  type branch[B,T <: B, E <: B] = T
  type or[R <: Bool] = True
  type and[R <: Bool] = R
  type Xor[R <: Bool] = R#not
}
trait False extends Bool {
  type not = True
  type branch[B,T <: B, E <: B] = E
  type or[R <: Bool] = R
  type and[R <: Bool] = False
  type Xor[R <: Bool] = R
}

Integer.scala

package baccata

/**
 * Inspired from Grant Beaty's Scunits
 */
sealed trait Integer {
  type N <: Integer
  type isZero <: Bool
  type isPos <: Bool
  type isNeg <: Bool
  type abs <: NonNegInt
  type sameSign[R <: Integer] = (isPos && R#isPos) || (isNeg && R#isNeg)

  type succ <: Integer
  type pred <: Integer

  type add[N <: Integer] <: Integer
  type sub[N <: Integer] <: Integer
  type prod[N <: Integer] <: Integer
  type div[N <: NonZeroInt] <: Integer

  type neg <: Integer

  type loop[B,F[_ <: B] <: B, Res <: B] <: B

  type lt[N <: Integer] = sub[N]#isNeg

  type lteq[N <: Integer] = ({
    type minus = sub[N]
    type res = minus#isNeg || minus#isZero
  })#res

  type eq[N <: Integer] = sub[N]#isZero
}
sealed trait NonNegInt extends Integer {
  type N <: NonNegInt
  type abs = N
  type isNeg = False
  type succ <: PosInt
  type neg <: NonPosInt
  type predNat <: NonNegInt
  type addNat[R <: NonNegInt] <: NonNegInt
  type subNat[R <: NonNegInt] <: NonNegInt
  type divNat[D <: PosInt] <: NonNegInt
}
sealed trait NonPosInt extends Integer {
  type N <: NonPosInt
  type isPos = False
  type pred <: NegInt
  type neg <: NonNegInt
  type loop[B,F[_ <: B] <: B, Res <: B] = Res
}
sealed trait NonZeroInt extends Integer {
  type N <: NonZeroInt
  type isZero = False
  type abs <: PosInt
  type div[R <: NonZeroInt] = ({
    type aRes = abs#divNat[R#abs]
    type result = sameSign[R]#branch[Integer, aRes, aRes#neg]
  })#result
}
sealed trait NegInt extends NonPosInt with NonZeroInt {
  type N <: NegInt
  type isNeg = True
  type neg <: PosInt
  type abs = neg
  type succ <: NonPosInt
  type pred <: NegInt
}
sealed trait PosInt extends NonNegInt with NonZeroInt {
  type N <: PosInt
  type isPos = True
  type neg <: NegInt
  type pred <: NonNegInt
  type succ <: PosInt
  type loop[B,F[_ <: B] <: B, Res <: B] = pred#loop[B,F,F[Res]]
}

case class ++[P <: NonNegInt]() extends PosInt {
  type N = ++[P]
  type succ = ++[++[P]]
  type add[R <: Integer] = P#add[R#succ]
  type pred = P
  type sub[R <: Integer] = P#sub[R#pred]
  type prod[R <: Integer] = P#prod[R]#add[R]
  type neg = --[P#neg]
  type predNat = P
  type addNat[R <: NonNegInt] = P#addNat[R#succ]
  type subNat[R <: NonNegInt] = (R#isZero)#branch[NonNegInt, N, P#subNat[R#predNat]]
  type divNat[D <: PosInt] = lt[D]#branch[NonNegInt, _0, p1#addNat[subNat[D]#divNat[D]]]
}

case class --[S <: NonPosInt]() extends NegInt {
  type N = --[S]
  type succ = S
  type add[N <: Integer] = S#add[N#pred]
  type pred = --[--[S]]
  type sub[N <: Integer] = S#sub[N#succ]
  type prod[N <: Integer] = (neg#prod[N])#neg
  type neg = ++[S#neg]
}

class _0 extends NonNegInt with NonPosInt {
  type N = _0
  type isZero = True
  type succ = ++[_0]
  type add[R <: Integer] = R
  type addNat[R <: NonNegInt] = R
  type subNat[R <: NonNegInt] = _0
  type divNat[R <: PosInt] = _0
  type pred = --[_0]
  type predNat = _0
  type sub[R <: Integer] = R#neg
  type prod[R <: Integer] = _0
  type div[R <: NonZeroInt] = _0
  type neg = _0
}