LinVect.scala

object LinVect {

  type K = Double

  trait NAT[N] { val nat: Int }
  def NAT[N: NAT]: NAT[N] = implicitly
  def nat[N: NAT]: Int = NAT[N].nat

  trait NAT_10
  implicit object NAT_10 extends NAT[NAT_10]
    { override val nat = 10 }

  trait NAT_100
  implicit object NAT_100 extends NAT[NAT_100]
  { override val nat = 100 }

  case class Fin[N: NAT](i: Int) { // 0 <= i < nat[N]
    final val max = nat[N]
  }

  trait Space [V]
  {
    val get_0 : V
    val get_+ : (V, V) => V
    val get_- : V => V
    val get_* : (K, V) => V
  }

  implicit class ToSpaceOps[V](v1: V)(implicit space: Space[V])
  {
    def unary_- : V = space.get_- (v1)
    def |+| (v2: V): V = space.get_+ (v1, v2)
    def |*| (k2: K): V = space.get_* (k2, v1)
  }

  def _0_[V](implicit space: Space[V]): V = space.get_0

  object Space {

    type Ob[X] = Space[X]

    implicit object dim_0_Space extends Space[Unit] {
      override val get_0: Unit = ()
      override val get_+ : (Unit, Unit) => Unit = (_,_) => ()
      override val get_- : Unit => Unit = _ => ()
      override val get_* : (K, Unit) => Unit = (_,_) => ()
    }

    implicit object dim_1_Space extends Space[K] {
      override val get_0: K = 0d
      override val get_+ : (K, K) => K = _+_
      override val get_- : K => K = -_
      override val get_* : (K, K) => K = _*_
    }

    // lazy vector
    case class Free[N: NAT](f: Fin[N] => K) extends (Fin[N] => K) {
      override def apply(i: Fin[N]): K = f(i)
      final val maxIndex = nat[N]
    }

    implicit def Free_Space[I: NAT] =
      new Space[Free[I]] {
        override val get_0: Free[I] = Free(_ => 0d)
        override val get_+ : (Free[I], Free[I]) => Free[I] = (f, g) => Free(i => f(i) + g(i))
        override val get_- : Free[I] => Free[I] = f => Free(i => - f(i))
        override val get_* : (K, Free[I]) => Free[I] = (k, f) => Free(i => k * f(i))
      }

    case class Hom[V1: Space, V2: Space](f: V1 => V2) extends (V1 => V2) { selfHom =>
      override def apply(v1: V1): V2 = f(v1)
      // (local|nested|dependent) Kernel
      final type Ker = KerBase[V1, V2, selfHom.type]
      def Ker(v1: V1): Ker = KerBase[V1, V2, selfHom.type](v1)
    }

    // lazy matrix
    implicit def Hom_Space[V1: Space, V2: Space] =
      new Space[Hom[V1, V2]] {
        override val get_0: Hom[V1, V2] = Hom(_ => _0_[V2])
        override val get_+ : (Hom[V1, V2], Hom[V1, V2]) => Hom[V1, V2] = (f, g) => Hom(v1 => f(v1) |+| g(v1))
        override val get_- : Hom[V1, V2] => Hom[V1, V2] = f => Hom(v1 => - f(v1))
        override val get_* : (K, Hom[V1, V2]) => Hom[V1, V2] = (k, f) => Hom(v1 => f(v1) |*| k)
      }

    // global parametrized Kernel
    case class KerBase[V1, V2, F <: Hom[V1, V2] with Singleton](v1: V1)

    implicit def KerBase_Space[V1: Space, V2: Space, F <: Hom[V1, V2] with Singleton] =
      new Space[KerBase[V1, V2, F]] {
        override val get_0: KerBase[V1, V2, F] = KerBase(_0_[V1])
        override val get_+ : (KerBase[V1, V2, F], KerBase[V1, V2, F]) => KerBase[V1, V2, F] = (a, b) => KerBase(a.v1 |+| b.v1)
        override val get_- : KerBase[V1, V2, F] => KerBase[V1, V2, F] = a => KerBase(a.v1)
        override val get_* : (K, KerBase[V1, V2, F]) => KerBase[V1, V2, F] = (k, a) => KerBase(a.v1 |*| k)
      }
  }

  object TEST {
    import Space._
    type K_10 = Free[NAT_10]
    type K_100 = Free[NAT_100]
    val v_10 = Free[NAT_10]{ case Fin(i) => i*i }
    val v_100 = Free[NAT_100]{ case Fin(i) => i }
    val f_10_100 = Hom[K_10, K_100]{ case Free(f) => Free{ case Fin(i) => f(Fin(i % 10)) |*| 1d } }
    val g_10_100 = Hom[K_10, K_100]{ case Free(f) => Free{ case Fin(i) => f(Fin(i % 10)) |*| 2d } }
    val f_100_10 = Hom[K_100, K_10]{ case Free(f) => Free{ case Fin(i) => f(Fin(i * 10)) } }
    // val add_v = v_10 |+| v_100 // error
    // val add_f = f_10_100 |+| f_100_10 // error

    val ker_f = f_10_100.Ker(v_10)
    val ker_g = g_10_100.Ker(v_10)
    val add_ker_f_f = ker_f |+| ker_f
    // val add_ker_f_g = ker_f |+| ker_g // error
  }

}

Hmm, so, I don't see how I can read a number from command line arguments and pick up the right type.
Or how I can calculate the dimensionality of a 17k-like space and provide the type.