从 Idris 到 Scala 的通用加法器？

Question

Type Driven Development with 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

我猜 shapeless 可以处理上面的通用 adder 函数。

在有或没有 shapeless 的情况下如何用 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 语法生效，表示有点不同——我们的 "base case" 本质上是一个 Int => Int 而不是 Int 因为否则我不看到一种避免需要在任何地方写 apply 或 () 的方法——但基本思想完全相同。

Answer 2

如果您正在长途旅行并且手头没有 shapeless，那么您可以在纯 Scala 中执行此操作。对于不熟悉 shapeless 以及出于某种原因不使用它的人来说，它可能很有用。

首先，我们需要一些方法来迭代类型，即在类型中表示自然数。您可以使用任何嵌套类型或只定义一个带有数字别名的新类型：

sealed trait Nat

trait Zero extends Nat
trait Succ[N <: Nat] extends Nat

// enough for examples:
type _0 = Zero
type _1 = Succ[_0]
type _2 = Succ[_1]
type _3 = Succ[_2]
type _4 = Succ[_3]
// etc...

当然，如果你会经常使用像_42和_342923这样的类型，那么更使用现有的Nat ] 键入一些宏魔法来从值构造那些值，但对于我们的示例来说就足够了。

现在，AdderType 依赖函数类型非常简单：

// first we define the type which take a Nat type argument
trait AdderType[N <: Nat] {

  type Out
  def apply(i: Int): Out
}

// then we inductively construct its values using implicits
case object AdderType {

  // base case: N = _0
  implicit def zero:
      AdderType[_0] { type Out = Int } =
  new AdderType[_0] {

    type Out = Int
    def apply(i: Int): Out = i
  }

  // induction step: N -> Succ[N]
  implicit def succ[N <: Nat, NOut](
    implicit prev: AdderType[N] { type Out = NOut }
  ):  AdderType[Succ[N]] { type Out = Int => NOut } =
  new AdderType[Succ[N]] {

    type Out = Int => NOut
    def apply(i: Int): Out = k => prev(i + k)
  }
}

现在，为了构建 AdderType 的实例并应用它，我们编写了一个函数，该函数将 N <: Nat 作为类型参数并隐式构造 AdderType[N]:

def adder[N <: Nat](initial: Int)(
  implicit adderFunction: AdderType[N]
): adderFunction.Out = adderFunction(initial)

就是这样：

scala> val add3Numbers = adder_[_3](0)
add3Numbers: Int => (Int => (Int => Int)) = <function1>

scala> add3Numbers(1)(2)(3)
res0: Int = 6

您可以看到，纯解决方案并不比使用 shapeless 的解决方案更大或更复杂（尽管后者为我们提供了即用型 Nat和 DepFn 类型）。

一点补充：如果（在一些更一般的情况下）你不想使用adderFunction.Out，这有时会导致问题，我也有一个没有它的解决方案。在这个特殊情况下它并没有更好，但我还是会展示它。

关键是要为输出类型添加另一个类型参数：adder[N <: Nat, NOut]，但不能将N作为类型传递给adder，因为我们将需要写 NOut，它想要被推断（否则，有什么意义）。所以我们可以传递一个额外的值参数，这将有助于派生 N type:

def adder[N <: Nat, NOut](n: NatVal[N])(initial: Int)(
  implicit adderFunction: AdderType[N] { type Out = NOut }
): NOut = adderFunction(initial)

构造NatVal[N]我们不需要为每个Nat类型创建一个实例，我们可以使用一个小技巧：

// constructing "values" to derive its type arg
case class NatVal[N <: Nat]()

// just a convenience function
def nat[N <: Nat]: NatVal[N] = NatVal[N]()

下面是您的使用方法：

scala> val add3Numbers = adder(nat[_3])(0)
add3Numbers: this.Out = <function1>

scala> add3Numbers(1)(2)(3)
res1: this.Out = 6

您可以看到它有效，但没有向我们展示实际类型。然而，当您有多个依赖于其他类型成员的隐式时，这种方法可以更好地工作。我是说

def foo[AOut]()(implicit
  a: A { type Out = AOut},
  b: B { type In = AOut }
) ...

而不是

def foo()(implicit
  a: A,
  b: B { type In = a.Out }
) ...

因为您不能在同一个参数列表中引用 a.Out。

您可以在 Github 上的 repo 中找到完整代码。

从 Idris 到 Scala 的通用加法器？

Generic Adder from Idris to Scala?

scala

shapeless

idris