Is it possible to type a variable-argument function?

EDIT: like those defined in Scheme.

  • 6
    $\begingroup$ 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 $\endgroup$ Sep 27, 2010 at 16:55

2 Answers 2


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.

  • $\begingroup$ Thanks, that's wonderful. But I think it better to change the first equation of `sum' to: sum {0} a = 0 $\endgroup$
    – day
    Sep 27, 2010 at 19:05
  • $\begingroup$ @plmday: That would make it ignore the first argument, so sum 1 2 would evaluate to 2! $\endgroup$
    – fishlips
    Sep 27, 2010 at 19:31
  • $\begingroup$ Ah, yeah, silly I am. Could you explain how the 'dynamic' arity is tracked since I see 'x' in 'sum' is declared as implicit. $\endgroup$
    – day
    Sep 27, 2010 at 19:46

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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.