How do I compute type-level M + N?

Question
2

You can move the responsibility to prove that N + M is a singleton value to the callsite of ++.

class Vec[N <: Int](using n: ValueOf[N]) :
  private val xs: Array[Double] = Array.ofDim[Double](n.value)
  def ++[M <: Int](other: Vec[M])(using ValueOf[N + M]) =
    val result = Vec[N + M]
    for i <- 0 until xs.length do
      result.xs(i) = xs(i)
    for i <- 0 until other.xs.length do
      result.xs(i + xs.length) = other.xs(i)
    result

That seems to work in this scastie:

1 Like