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 '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.

  • $\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 '10 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 '10 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 '10 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, privacy policy and cookie policy

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