Scala — вычитание двух натуральных чисел на уровне типа

Мы можем кодировать сложение и умножение натуральных чисел в Scala. Но можно ли вычесть два натуральных числа на уровне типа?

Я наполовину скопировал следующую кодировку натуральных чисел в Scala:

sealed trait  Natural {
  type Plus[That <: Natural] <: Natural
}

case object Zero extends Natural {
  override type Plus[That <: Natural] = That
}

case class Suc[Prev <: Natural](n: Prev) extends Natural {
  override type Plus[That <: Natural] = Suc[Prev#Plus[That]]
}

Затем я добавил умножение самостоятельно:

sealed trait Natural {
  type Plus[That <: Natural] <: Natural
  type Mult[That <: Natural] <: Natural
}

case object Zero extends Natural {
  override type Plus[That <: Natural] = That
  override type Mult[That <: Natural] = Zero.type
}

case class Suc[Prev <: Natural](n: Prev) extends Natural {
  override type Plus[That <: Natural] = Suc[Prev#Plus[That]]
  override type Mult[That <: Natural] = (Prev#Mult[That])#Plus[That]
}

Который, кажется, соответствует другим реализациям, которые я позже нашел, и также работает правильно:

implicitly[Nat5#Mult[Nat2] =:= Nat10]
implicitly[Nat4#Mult[Nat4] =:= Nat8#Mult[Nat2]]

В течение последних часов я пытался реализовать вычитание. При следующем подходе я, кажется, могу правильно вычесть два числа, если тот, который вы вычитаете (b в a - b), является нечетным числом:

sealed trait  Natural {
  type Previous <: Natural
  type Minus[That <: Natural] <: Natural
}

case object Zero extends Natural {
  override type Previous = Zero.type
  override type Minus[That <: Natural] = That
}

case class Suc[Prev <: Natural](n: Prev) extends Natural {
  override type Previous = Prev
  override type Minus[That <: Natural] = (That#Previous)#Minus[Prev]
}

Вышеизложенное использует тот факт, что (N - M) = (N - 1) - (M - 1). В конце концов, шаг рекурсии M достигнет Zero.type и вернет соответствующий шаг рекурсии N. На самом деле, обратите внимание, что моя реализация на данном этапе преобразуется в (N - M) = (M - 1) - (N - 1). Поскольку вычитание не является коммутативным, это неверно; но, поскольку этот "перестановка" происходит на каждом рекурсивном шаге, он отменяется, если вычитаемое число нечетное. Если это четное число, то эта реализация отличается на единицу. В частности, оно на единицу меньше правильного числа:

implicitly[Nat10#Minus[Nat3] =:= Nat7]  // Compiles
implicitly[Nat9#Minus[Nat3] =:= Nat6]   // Compiles
implicitly[Nat8#Minus[Nat3] =:= Nat5]   // Compiles

implicitly[Nat10#Minus[Nat2] =:= Nat8]  // Does not compile, while:
implicitly[Nat10#Minus[Nat2] =:= Nat7]  // Compiles

implicitly[Nat5#Minus[Nat2] =:= Nat3]  // Does not compile, while:
implicitly[Nat5#Minus[Nat2] =:= Nat2]  // Compiles

Чтобы понять почему, попробуйте на бумаге с m = Suc[Zero.type] (Nat1) для нечетного/правильного случая и m = Suc[Suc[Zero.type]] (Nat2) для неправильного сценария. В любом случае число n (как и в n - m не важно)

Во всяком случае, у меня есть ощущение, что я могу быть на правильном пути с этим подходом, но я застрял.

1. У вас есть идеи, как это сделать? Может быть, вы можете указать мне на реализацию вычитания на уровне типа?
2. Возможно, этого можно добиться, только закодировав отрицательную копию натуральных чисел?

p.s. Меня не волнует, что происходит, когда m > n в n - m.

Полезно для опробования примеров на реплике:

type Nat0  = Zero.type  
type Nat1  = Suc[Nat0]  
type Nat2  = Suc[Nat1]  
type Nat3  = Suc[Nat2]  
type Nat4  = Suc[Nat3]  
type Nat5  = Suc[Nat4]  
type Nat6  = Suc[Nat5]  
type Nat7  = Suc[Nat6]  
type Nat8  = Suc[Nat7]  
type Nat9  = Suc[Nat8]  
type Nat10 = Suc[Nat9]  
type Nat11 = Suc[Nat10]