First simple type computation

simplecomputation.scala

object console extends App {

  trait Nat {
    type Plus[That <: Nat] <: Nat
  }
  trait _0 extends Nat {
    type Plus[That <: Nat] = That
  }
  trait Succ[N <: Nat] extends Nat {
    type Plus[That <: Nat] = Succ[N#Plus[That]]
  }

  type _1 = Succ[_0]
  type _2 = Succ[_1]
  type _3 = Succ[_2]

  implicitly[_1#Plus[_2] =:= _3]
  // implicitly[_1#Plus[_1] =:= _3]

  object phantom {

    //trait SList[Size <: Nat] {
    //  def ::(t: Int): SList[Nat]
    //}
    //object SNil extends SList[_0] {
    //  def ::(t: Int): SList[_1] = SCons[_1](t, SNil) 
    //}
    //case class SCons[TailSize <: Nat](head: Int, tail: SList[TailSize]) extends SList[TailSize] {
    //  def ::(t: Int): SList[Succ[TailSize]] = SCons(t, head :: tail) 
    //}
  }

  object implicits {

    trait Size[T] {
      type V <: Nat
    }

    trait Size0 {
    }

    object Size extends Size0 { 
      implicit def nil[T] = new Size[T] {
        type V = _0
      }
      implicit def cont[F[_], T](implicit s: Size[T]) = new Size[F[T]] {
        type V = Succ[s.V]
      } 
    }

    def foo[T](t: T)(implicit S: Size[T]): S.V = ???
   
    val count2: _2 = foo(List(Option(3)))
    val count1: _1 = foo(Option(3))
    val count0: _0 = foo(3)

    // val wrongCount1: _1 = foo(List(Option(3)))
  }

  object Print {
    trait Print[T] {
      type R
      def print: R   
    }

    object Print {
      implicit def printT[T] = new Print[T] {
        type R = String
        def print = s"T"
      } 
      implicit def printF[F[_], T](implicit p: Print[T]) = new Print[F[T]] {
        type R = String
        def print = s"F[T]: ${p.print}"
      }
    }
    def print[T](t: T)(implicit p: Print[T]): p.R = ??? // p.print
    val res = print(List(Option(2)))
    println(s"res: ${res}")
  }

   Print
}