Using a match type as a function return type

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: (_, _)
1 Like

There’s no guarantee that m is either a Zero or Succ. It could be some other class that is a subclass of NatM. If you, say:

final case class Numb(i: Int) extends NatT

and makes a call:

val temp1 = Numb(6)
val temp2 = Numb(7)
natSum(temp1, temp2)

It turns into an error. But of course the compiler has to figure it can’t predict what you’ll link to this code later,

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.

1 Like

Yup! That’s how it’s usually axiomatized in Peano Arithmetic: x + Sy = S(x + y) Peano axioms - Wikipedia

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)))
1 Like

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.

Here is a reference that talks about using match types as function return types.

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.

Something like

trait Thing[N <: NatT] {
  def value: N
}

object Thing {
  implicit val zero: Thing[Zero] = new Thing[Zero] {
     value: Zero = Zero()
  }

  implicit def succ[Succ[Prev], Prev <: NatT: Thing] = new Thing[Succ[Prev]] {
     value: Succ[Prev] = Succ(summon[Thing[Prev]].value)
  }
}


def natSum[N, M](implicit thing: Thing[NatSum[N, M]]) : NatSum[N,M] = thing.value

but I can imagine you would hit implicit resolution problems fairly quickly (if it works at all)

Example of this sort of working: Scastie - An interactive playground for Scala.

1 Like

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?

Regardless, your approach is interesting!

I filed an issue.

Here is a simplified version.