从Idris到Scala的通用加法器？

Question

使用Idris进行类型驱动开发提供了以下通用加法器方法:

AdderType : (numArgs : Nat) -> Type
AdderType Z     = Int
AdderType (S k) = (next : Int) -> AdderType k

adder : (n : Nat) -> (acc : Int) -> AdderType n
adder Z acc     = acc
adder (S k) acc = \x => (adder k (x+acc))

例:

-- expects 3 Int's to add, with a starting value of 0
*Work> :t (adder 3 0) 
adder 3 0 : Int -> Int -> Int -> Int

-- 0 (initial) + 3 + 3 + 3 == 9
*Work> (adder 3 0) 3 3 3
9 : Int

我猜测无形可以处理上面的泛型adder函数.

无论是否有无形,它如何用Scala编写？

Answer 1

更新:我将保留下面的原始实现,但这里有一个更直接的实现:

import shapeless._

trait AdderType[N <: Nat] extends DepFn1[Int]

object AdderType {
  type Aux[N <: Nat, Out0] = AdderType[N] { type Out = Out0 }
  def apply[N <: Nat](base: Int)(implicit at: AdderType[N]): at.Out = at(base)

  implicit val adderTypeZero: Aux[Nat._0, Int] = new AdderType[Nat._0] {
    type Out = Int
    def apply(x: Int): Int = x
  }

  implicit def adderTypeSucc[N <: Nat](implicit
    atN: AdderType[N]
  ): Aux[Succ[N], Int => atN.Out] = new AdderType[Succ[N]] {
    type Out = Int => atN.Out
    def apply(x: Int): Int => atN.Out = i => atN(x + i)
  }
}

然后:

scala> val at3 = AdderType[Nat._3](0)
at3: Int => (Int => (Int => Int)) = <function1>

scala> at3(3)(3)(3)
res8: Int = 9

原答案如下.

这是一个不受欢迎的Scala翻译:

import shapeless._

trait AdderType[N <: Nat] extends DepFn1[Int] {
  protected def plus(x: Int): AdderType.Aux[N, Out]
}

object AdderType {
  type Aux[N <: Nat, Out0] = AdderType[N] { type Out = Out0 }

  def apply[N <: Nat](base: Int)(implicit at: AdderType[N]): Aux[N, at.Out] =
    at.plus(base)

  private[this] case class AdderTypeZero(acc: Int) extends AdderType[Nat._1] {
    type Out = Int
    def apply(x: Int): Int = acc + x
    protected def plus(x: Int): Aux[Nat._1, Int] = copy(acc = acc + x)
  }

  private[this] case class AdderTypeSucc[N <: Nat, Out0](
    atN: Aux[N, Out0],
    acc: Int
  ) extends AdderType[Succ[N]] {
    type Out = Aux[N, Out0]
    def apply(x: Int): Aux[N, Out0] = atN.plus(acc + x)
    protected def plus(x: Int): Aux[Succ[N], Aux[N, Out0]] = copy(acc = acc + x)
  }

  implicit val adderTypeZero: Aux[Nat._1, Int] = AdderTypeZero(0)
  implicit def adderTypeSucc[N <: Nat](implicit
    atN: AdderType[N]
  ): Aux[Succ[N], Aux[N, atN.Out]] = AdderTypeSucc(atN, 0)
}

然后:

scala> val at3 = AdderType[Nat._3](0)
at3: AdderType[shapeless.Succ[shapeless.Succ[shapeless.Succ[shapeless._0]]]] { ...

scala> at3(3)(3)(3)
res0: Int = 9

它更冗长,表示与Scala语法有所不同 - 我们的"基本情况"本质上是一个Int => Int而不是一个Int因为否则我没有看到一种方法来避免需要写apply或()无处不在 - 但基本想法完全一样.