Playing with dependent types in Scala

Vect.scala

package Vect

import scala.language.higherKinds

sealed trait Nat
sealed trait Z extends Nat
sealed trait S[N <: Nat] extends Nat

trait Exists[A, +B[_ <: A]] {
  type fst <: A
  def  snd: B[fst]
}

sealed trait Vect[N <: Nat, +A] {
  // helper, so I don't have to write type-level lambdas
  type V[N <: Nat] = Vect[N, A] 
  type Length = N

  def ::[B >: A](a: B): Vect[S[Length], B]

  def map[B](f: A => B): Vect[Length, B]
  def filter(f: A => Boolean): Exists[Nat, V]
}

final case object VNil extends Vect[Z, Nothing] {
  def ::[A](a: A): Vect[S[Length], A] =
    VCons(a, VNil)

  def map[B](f: Nothing => B): Vect[Length, Nothing] =
    VNil

  def filter(f: Nothing => Boolean): Exists[Nat, V] =
    new Exists[Nat, V] {
      type fst = Z
      def  snd = VNil
    }
}

final case class VCons[A, N <: Nat](head: A, tail: Vect[N, A])
  extends Vect[S[N], A]
{
  def ::[B >: A](a: B): Vect[S[Length], B] =
    VCons(a, this)

  def map[B](f: A => B): Vect[Length, B] =
    VCons(f(head), tail.map(f))

  def filter(f: A => Boolean): Exists[Nat, V] = {
    val v = tail.filter(f)

    if (f(head))
      new Exists[Nat, V] {
        type fst = S[v.fst]
        def  snd = head :: v.snd
      }
    else
      new Exists[Nat, V] {
        type fst = v.fst
        def  snd = v.snd
      }
  }
}