In the code below, I define addition at the type level, and then at the term level. Is it possible to modify the code in such a way that the refined signature def natSum[M <: NatT, N <: NatT](m: M, n: N): NatSum[M, N] type checks?

sealed trait NatT
final case class Zero() extends NatT
final case class Succ[+N <: NatT](n: N) extends NatT
type NatSum[M <: NatT, N <: NatT] <: NatT = (M, N) match
case (_, Zero) => M
case (Zero, _) => N
case (Succ[predM], Succ[predN]) => Succ[Succ[NatSum[predM, predN]]]
def natSum(m: NatT, n: NatT): NatT = (m, n) match
case (_, Zero()) => m
case (Zero(), _) => n
case (Succ(predM), Succ(predN)) => Succ(Succ(natSum(predM, predN)))

Adding types to the patterns seems to do the trick:

sealed trait NatT
final case class Zero() extends NatT
final case class Succ[+N <: NatT](n: N) extends NatT
type NatSum[M <: NatT, N <: NatT] <: NatT = (M, N) match
case (_, Zero) => M
case (Zero, _) => N
case (Succ[predM], Succ[predN]) => Succ[Succ[NatSum[predM, predN]]]
def natSum[M <: NatT, N <: NatT](m: M, n: N): NatSum[M, N] = (m, n) match
case (_, Zero()): (_, Zero) => m
case (Zero(), _): (Zero, _) => n
case (Succ(predM), Succ(predN)): (Succ[_], Succ[_]) => Succ(Succ(natSum(predM, predN)))

Oddly, the compiler issues the following warning:

match may not be exhaustive.
It would fail on pattern case: (_, _)

I knew Iâ€™d seen this problem before. I took the Coursera course last year and it had a similar problem in course 1, week 3.

Even with it compiling, I wasnâ€™t able to get it to run as-is. The problem was a ClassCastException, because once itâ€™s run, all it knows is that M is a subclass of NatT, but it doesnâ€™t know how to translate it to a NatSum[A, B], because NatSum[A, B] is defined in terms of two types, A and B, and m only has one type. M might be a different subtype branch of NatT than NatSum[A, B]. (And Iâ€™m using A and B, because the M and N in the NatSum definition arenâ€™t the same M and N in the natSum definition) You can either give it guidance on how to convert it to that type, which is what I did at first, but then I looked up the problem demonstration in the class, and then implemented that solution with natSum instead of a class implementation of â€ś+â€ť. Hereâ€™s what Iâ€™ll tell you: you donâ€™t need the type NatSum at all. Just think that x + y is the successor to xâ€™s predecessor + y.

Thereâ€™s no guarantee that m is either a Zero or Succ. It could be some other class that is a subclass of NatM.

I donâ€™t know what NatM is. But if you mean NatT, then I think there is: NatT is sealed (so the compiler neednâ€™t consider someone adding another extention to NatT), and Zero and Succ are its only subtypes.

In fact, this warning doesnâ€™t show up when compiling the original code:

def natSum(m: NatT, n: NatT): NatT = (m, n) match
case (_, Zero()) => m
case (Zero(), _) => n
case (Succ(predM), Succ(predN)) => Succ(Succ(natSum(predM, predN)))

There are many ways to implement NatSum. I know my way is not the simplest, but I like its symmetry and efficiency in terms of steps. Whether I â€śneedâ€ť it or not depends on what you mean by that, and is rather irrelevant in this conversation.

I think the problem here is that you have a recursive match type, and I think that the necessary type information is missing when you are working on values.

In the NatSum match type you are telling the compiler to destructure the type, but (AFAIK) there is no such ability when dealing with concrete methods.

Inside the def natSum[N, M] method the compiler doesnâ€™t know what the concrete types are (as they are passed in from the outside), so it has no way to determine what the NatSum of the inner types of Succ. You might be able to do something clever with typeclasses that would fit the bill.

Yes, I meant NatT. If you think because it is sealed it shouldnâ€™t give that warning, talk to the compiler designers. It warns about a missing (_, _) case because it thinks it is possible to have some result other than the three you specified.

EDIT: Hereâ€™s one way, with a sealed type, you can have an unmatched type:

val temp0 = new NatT() {}

I canâ€™t test it exactly, because I get a ClassCastException every time I run your code as-is unless the second argument is Zero(), whatever the first argument is, and then, if the first argument is temp0 the returned type is Main$$anon$1@277 because it matches on the second match. The following code will run the way you want it, and demonstrate a match error:

def natSum[M <: NatT, N <: NatT](m: M, n: N): NatSum[M, N] = (m, n) match
case (_, Zero) => m.asInstanceOf[NatSum[M, N]]
case (Zero, _) => n.asInstanceOf[NatSum[M, N]]
case (Succ(predM), Succ(predN)) => Succ(Succ(natSum(predM, predN))).asInstanceOf[NatSum[M, N]]
object Main extends App {
val temp0 = new NatT() {}
val temp1 = Zero
val temp2 = Succ(Zero)
val temp3 = natSum(temp0, temp2)
println("Hello")
}

This the code I was referring to before when I said, â€śYou can â€¦ give it guidance on how to convert it to that type.â€ť You have to specify to NatSum[A, B] what A and B are to get it to understand what to do.

Iâ€™m not sure I fully follow your argument. However, note that my solution does compile, albeit with a warning. Also, the simple version of natSum compiles without warning:

type NatSum[M <: NatT, N <: NatT] <: NatT = N match
case Zero => M
case Succ[predN] => Succ[NatSum[M, predN]]
def natSum[M <: NatT, N <: NatT](m: M, n: N): NatSum[M, N] = n match
case Zero(): Zero => m
case Succ(predN): Succ[_] => Succ(natSum(m, predN))

Are these facts compatible with your line of reasoning?