Сумма N чисел

[thedeemon]

Описанная ниже функция add принимает натуральное число n и n интов и возвращает сумму этих интов. Т.е.
add 0 == 0
add 1 42 == 42
add 2 33 44 == 77
add 8 2 2 2 2 2 2 2 2 == 16
Вот так она описывается на Идрисе:

sumType : Nat -> Type
sumType Z = Int
sumType (S k) = Int -> sumType k

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

add : (n:Nat) -> sumType n
add Z = 0
add (S k) = adder k 

Можно ли ее еще упростить и обойтись без вспомогательной функции adder? Че-то я торможу.

Comments

[sassa-nf.livejournal.com]

дык, как-то так вроде, нет?

add Z = 0
add (S Z) = ((add Z) +) -- could use id; this is a reduction step from a->sumType 0 to sumType 0
add (S k) = \ x y => add k (x + y) -- a general reduction step from b->a->sumType n to b->sumType n, eg k = S n

[thedeemon.livejournal.com]

Да!

Только последняя строчка такая:
add (S (S k)) = \x, y => add (S k) (x + y)

иначе он почему-то не догадывается, что k не Z, и потому не убежден, что add k - функция.

[sassa-nf.livejournal.com]

а, само собой. жаль, не умеет догадаться, что ведь (S Z) уже поматчено строкой выше. Но да, это типичный проблем.

[sassa-nf.livejournal.com]

кстати, можно ещё вот так переписать:

  folding : ∀ {n A} → (A → A → A) → sumT A (succ n)
  folding {zero} add z = z
  folding {(succ n)} add acc = λ x → folding {n} add (add acc x)

  add : (n : ℕ) → sumT ℕ n
  add n = folding {n} {ℕ} (_+_) zero

- здесь zero добавляется с другого боку. Хотя не соответствует условию "одной функцией", но этот folding уже adder (за вычетом обобщения) (также, тривиально обобщается до "настоящего" фолда с типом функции (B → A → B)