Scala type table lookup

Question

Given opaque types X, Y, is it possible to have a return type of Table[X, Y], which resolves to one of X, Y, or to a third type Z?

The following (obviously) doesn't compile:

opaque type ConstrainedInt = Int
opaque type PositiveInt <: ConstrainedInt = Int
opaque type NegativeInt <: ConstrainedInt = Int

object PositiveInt:
    def apply(n: Int): PositiveInt =
        require(n > 0)
        n

object NegativeInt:
    def apply(n: Int): NegativeInt =
        require(n < 0)
        n

type AddType[PositiveInt, PositiveInt] = PositiveInt
type AddType[NegativeInt, NegativeInt] = NegativeInt

extension[X <: ConstrainedInt](x: X)
    def +[Y <: ConstrainedInt](y: Y): AddType[X, Y] = x + y

A typeclass version doesn't compile either

trait AddType[X <: ConstrainedInt, Y <: ConstrainedInt]:
    type Result <: ConstrainedInt

given AddType[PositiveInt, PositiveInt] = new AddType { type Type = PositiveInt }
given AddType[NegativeInt, NegativeInt] = new AddType { type Type = NegativeInt }

extension[X <: ConstrainedInt](x: X)
    def +[Y <: ConstrainedInt](y: Y)(using t: AddType[X, Y]): t.Result = x + y

producing

[E007] Type Mismatch Error: cmd2.sc:22:77 -----------------------------------
22 |        def +[Y <: ConstrainedInt](m: Y)(using t: AddType[X, Y]): t.Result = n + m
   |                                                                             ^^^^^
   |    Found:    Int
   |    Required: t.Result

Update

Trying to follow https://stackoverflow.com/a/76046222 advice.

constrained.scala

object constrained:
    opaque type PositiveInt = Int
    opaque type NegativeInt = Int

    object PositiveInt:
        def apply(n: Int): PositiveInt =
            require(n > 0)
            n

    object NegativeInt:
        def apply(n: Int): NegativeInt =
            require(n < 0)
            n

    extension[X <: PositiveInt | NegativeInt](x: X)
        def +[Y <: PositiveInt | NegativeInt](y: Y): TypeTables.AddType[X, Y] = x + y

TypeTables.scala

object TypeTables:
    import constrained.*

    type AddType[X <: PositiveInt | NegativeInt, Y <: PositiveInt | NegativeInt] = X match
        case PositiveInt => Y match
            case PositiveInt => PositiveInt
            case NegativeInt => Int
        case NegativeInt => Y match
            case NegativeInt => NegativeInt
            case PositiveInt => Int

scalac constrained.scala TypeTables.scala
scala -classpath .

scala> import constrained.*
scala> import TypeTables.*

scala> PositiveInt(3) + NegativeInt(-4)
val res0: 
  constrained.NegativeInt match {
    case constrained.PositiveInt => constrained.PositiveInt
    case constrained.NegativeInt => Int
  } = -1

scala> NegativeInt(-4) + PositiveInt(3)
val res1: TypeTables.AddType[constrained.NegativeInt, constrained.PositiveInt] = -1

scala> NegativeInt(-3) + NegativeInt(-4)
     | 
val res2: TypeTables.AddType[constrained.NegativeInt, constrained.NegativeInt] = -7

scala> val a: Int = PositiveInt(3) + NegativeInt(-4)
-- [E007] Type Mismatch Error: ---------------------------------------------------------------------
1 |val a: Int = PositiveInt(3) + NegativeInt(-4)
  |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  |             Found:    constrained.NegativeInt match {
  |               case constrained.PositiveInt => constrained.PositiveInt
  |               case constrained.NegativeInt => Int
  |             }
  |             Required: Int
  |
  | longer explanation available when compiling with `-explain`
1 error found

scala> val a: NegativeInt = NegativeInt(-4) + NegativeInt(-3)
-- [E007] Type Mismatch Error: ---------------------------------------------------------------------
1 |val a: NegativeInt = NegativeInt(-4) + NegativeInt(-3)
  |                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  |      Found:    TypeTables.AddType[constrained.NegativeInt, constrained.NegativeInt]
  |      Required: constrained.NegativeInt
  |
  |      Note: a match type could not be fully reduced:
  |
  |        trying to reduce  TypeTables.AddType[constrained.NegativeInt, constrained.NegativeInt]
  |        failed since selector  constrained.NegativeInt
  |        does not match  case constrained.PositiveInt => constrained.NegativeInt match {
  |        case constrained.PositiveInt => constrained.PositiveInt
  |        case constrained.NegativeInt => Int
  |      }
  |        and cannot be shown to be disjoint from it either.
  |        Therefore, reduction cannot advance to the remaining case
  |
  |          case constrained.NegativeInt => constrained.NegativeInt match {
  |        case constrained.NegativeInt => constrained.NegativeInt
  |        case constrained.PositiveInt => Int
  |      }
  |
  | longer explanation available when compiling with `-explain`
1 error found

Answer 1

I think you can make your first example work if you define AddType as a match type, as you need to cover all cases. Something like this:

type AddType[A <: ConstrainedInt, B <: ConstrainedInt] = A match 
  case PositiveInt => B match 
    case PositiveInt => PositiveInt
    case NegativeInt => ConstrainedInt
    case ConstrainedInt => ConstrainedInt
  case NegativeInt => B match 
    case PositiveInt => ConstrainedInt
    case NegativeInt => NegativeInt
    case ConstrainedInt => ConstrainedInt
  case ConstrainedInt => ConstrainedInt