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

[theiced.livejournal.com]

можно. (defn sum [n & rest] ....) - только вот зачем н передавать и делать за кампухтир его работу :)

[bwbwbw.livejournal.com]

А так не пойдет?
add : Int -> (n:Nat) -> sumType n
add acc Z = acc
add acc (S k) = \x => add (x + acc) k

[voidex.livejournal.com]

Это ж не статика

[dima-starosud.livejournal.com]

Наверное нельзя, поскольку постоянно передается аккумулятор. Просматривается аналогия с обеспечением хвостовой рекурсии, где тоже вводится дополнительная функция с аккумулятором.

[dima-starosud.livejournal.com]

Можно чуть упростить:

Add : ℕ → Set
Add zero = ℕ
Add (suc n) = ℕ → Add n

add : ∀ n → Add n
add = helper 0
  where
    helper : ∀ acc n → Add n
    helper acc zero = acc
    helper acc (suc n) = λ x → helper (acc + x) n

[109.livejournal.com]

int Add(params int[] p) { return p.Sum(); }

извините :)

[dima-starosud.livejournal.com]

int add(int n, ...) { /* тут уж сами напишите :-D */ }

[109.livejournal.com]

ни фига, Sum - это стандартная библиотека. но и без Sum ненамного длиннее.

[gds.livejournal.com]

проблемы начнутся тогда, когда типы аргументов внезапно будут не совсем одинаковыми.

[109.livejournal.com]

это да. нету типа ISummable, или там INumber, поэтому красиво не получится.

[wizzard]

и ведь не поправишь же, вот что удручает!

monomorphism restriction, впрочем, недалеко ушло...

[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 → ℕ, ну ты понял

[theiced.livejournal.com]

зато просто и в одну строку.

[thedeemon.livejournal.com]

Не, лишний аргумент для 0 параметров, странный порядок для остальных.

[thedeemon.livejournal.com]

Список чисел я и тут мог бы передать, это не интересно.

[thedeemon.livejournal.com]

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

[voidex.livejournal.com]

Дык sum = foldr 0 (+) ещё проще и статика. Но автор-то не того хотел.

[voidex.livejournal.com]

А sumType можно описать как-то так (псевдокод)?

sumType : Nat -> Type
sumType n = foldr (-> Int) (->) $ replicate n Int

[ilya-portnov.livejournal.com]

А тайпклассы в идрисе есть? Если есть — то можно сделать как Text.Printf в х-ле :) Ну или вобще, для данного случая нарисовать реализацию тайпкласса через record.

[thedeemon.livejournal.com]

D:

int sum(int[] xs ...) { return xs.reduce!"a + b"; }

[thedeemon.livejournal.com]

Тайпклассы есть. Я как раз и хочу простенький printf сделать.

[thedeemon.livejournal.com]

Можно так:

sumType2 : Nat -> Type
sumType2 n = foldr f Int $ List.replicate n Int where
               f a b = a -> b

Определение компиляется и в репле работает, но при попытке использования в коде выше что-то не срастается в унификации.

[deni-ok.livejournal.com]

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

[thedeemon.livejournal.com]

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

[thedeemon.livejournal.com]

В менее игрушечном примере (см. следующий пост) вместо n передается format string, там уже ничего лишнего за компьютер не делается, наборот, компьютер за меня проверяет, что ничего не забыто.

[109.livejournal.com]

нет, params это не список, это как раз, как у тебя - variable number of arguments.

[thedeemon.livejournal.com]

Да, точно, я потом уже заметил.
Но все равно не подходит для менее игрушечной задачи, где типы разные.

[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 - функция.

Функция с переменным числом параметров

[livejournal.livejournal.com]

Пользователь sassa_nf сослался на вашу запись в записи «Функция с переменным числом параметров (http://sassa-nf.livejournal.com/17828.html)» в контексте: [...] Прозвучал интересный вопрос: Сумма N чисел [...]

[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)

[dima-starosud.livejournal.com]

Где-то я уже это [видел] смотрю )))))))
infoq.com/presentations/scala-idris