Polyvariadic functions in Haskell

Polyvariadic Functions

This is a write-up of a conversation from the June 2015 Haskell meetup, where Leo and others were kicking around the idea that it would be nice to be able to write a web framework that could do this:

main = do
  get "/add" ["a", "b"] ((+) :: Int -> Int -> Int)
  get "/hello" ["name"] ("hello" ++)

The framework would be able to tell what types of parameters the handlers need based on their types - /add would take two ints from parameters named a and b respectively, and /hello would take one string called name. In either case, the response would be something of type (Respondable a) => a. Simple handler like these would return a primitive type, and more complicated handlers would return a WAI Response object.

To pull this off, the framework would need to be able to understand the types of the arguments involved. We know that Haskell can do something like this, based on the printf function and a tutorial by Oleg that we don't really understand yet.

Building a variadic fold function

Albert walked us through some of the key ideas, using a rather more accessible tutorial from ML that builds a variadic fold function such that:

fold (a, f) (step0 h1) (step0 h2) ... (step0 hn) $
= f (hn (... (h2 (h1 a))))

So for example, you could use it to write a function sum that added up its arguments like so:

sum (p 1) (p 2) (p 3) $ = 6

and in ML, the syntax allows you to write it more neatly as

sum `1 `2 `3 $ = 6

So we start with 3 functions as follows:

fold :: (a,a->b) -> ((a,a->b) -> c) -> c
fold (a,f) g = g (a,f)

step0 :: (a->a) -> (a,a->b) -> ((a,a->b) -> c) -> c
step0 h (a,f) = fold (h a, f)

end :: (a,a->b) -> b
end (a,f) = f a

The general idea is that we are going to carry around a pair (a,f) of type (a,a->r), where a is an accumulator, and f is a termination function that is just passed down the line until it's called with a just before it falls off the end. I'm assuming this function is normally id.

Mathematical Interlude

Before we define sum in terms of these three functions, let's prove the theorem we stated earlier, which is that:

fold (a, f) (step0 h1) (step0 h2) ... (step0 hn) end
= f (hn (... (h2 (h1 a))))

We'll use induction. The base case is:

  fold (a,f) end
= end (a,f) -- by definition of fold
= f a       -- by definition of end

The induction case has induction hypothesis:

(ih)    fold (a,f) (step0 h1) ... (step0 hn) end = f (hn (... (h1 x))

So adding an h0 to the start, we get:

  fold (a,f) (step0 h0) (step0 h1) ... (step0 hn) end
= step0 h0 (a,f) (step0 h0) (step0 h1) ... (step0 hn) end -- defn. of fold
= fold (h0 a,f) (step0 h1) ...(step0 hn) end              -- defn. of step0
= f (hn (... (h1 (h0 a))))                                -- induction hyp.
[]

Adding up numbers

OK, so let's use this to build a variadic sum function. Remember that we wanted to say sum (p 1) (p 2) (p 3) end and have it return 6. Here's how we define sum and a.

mysum :: Num a => ((a,a->a) -> c) -> c
mysum = fold (0,id)

p :: Num a => a -> (a,a->b) -> ((a,a->b) -> c) -> c
p i = step0 (i +)

So let's walk through an evaluation of this expression:

sum (p 1) (p 2) (p 3) end

The pair (0,id) goes in at the left hand side, and we get:

fold (0,id) (p 1) (p 2) (p 3) end

Then fold evaluates this to

p 1 (0,id) (p 2) (p 3) end

By definition of p and step0, we get

step0 (1+) (0,id) (p 2) (p 3) end
= fold (1+0,id) (p 2) (p 3) end
= fold (1,id) (p 2) (p 3) end

Now we are back to a fold expression, but the accumulator has an updated value. Proceeding:

= p 2 (1,id) (p 3) end
= step0 (2+) (1,id) (p 3) end
= fold (3,id) (p 3) end
= p 3 (3,id) end
= step0 (3+) (3,id) end
= fold (6,id) end

Now we're out of (p n) expressions, so end kicks in:

= end (6,id)
= id 6
= 6

Yay!

Some things I don't understand yet

1. What is the type c in the types of fold and step0 doing? It should be (a,a->r) because then the final output of fold would match the input of end. But if I make the substitution, it doesn't typecheck.

2. What's the point of the f half of the (a,f) pair? The whole thing is 100 times simpler without it:

    ```
    fold :: a -> (a -> b) -> b
    fold a g = g a
   
    step0 :: (a->a) -> a -> (a -> b) -> b
    step0 h a = fold (h a)
   
    end :: a -> a
    end = id
   
    mysum :: Num a => (a -> b) -> b
    mysum = fold 0
   
    p :: Num a => a -> a -> (a -> b) -> b
    p i = step0 (i +)
    ```
   

   Note that the definition end = id gives a shout out to the first paragraph of Oleg's article: "The simplest polymorphic function, the identity, is already polyvariadic"

3. It's easy to intuit that we could use this general idea to solve our problem, but much less obvious how to actually do that. But on the plus side, Oleg's tutorial might be a bit easier to read now!