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

[deni-ok.livejournal.com]

Можно воспользоваться стандартной библиотекой :)

open import Data.Vec
open import Data.Vec.N-ary
open import Function

add : ∀ n → N-ary n ℕ ℕ
add n = curryⁿ $ sum {n}

Слегка обобщенный sumType - это N-ary, который далее каррируется в вектор и сворачивается библиотечной же sum : ∀ {n} → Vec ℕ n → ℕ

[deni-ok.livejournal.com]

Тьфу, язык заплетается, каррируется в N-арку, конечно, функция над вектором Vec ℕ n → ℕ, ну ты понял

[thedeemon.livejournal.com]

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

[deni-ok.livejournal.com]

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

[thedeemon.livejournal.com]

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