Dependent typing without no-longer-supported type ascriptions

Question
1

Starting with Scala 3.3,

Type ascriptions after patterns other than:

  • variable pattern, e.g. case x: String =>
  • number literal pattern, e.g. case 10.5: Double =>

are no longer supported. Remove the type ascription or move it to a separate variable pattern.

I relied on such type ascriptions for certain forms of dependent typing. The code below is an example. Is there a way to rewrite it without such type ascriptions?

def dependentlyTypedMod2[N <: NatT](n: N): Mod2[N] = n match
  case z: Zero => z
  case Succ(Zero()): Succ[Zero] => Succ(Zero())
  case Succ(Succ(predPredN)): Succ[Succ[?]] => dependentlyTypedMod2(predPredN)

type Mod2[N <: NatT] <: NatT = N match
  case Zero => Zero
  case Succ[Zero] => Succ[Zero]
  case Succ[Succ[predPredN]] => Mod2[predPredN]

sealed trait NatT
case class Zero() extends NatT
case class Succ[N <: NatT](n: N) extends NatT
2

I think I found a solution:

def dependentlyTypedMod2[N <: NatT](n: N): Mod2[N] = n match
  case _: Zero => Zero()
  case s: Succ[?] => s match
    case Succ(predN) => predN match
      case _: Zero => Succ(Zero())
      case s: Succ[?] => s match
        case Succ(predPredN) => dependentlyTypedMod2(predPredN)

type Mod2[N <: NatT] <: NatT = N match
  case Zero => Zero
  case Succ[predN] => predN match
    case Zero => Succ[Zero]
    case Succ[predPredN] => Mod2[predPredN]

sealed trait NatT
case class Zero() extends NatT
case class Succ[N <: NatT](n: N) extends NatT
1 Like
3

This has quite a bit of boilerplate. It would be nice if type ascriptions were allowed again as syntactic sugar for such nested match expressions.

1 Like
4

It would also be nice if such code could be written with normal Int types. The best I can do is below, but it still uses asInstanceOf.

import scala.compiletime.ops.int.-

def dependentlyTypedMod2[I <: Int](i: I): Mod2[I] = i match
  case _: 0 => 0
  case _: 1 => 1
  case _ => dependentlyTypedMod2((i - 2).asInstanceOf[I - 2])

type Mod2[I <: Int] <: Int = I match
  case 0 => 0
  case 1 => 1
  case _ => Mod2[I - 2]
5

Actually, never mind, I just figured out a way to do it:

import scala.compiletime.constValue
import scala.compiletime.ops.int.-

inline def dependentlyTypedMod2[I <: Int](i: I): Mod2[I] = i match
  case _: 0 => 0
  case _: 1 => 1
  case _ => dependentlyTypedMod2(constValue[I - 2])

type Mod2[I <: Int] <: Int = I match
  case 0 => 0
  case 1 => 1
  case _ => Mod2[I - 2]
1 Like