How do I compute type-level M + N?

Question
1

This query got no love on Discord.

How do I use the sum of two singleton integer types? I am trying to make a ++ operator for concatenating a vector of length N with one of length M (both compile-time constants). The obvious thing

class Vec[N <: Int & Singleton](using n: ValueOf[N]) :
  private val xs: Array[Double] = Array.ofDim[Double](n.value)
  def ++[M <: Int & Singleton](other: Vec[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

(complete code on Scastie - An interactive playground for Scala.) fails with

No singleton value available for N + M where:    M is a type in method ++ with bounds <: Int & Singleton.

There is a related bug report at https://github.com/lampepfl/dotty/issues/8257 that was closed, apparently without action. So how am I supposed to do this?

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
3

Thank you very much! That works.

I would love to understand why. My guess is the using clause of the class.

I tried removing the using clause, like this:

class Vec[N <: Int & Singleton] :
  private val xs: Array[Double] = Array.ofDim[Double](summon[ValueOf[N]].value)

Now I got

No singleton value available for N.

With

class Vec[N <: Int & Singleton] :
  private val xs: Array[Double] = Array.ofDim[Double](valueOf[N])

the message becomes even less helpful:

cannot reduce summonFrom with patterns :  case given ev @ _:ValueOf[N]

Obviously, I ascribe too much power to the Singleton bound, perhaps because of the wording in https://scala-lang.org/api/3.x/scala/Singleton.html: “When a type parameter has an explicit upper bound of Singleton, the compiler infers a singleton type.” Clearly here it did not.

Is that how it should be, or should I report a bug?

Thanks,

Cay

4

I think your analysis is pretty accurate. I’m not sure there’s a bug here though. But the error messages could definitely be better.

5

Thanks very much! I filed https://github.com/lampepfl/dotty/issues/15829, noting that either this is a bug or the error message needs work.

1 Like