Units.scala

object UnitsTest extends App {
  import Units._
  import Integers._
    
  val length1 = m(23)
  val length2 = m(17)
  val area: Quantity[_2, _0] = length1 * length2 // Works
   
  val time = s(42)
  val foo: Quantity[_1, _1] = time * length1  // Works
  
  val speed: Quantity[_1, _1#Neg] = length1 / time // Doesn't work
  /*
  type mismatch;
    found   : 
      Units.Quantity[Subtractables.-[Integers._1,Integers._0],
                     Subtractables.-[Integers._0,Integers._1]]
    required:
      Units.Quantity[Integers._1,Integers._0]
  */
  
  val lengt3: Quantity[_1, _0] = length1 * length2 / length1 // Doesn't work
  /*
  type mismatch;
    found   : 
      Units.Quantity[Subtractables.-[Addables.+[Integers._1,Integers._1],Integers._1],
                     Subtractables.-[Addables.+[Integers._0,Integers._0],Integers._0]]
    required: 
      Units.Quantity[Integers._1,Integers.MNeg[Integers.MSucc[Integers._0]]]	
   */
}

object Units {
  import Integers._
  import Addables._
  import Subtractables._

  trait Unit {
    type M <: MInt
    type S <: MInt
  }
  
  final class TUnit[_M <: MInt, _S <: MInt] {
    type M = _M
    type S = _S
  }
  
  case class Quantity[M <: MInt, S <: MInt](value : Double) {
    type This = Quantity[M, S]
    def *[M2 <: MInt, S2 <: MInt](m : Quantity[M2, S2]) = Quantity[M + M2, S + S2](value * m.value)
    def /[M2 <: MInt, S2 <: MInt](m : Quantity[M2, S2]) = Quantity[M - M2, S - S2](value / m.value)
    def apply(v : Double) = Quantity[M, S](v * value)
  }
    
  val m = Quantity[_1, _0](1)
  val s = Quantity[_0, _1](1)
}

object Addables {
  trait Addable {
    type AddType <: Addable
    type Add[T <: AddType] <: AddType
  }

  type +[A1 <: Addable, A2 <: A1#AddType] = A1#Add[A2]  
}

object Subtractables {
  trait Subtractable {
    type SubType <: Subtractable
    type Sub[T <: SubType] <: SubType
  }

  type -[S1 <: Subtractable, S2 <: S1#SubType] = S1#Sub[S2]
}

object Comparables {
  import Booleans._

  trait Comparable {
    type CompareType <: Comparable
    type LessThan[T <: CompareType] <: Bool
  }
}


object Booleans {
  sealed trait Bool {
    type Not <: Bool
  }
  
  final class True extends Bool {
    type Not = False
  }
  
  final class False extends Bool {
    type Not = True
  }
}

object Integers {
  import Visitables._
  import Addables._
  import Subtractables._

  trait NatVisitor extends TypeVisitor {
    type Visit0 <: ResultType
    type VisitSucc[Pre <: Nat] <: ResultType
  }
  
  trait IntVisitor extends NatVisitor {
    type VisitNeg[Pos <: Nat] <: ResultType
  }
  
  sealed trait MInt extends Visitable[IntVisitor] with Addable with Subtractable {
    type AddType = MInt
    type SubType = MInt
    type Add[I <: MInt] <: MInt
    type Neg <: MInt
    type Succ <: MInt
    type Pre <: MInt
  }
  
  sealed trait Nat extends MInt {
    type Accept[V <: IntVisitor] = AcceptNatVisitor[V]
    type AcceptNatVisitor[V <: NatVisitor] <: V#ResultType
  }
  
  final class _0 extends Nat {
    type Add[I <: MInt] = I
    type AcceptNatVisitor[V <: NatVisitor] = V#Visit0
    type Neg = _0
    type Succ = MSucc[_0]
    type Pre = Succ#Neg
  }
  
  sealed trait Pos extends Nat
  
  final class MSucc[P <: Nat] extends Pos {
    type This = MSucc[P]
    type Add[N <: MInt] = P#Add[N]#Succ
    type AcceptNatVisitor[V <: NatVisitor] = V#VisitSucc[P]
    type Neg = MNeg[This]
    type Pre = P
    type Succ = MSucc[This]
  }
  
  final class MNeg[N <: Pos] extends MInt {
    type Add[N <: MInt] = N#Add[N#Neg]#Neg
    type Accept[V <: IntVisitor] = V#VisitNeg[N]
    type Neg = N
    type Succ = N#Pre#Neg
    type Pre = N#Succ#Neg
  }
  
  type _1 = MSucc[_0]
  type _2 = MSucc[_1]
  type _3 = MSucc[_2]
  
  val _0 = new _0
  val _1 = new _1
  val _2 = new _2
  val _3 = new _3
}

object Nats {
  import Utils._
  import Booleans._
  import Addables._
  import Comparables._
  import Visitables._

  trait NatVisitor extends TypeVisitor {
    type Visit0 <: ResultType
    type VisitSucc[Pre <: Nat] <: ResultType
  }
  
  sealed trait Nat extends Addable with Comparable {
    type CompareType = Nat
    
    type Pre
    type Is0 <: Bool
    type Add[T <: Nat] <: Nat
    type AddType = Nat
    type Accept[N <: NatVisitor] <: N#ResultType
    type Equals[N <: Nat] <: Bool
    type LessThan[N <: Nat] <: Bool

    def toInt : Int
  }
  
  final class _0 extends Nat {
    type Pre = Invalid
    type Is0 = True
    type Add[N <: Nat] = N
    type Accept[N <: NatVisitor] = N#Visit0

    type Equals[N <: Nat] = N#Is0
    type LessThan[N <: Nat] = N#Is0#Not

    def toInt = 0
  }
  
  final case class Succ[P <: Nat](toInt : Int) extends Nat {
    type Pre = P
    type Is0 = False
    type Add[N <: Nat] = Succ[P#Add[N]]
    type Accept[N <: NatVisitor] = N#VisitSucc[P]

    trait EqualsVisitor extends NatVisitor {
      type ResultType = Bool
      type Visit0 = False
      type VisitSucc[Pre <: Nat] = P#Equals[Pre]
    }

    type Equals[N <: Nat] = N#Accept[EqualsVisitor]

    trait LessThanVisitor extends NatVisitor {
      type ResultType = Bool
      type Visit0 = False
      type VisitSucc[Pre <: Nat] = P#LessThan[Pre]
    }

    type LessThan[N <: Nat] = N#Accept[LessThanVisitor]

    def +[N <: Nat](n : N) : Add[N] = Succ[P#Add[N]](toInt + n.toInt)
  }
  
  type _1 = Succ[_0]
  type _2 = Succ[_1]
  type _3 = Succ[_2]
  
  val _0 = new _0
  val _1 = new _1(1)
  val _2 = new _2(2)
  val _3 = new _3(3)
}

object Visitables {
  trait TypeVisitor {
    type ResultType
  }

  trait Visitable[V <: TypeVisitor] {
    type Accept[V2 <: V] <: V2#ResultType
  }
}

object Utils {
  final class Invalid

  case class TypeToValue[T, VT](value : VT) {
    def apply() = value
  }
}