从Idris到Scala的泛型加法器？
基于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编写的，有无形状？
回答 2
Stack Overflow用户
发布于 2016-03-10 17:01:31
更新:我将在下面保留我最初的实现，但这里有一个更直接的实现：
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或() --但基本思想完全相同。
Stack Overflow用户
发布于 2016-03-11 17:56:59
如果您正在进行一次长途旅行，而且手上没有您的不成形的形状，下面是如何在纯Scala中实现这一点的方法。对于那些不熟悉无形体的人和那些由于某种原因而不使用它的人来说，它是有用的。
首先，我们需要某种方法来迭代类型，即在类型中表示自然数。您可以使用任何嵌套类型，也可以定义一个带有数字别名的新类型：
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您可以看到，纯解决方案并不比使用无形状的解决方案更大或更复杂(尽管后者提供了现成的Nat和DepFn类型)。
补充一点:如果(在更一般的情况下)您不想使用adderFunction.Out，这有时会导致问题，那么我也有一个没有它的解决方案。在这个特殊的情况下，它没有任何更好的，但我将展示它无论如何。
关键是为out类型添加另一个类型参数：adder[N <: Nat, NOut]，但不能将N作为类型传递给adder，因为我们需要编写希望推断的NOut (否则，重点是什么)。因此，我们可以传递一个额外的值参数，这将有助于派生N类型：
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。
你可以在我的存储库上找到完整的代码。
https://stackoverflow.com/questions/35907690
复制相似问题
腾讯云开发者
