size-safe vector

RowVectorPhantom.sc

// A row vector of Ts, with the number of rows encoded as a type.
// Key invariants on methods are encoded through types and witnesses.
@tinvariant[R >= 0)]
trait RowVectorPhantom[T, R <: XInt] {
  def apply[I]
    (implicit i: ValueOf[I])
    (implicit iIsPositive: I >= 0, iIsWithinRange: I < R): T

  def rows(implicit r: ValueOf[R]): Int = r.value
}

// We can concatonate two row vectors, into a new vector that is the sum of their lengths
def concat[T, M <: XInt, N <: XInt]
  (ms: RowVectorPhantom[T, M], ns: RowVectorPhantom[T, N])
  (implicit mn: M + N): RowVectorPhantom[T, mn.Out]


// We should be able to provably-safely access elements and loop over them.
//
// 0.until[rvp.R] provides elements of a type something like:
//   i : BoundedByRange[F <: XInt, U <: XInt] { type I <: XInt }
// which has implicit witnesses for:
//   i => ValueOf[i.I],
//   i.I >= F,
//   i.I < U
for(i <- 0.until[rvp.R]) {
  println(
    rvp(i) // implicit conversion of i kicks in
  )
}

UnitsKnownPoint.sc

// Let's propogate units as a phantom on the numeric type
// 4 meters per second x 10 seconds is 40 m
// n^[X] is `n` with the units `X`
4^[M/S] * 10^[S] ==> 40^[M]

// And propagate the known decimal points with a phantom type
// D[i] is a numeric with `i` places after the decimal point
(0.4: D[1]) * (0.01: D[2]) ==> (0.040: D[3])

// Now put the two together to track the decimal points and units:
(0.4: D[1])^[M/S] * (0.01: D[2])^[S] ==> (0.040: D[3])^[M]

//So what is the generalised signature of `*`?

trait Multiply [L, R] {
  type Out
  def apply(l: L, r: R): Out
}

implicit object multiplyInt extends Multiply[Int, Int] = ...
implicit object multiplyDouble extends Multiply[Double, Double) = ...

implicit object multiplyD[LP, RP] {
  type Out = D[LP + RP]
  def apply(l: D[LP], r: D[RP]): Out = ...
}

implicit def multiplyUnits[Ln, Rn, On, Lu, Ru, Ou]
  (implicit m: Multiply[Ln, Rn] { type Out = On }) = new MultiplyUnits[Ln^Lu, Rn^Lu] {
  type Out = On^Ou
  def apply(l: Ln^Lu, r: Rn^Lu): On^Ou = m(l.value, r.value)^[Ou]
}