Dependent Types and Generalized Type Constraints

nat.scala

sealed trait Nat
sealed trait Zero extends Nat
sealed trait Succ[N <: Nat] extends Nat

vector.scala

sealed trait Vector[N <: Nat, +A] {

  type Length = N

  def zap[R](l: Vector[Length, A => R]): Vector[Length, R]

}

case object VNil extends Vector[Zero, Nothing] {

 def zap[R](l: Vector[Zero, Nothing => R]): VNil.type = VNil

}

case class VCons[N <: Nat, A](head: A, tail: Vector[N, A]) extends Vector[Succ[N], A] {

  def zap[R](l: Vector[Length, A => R]): Vector[Length, R] = l match {
    case VCons(f, fs) => VCons(f(head), tail zap fs)
  }

}

vector2.scala

sealed trait Vector2[+A] {
  
  type Length <: Nat

  def zap[R](l: Vector2[A => R])(implicit ev: l.Length =:= Length): Vector2[R]
}

object Vector2 {

  // adding a theorem that proves: Succ(N) == Succ(M) iff N == M
  implicit def succCong[A <: Succ[Zero], B <: Succ[Zero]]: A =:= B = ???
  implicit def succCong[N1, N2, A <: Succ[Succ[N1]], B <: Succ[Succ[N2]]](implicit ev: Succ[N1] =:= Succ[N2]): A =:= B = ???
}


case object VNil2 extends Vector2[Nothing] {

 type Length = Zero

 def zap[R](l: Vector2[Nothing => R])(implicit ev: l.Length =:= Length): VNil2.type = VNil2

}



case class VCons2[A](head: A, tail: Vector2[A]) extends Vector2[A] {

  type Length = Succ[tail.Length]

  def zap[R](l: Vector2[A => R])(implicit ev: l.Length =:= Length): Vector2[R] = l match {
    case VCons2(f, fs) => VCons2(f(head), tail zap fs)
  }

}