Search code examples
scalascala-3type-level-computationsingleton-type

How to do type-level addition in Scala 3?


How can I impletement type-level operations (addition in this case) in Scala 3 ?

Here is what I would like to do (this does not compile) :

case class foo[S <: Int & Singleton](value: Double) {
    def bar[T <: Int & Singleton](that: foo[T]): foo[S + T] = new foo[S + T](this.value * that.value)
}

val t1 = foo[1](1.5)
val t2 = foo[1](2.0)

val t3 = t1 bar t2 //foo[2](3.0)

PS : the SIP-23 proposal talks about libraries that implement such behaviour in Scala 2 but I am interested in Scala 3.


Solution

  • You need to import scala.compiletime.ops.int.+

    https://docs.scala-lang.org/scala3/reference/metaprogramming/compiletime-ops.html#the-scalacompiletimeops-package

    But then you have to remove upper bound & Singleton for S

    case class foo[S <: Int /*& Singleton*/](value: Double):
      def bar[T <: Int & Singleton](that: foo[T]): foo[S + T] =
        new foo[S + T](this.value * that.value)
    

    The thing is that the + is defined as

    type +[X <: Int, Y <: Int] <: Int
    

    This addition is executed at compile time by the compiler but technically there is no upper bound <: Singleton for S + T.

    If you really want to restore the upper bound for S you can replace the upper bound with generalized type constraint <:<

    case class foo[S <: Int](value: Double)(using S <:< Singleton):
      def bar[T <: Int & Singleton](that: foo[T])(using (S + T) <:< Singleton): foo[S + T] =
        new foo[S + T](this.value * that.value)
    

    More about the difference <: vs <:< :

    In scala 3, is it possible to make covariant/contravariant type constructor to honour coercive subtyping?

    https://blog.bruchez.name/posts/generalized-type-constraints-in-scala/