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?