Inverses are (horrible)-1

This section gives an introduction to the extremely interesting concept of implementing a function as the inverse of another with zip and unzip as the examples. First, the goal is to build out our zip and unzip functions to satisfy the equation
zip . unzip = id

A couple of notes here. Previously everything has been defined in terms of Haskell, but this is simply an equation. Also, if you're coming from a non-functional background, id is a function that gives you back the same thing you pass to it. No matter what. In this case the equation is meant to point out that, if you give unzip a list of pairs (two element tuples) and give that result, a tuple of two lists, to zip, in the end you'll get back the original list of pairs. So zip compose unzip is equivalent to the id function. You get back just what you gave it.
zip $ unzip [(1,2), (3,4)] = [(1,2), (3,4)]

Before we get into why this is immediately useful lets define the two functions as the book does, but with Haskell.
data Listr a = Empty | Cons (a, Listr a) deriving Show

foldr' c h Empty = c
foldr' c h (Cons (a, x)) = h a $ foldr' c h x

Our old friends the Cons list and foldr here. If you're new to these you can check out more information on them here.
unzip' :: Listr (a, b) -> (Listr a, Listr b)
unzip' = foldr' emptys conss
        where emptys = (Empty, Empty)
              conss (a, b) (x, y) = (Cons (a, x) , Cons (b, y))

unzip_' :: Listr (a, b) -> (Listr a, Listr b)
unzip_' Empty = (Empty, Empty)
unzip_' (Cons ((a,b), x)) = (Cons (a, left $ unzip_' x), Cons (b, right $ unzip_' x))
                           where left (x, y) = x
                                 right (x, y) = y

unzip' and unzip_' represent two possible ways of unzipping a list of pairs. Of interest here is the fact that my own, much less efficient, implementation involves two "folds" over the data structure, and the one implemented in the book only requires one. Apparently, any and all functions defined by a pair of folds can be defined in terms of a single fold (to be demonstrated later in the book).
zip' :: (Listr a, Listr b) -> Listr (a, b)
zip' (Empty, _) = Empty
zip' (_, Empty) = Empty
zip' (Cons (a, x), Cons (b, y)) = Cons ( (a, b) , zip' (x, y) )

-- > let x = zip' . unzip'
-- > x  $ Cons ((1, 'a'), Cons ((2, 'b'), Empty))

-- Cons ((1,'a'),Cons ((2,'b'),Empty))

-- > let y = zip' . unzip_'
-- > y  $ Cons ((1, 'a'), Cons ((2, 'b'), Empty))

-- Cons ((1,'a'),Cons ((2,'b'),Empty))

Finally we have an exhaustive (can handle lists of different lengths) definition of zip' and the results of composing zip' with unzip' and unzip_' using ghci.

Testing with maths

If you know how zip and unzip work its not imperative (though it is fun) to walk yourself through how each of them operates as defined here. What is important is the result we've gotten out of ghci. We've composed our two functions, and as stated above in our original equation we've gotten back the very same thing we put in. Just as though it were the id function. I had originally wanted to build my own "foldrless" version of unzip_ in the hopes that it would be easier to see the "inversity" in the code itself. Unfortunately its not incredibly clear, and whats worse the implementation isn't extremely efficient. BUT! Its not a total loss, because in order to satisfy myself that my hack was working properly, all I had to do was run the results BACK through zip and see if I got the original Cons list out the other side to satisfy our original assertion. And that's really the sweet spot here. While its not a formal proof of the functionality, it provides us with a lot of confidence that our functions are working properly. By defining the function as the inverse of another function we get a way to build it and test it. Incredible.


26 Sep 2009