# Type a variable-argument function?

Is it possible to type a variable-argument function?

EDIT: like those defined in Scheme.

• 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 cstheory.stackexchange.com/faq Sep 27 '10 at 16:55

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.

• Thanks, that's wonderful. But I think it better to change the first equation of `sum' to: sum {0} a = 0
– day
Sep 27 '10 at 19:05
• @plmday: That would make it ignore the first argument, so sum 1 2 would evaluate to 2! Sep 27 '10 at 19:31
• 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
Sep 27 '10 at 19:46