LinVect.scala

object LinVect {

  type K = Double

  // type Nat

  trait NatClass[N] {
    val nat: Int
  }

  def NatClass[N: NatClass]: NatClass[N] = implicitly

  def nat[N: NatClass]: Int = NatClass[N].nat

  case class FinBase[N: NatClass](i: Int)

  trait NatValue {
    type N
    type Fin
    val typeclass: NatClass[N]
  }

  // conctructor Zero

  final class Zero

  implicit object ZeroClass
    extends NatClass[Zero]
  {
    override val nat = 0
  }

  object ZeroValue
    extends NatValue
  {
    override type N = Zero
    override type Fin = FinBase[N]
    override val typeclass = ZeroClass
  }

  // constructor Add1

  final class Add1[N: NatClass]

  implicit def Add1Class[N: NatClass] =
    new NatClass[Add1[N]] {
      override val nat = 1 + NatClass[N].nat
    }

  case class Add1Value(n1: NatValue)
    extends NatValue
  {
    private implicit val local: NatClass[n1.N] = n1.typeclass
    override type N = Add1[n1.N]
    override type Fin = FinBase[N]
    override val typeclass = Add1Class[n1.N]
  }

  // constructor Mul2

  final class Mul2[N: NatClass]

  implicit def Mul2Class[N: NatClass] =
    new NatClass[Mul2[N]] {
      override val nat = 2 * NatClass[N].nat
    }

  case class Mul2Value(n1: NatValue)
    extends NatValue
  {
    private implicit val local: NatClass[n1.N] = n1.typeclass
    override type N = Mul2[n1.N]
    override type Fin = FinBase[N]
    override val typeclass = Mul2Class[n1.N]
  }

  // get Nat from Int

  def buildNat(i: Int): NatValue = {
    require(i >= 0)

    if (i == 0)
      ZeroValue
    else if (i % 2 == 1)
      Add1Value(buildNat(i - 1))
    else
      Mul2Value(buildNat(i / 2))
  }

  // now linear algebra

  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: NatClass](f: FinBase[N] => K) extends (FinBase[N] => K) {
      override def apply(i: FinBase[N]): K = f(i)
      final val maxIndex = nat[N]
    }

    implicit def Free_Space[I: NatClass] =
      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)
      }
  }

  def main(args: Array[String]): Unit = {
    import Space._

    val NAT_10 = buildNat(scala.io.StdIn.readLine("NAT_10 > ").toInt)
    implicit val NAT_10_class = NAT_10.typeclass
    val NAT_100 = buildNat(scala.io.StdIn.readLine("NAT_100 > ").toInt)
    implicit val NAT_100_class = NAT_100.typeclass

    type K_10 = Free[NAT_10.N]
    type K_100 = Free[NAT_100.N]
    val v_10 = Free[NAT_10.N]{ case FinBase(i) => i*i }
    val v_100 = Free[NAT_100.N]{ case FinBase(i) => i }
    val f_10_100 = Hom[K_10, K_100]{ case Free(f) => Free{ case FinBase(i) => f(FinBase(i % 10)) |*| 1d } }
    val g_10_100 = Hom[K_10, K_100]{ case Free(f) => Free{ case FinBase(i) => f(FinBase(i % 10)) |*| 2d } }
    val f_100_10 = Hom[K_100, K_10]{ case Free(f) => Free{ case FinBase(i) => f(FinBase(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
  }

}