Сумма 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

[thedeemon.livejournal.com]

Вместо одной дополнительной функции две. Плохое упрощение. :)

[deni-ok.livejournal.com]

Зато короткое!
Правильный компилятор (tm) должен выполнить статический контроль и сделать fusion.

[thedeemon.livejournal.com]

Ну, на самом деле наличие библиотечного решения игрушечной задачи не особо помогает в менее игрушечной, см. следующий пост.