Polyvariadic functions and keyword arguments

Introduction

At first sight, functions with the variable number of arguments of different types appear impossible to define in a typed language, without resorting to dependent types. In reality, we only need polymorphism. The simplest polymorphic function, the identity, is already polyvariadic:


     id id id id id True
     -- True
     id (\\k -> k 1) (\\v k -> k (v,True)) (\\v k -> k (v,"str")) id
     -- ((1,True),"str")
     
     let go = flip ($)
         begin = go ()
         push x s = go (x,s)
         add (x,(y,s)) = go (x+y,s)
         mul (x,(y,s)) = go (x*y,s)
     in begin (push 1) (push 2) (push 3) mul (push 4) add add id
     -- (11,())

The trick is to arrange for the return type of the function to be a type variable. It can always be instantiated to an arrow type, letting the function accept one more argument. Functions in the continuation-passing style are naturally polymorphic in the return, that is, the answer-type. Danvy's Functional Unparsing is the clearest demonstration of the technique.

On this page we collect more elaborate applications. The key idea is that the concrete type of a polymorphic term is determined by the context into which the term is placed. Pattern-matching on that concrete type lets the term determine the context of its use: specifically, the term can determine the number and the types of the values it receives as arguments, and what is expected in return. The term uses that information to chose the appropriate operation. For example, given


    class C a where
         f :: String -> a