Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment