Scala - вычитание двух натуральных чисел на уровне типа - PullRequest
Новая
       43

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

0 голосов
/ 16 декабря 2018

Мы можем кодировать сложение и умножение натуральных чисел в 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 in 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. Возможно, этого можно достичь только путем кодирования отрицательного аналога натуральных чисел?

ps Меня не волнует, что произойдет, когда m > n in 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]

1 Ответ

0 голосов
/ 16 декабря 2018

Поскольку рекурсивное определение для вычитания совпадает со вторым аргументом, вы можете определить: 

sealed trait Natural {
  type ThisType <: Natural  
  type Previous <: Natural
  type Minus[That <: Natural] = That#SubtractThis[ThisType]
  type SubtractThis[That <: Natural] <: Natural
}

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

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