DependentTypedLength.scala

object DependentTypedLength extends App {

  sealed trait Nat

  sealed trait Z extends Nat

  sealed trait S[A <: Nat] extends Nat

  trait NList[A <: Nat, +B] {
    type Length = A

    def zip[C](l: NList[Length, C]): NList[Length, (B, C)]

    def length: Int
  }

  case object NNil extends NList[Z, Nothing] {
    override def zip[C](l: NList[NNil.Length, C]): NNil.type = NNil

    def ::[A](h: A): Z NCons A = NCons(h, this)

    override def length: Int = 0
  }

  case class NCons[A <: Nat, B](head: B, tail: NList[A, B]) extends NList[S[A], B] {
    override def zip[C](l: NList[Length, C]): NList[Length, (B, C)] = l match {
      case NCons(x, xs) => NCons((head, x), tail zip xs)
    }

    def ::(h: B): NCons[S[A], B] = NCons(h, this)

    override def toString = s"$head :: ${tail.toString}"

    override def length: Int = tail.length + 1
  }

  val l0 = 2 :: 1 :: NNil

  val l1 = 0 :: 1 :: 2 :: NNil
  val l2 = "A" :: "B" :: "C" :: NNil

  val b = (l1 zip l2) == (0, "A") ::(1, "B") ::(2, "C") :: NNil

}