Dotty Natural Numbers Proofs Using Dependent Types

DepTypedNats.scala

object Main extends App {
  type Nat
  type Zero <: Nat
  type Succ[N <: Nat] <: Nat

  type One = Succ[Zero]

  type NonZero[X <: Nat] = X match {
    case Zero => Zero
    case Succ[_] => Succ[Zero]
  }

  type Add[X <: Nat, Y <: Nat] = X match {
    case Zero => Y
    case Succ[lessone] => Add[lessone, Succ[Y]]
  }

  type Two = Add[One, One]
  type Three = Add[Two, One]
  type Theer = Add[One, Two]

  type Twice[X <: Nat] = Add[X, X]

  println(implicitly[Three =:= Theer])
  println(implicitly[Three =:= Succ[Twice[One]]])

//  type Even[X] = X match { // TODO this seems impossible without existential types
//    case Twice[half] => X =:= Twice[half]
//  }

}