<p>Here's a link describing how to do it in Haskell <a href="http://okmij.org/ftp/Haskell/polyvariadic.html#polyvar-fn" rel="nofollow">http://okmij.org/ftp/Haskell/polyvariadic.html#polyvar-fn</a></p>

<p>Other languages have variadic functions, too: <a href="http://en.wikipedia.org/wiki/Variadic_function" rel="nofollow">http://en.wikipedia.org/wiki/Variadic_function</a></p>

CC BY-SA 2.5
2010-09-27T16:58:38.727Z
2010-09-27T16:58:38.727Z
Dave Clarke
<p>Such functions can be typed in dependently typed programming languages (among others).</p>

<p>This is an example in <a href="http://wiki.portal.chalmers.se/agda/">Agda</a>, a dependently typed language that looks similar to Haskell:</p>

<pre><code>more : Nat -&gt; Set
more 0 = Nat
more (S x) = Nat -&gt; more x


sum : \forall {x : Nat} -&gt; Nat -&gt; more x
sum {0}   a = a
sum {S x} a = \lambda m -&gt; sum {x} (m + a)
</code></pre>

<p>The function sum takes x natural numbers as arguments and returns with the sum of all arguments. The S in the pattern matches is the "successor" constructor on the natural numbers.</p>

<p>Note: Agda has a much nicer Unicode syntax, but most browsers can't display it correctly.</p>

CC BY-SA 2.5
2010-09-27T19:05:23.100Z
Thanks, that's wonderful. But I think it better to change the first equation of `sum' to:

sum {0}   a = 0
day
CC BY-SA 2.5
2010-09-27T19:31:23.920Z
@plmday: That would make it ignore the first argument, so sum 1 2 would evaluate to 2!
fishlips
CC BY-SA 2.5
2010-09-27T19:46:48.120Z
Ah, yeah, silly I am. Could you explain how the 'dynamic' arity is tracked since I see 'x' in 'sum' is declared as implicit.
day
CC BY-SA 2.5
2010-09-27T18:56:01.787Z
2010-09-27T18:56:01.787Z
fishlips
<p>Is it possible to type a variable-argument function?</p>

<p>EDIT: like those defined in Scheme.</p>

CC BY-SA 2.5
2010-09-27T16:55:26.987Z
You might want to add a little more context, try to improve your question, make it easier for people to understand what you are asking, and why you are asking this. See the FAQ for more details http://cstheory.stackexchange.com/faq
Dave Clarke
<type-theory>
Type a variable-argument function?
day
# Type a variable-argument function?

(Asked by: username_0 on 2010-09-27)

Is it possible to type a variable-argument function?

EDIT: like those defined in Scheme.

**Tags:** type-theory
> **Comments:**
> **username_1**: You might want to add a little more context, try to improve your question, make it easier for people to understand what you are asking, and why you are asking this. See the FAQ for more details http://cstheory.stackexchange.com/faq  

---

## 2 answers

### Answer by username_2 on 2010-09-27. Score: 11 | Accepted answer

Such functions can be typed in dependently typed programming languages (among others).
This is an example in Agda, a dependently typed language that looks similar to Haskell:
more : Nat -> Set
more 0 = Nat
more (S x) = Nat -> more x


sum : \forall {x : Nat} -> Nat -> more x
sum {0}   a = a
sum {S x} a = \lambda m -> sum {x} (m + a)

The function sum takes x natural numbers as arguments and returns with the sum of all arguments. The S in the pattern matches is the "successor" constructor on the natural numbers.
Note: Agda has a much nicer Unicode syntax, but most browsers can't display it correctly.

> **Comments:**
> **username_0**: Thanks, that's wonderful. But I think it better to change the first equation of `sum' to:  sum {0}   a = 0  
> **username_2**: @plmday: That would make it ignore the first argument, so sum 1 2 would evaluate to 2!  
> **username_0**: Ah, yeah, silly I am. Could you explain how the 'dynamic' arity is tracked since I see 'x' in 'sum' is declared as implicit.  

---

### Answer by username_1 on 2010-09-27. Score: 7

Here's a link describing how to do it in Haskell <http://okmij.org/ftp/Haskell/polyvariadic.html#polyvar-fn>

Other languages have variadic functions, too: <http://en.wikipedia.org/wiki/Variadic_function>


---

