Type Driven Development with Idris presents the following generic adder approach:
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))
Example:
-- 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
I'm guessing that shapeless can handle the above generic adder
function.
How can it be written in Scala with or without shapeless?
Update: I'll leave my original implementation below, but here's one that's a little more direct:
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)
}
}
And then:
scala> val at3 = AdderType[Nat._3](0)
at3: Int => (Int => (Int => Int)) = <function1>
scala> at3(3)(3)(3)
res8: Int = 9
Original answer below.
Here's an off-the-cuff Scala translation:
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)
}
And then:
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
It's more verbose and the representation is a little different to get the Scala syntax to work out—our "base case" is essentially an Int => Int
instead of an Int
because otherwise I don't see a way to avoid needing to write apply
or ()
everywhere—but the basic ideas are exactly the same.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With