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.

Lists

The third section of chapter one covered some basic functional programming concepts. Namely Cons lists, their mirror Snoc lists, and the functions built to operate on them. Particularly the adaptations of the foldn function from the previous section which operated over Nat.

data Listl a = Nil | Snoc (Listl a, a) deriving Show
data Listr a = Empty | Cons (a, Listr a) deriving Show 

foldl' c h Nil = c
foldl' c h (Snoc (x, a)) = h (foldl' c h x) a

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

As you can see in the definition of both Cons and Snoc they are identical to the previous sections definition of natural numbers save for an addition bit of information, whatever you are storing in your list. Also, Cons and Snoc are only different in the position of their recursive self reference. It’s only the general understanding of the position by those using the type and the functions created for them ( : as an example ) that makes it behave the way it does. If you were, without prior knowledge, to examine the types by themselves it wouldn’t be clear that they were operated upon in significantly different ways when adding new elements (other than the difference in the names of the data constructor). As an example we could redefine the haskell infix cons operator to work with Snoc lists just as it would a Cons list (Note: I’ve been informed that in practice this isn’t possible, but the purpose of the example still holds).

data Listl a = Nil | Snoc (Listl a, a) deriving Show

(:) :: a -> Listl a -> Listl a
x : y = Snoc (y, x) 

example = 1 : Snoc(Snoc(Nil, 3), 2)
          --  Cons(2, Cons(1, Nil)) would be the norm

Also of interest in this chapter is the myriad of operations that can be defined in terms of foldr for Cons lists and foldl for Snoc lists, much as with Nat. From two of the excercises:

--Excercise 1.7
convert :: Listl a -> Listr a
convert = foldl' Empty h
    where h x y = Cons(y, x)

--Excercise 1.8
catconv :: Listl a -> Listr a -> Listr a
catconv m n = foldl' n h m
    where h x y = Cons(y, x)

Or a quick implementation of map’ for Cons lists built atop our extremely reusable foldr’

map' f = foldr' Empty h
    where h x y = Cons (f x, y)

-- > map' (+2) $ Cons (1, Cons(2, Empty))
-- Cons (3,Cons (4,Empty))

Further Work

I’m getting a lot of joy from rehashing these basic data structures and the implications of understanding them at a relatively low level are obvious. Lists make up such a huge portion of the programming that we do and understanding the types of lists that make the most sense for use within code for both comprehension and performance can provide real value. Also, in fooling around with some little coding challenges on the side (examples to be posted soon I hope) in haskell I’ve noticed my ease with maps and folds becoming greater.

One bit that I have to revisit is the proof from the middle of the section that the ++ operation is associative and that nil is the left and right unit. I was never very good with proofs, I’ve long since lost the terminology, and I would like to complete the exercise that requires that knowledge.

[update] you’ll notice I corrected the title to represent the section I went through. Not clear how I got the idea this was the whole first chapter.

My wife, bless her heart, heard me talking about Algebra of Programming after it was recommended to my by the fine people in #haskell and she went out and ordered a print on demand copy. You can do the same for yourself here (Note: the price at amazon.ca is much better than amazon.com).

Since my new job is working with Ruby, my free time can be devoted to other languages/projects and I’ve fallen under the spell of Haskell. As an example, Unraverl‘s partial application parse transform for Erlang grew out of my time spent learning about Haskell, and how useful partial application can be. And as a natural sort of progression I’ve gotten interested in how mathematics can play a larger roll in my programming.

Starting Out

I was initially a bit worried that I would be out of my depth with this book but I was also determined to do whatever was necessary to fill in the gaps of understanding. Luckily the first bit hasn’t been too difficult, as most of my questions have been around terminology which were quickly answered thanks, once again, to #haskell. As an aside, if you’re on the fence about which functional language to learn spend a couple minutes in haskell’s irc channel. Huge thanks to heatsink, c_wraith, and others.

Recursive Data Types

The second section of the first chapter is where things started to get exciting and dense. The first example of recursive data types they provide, that make the basis for the rest of the chapter, is natural numbers (all integers >= 0). In haskell it would look something like

data Nat = Zero | Successor Nat

To further explain how this can represent any natural number consider the following possible definitions of a function that represents the value 3

-- What we would normally do
three = 3

-- Another "unrolled" recursive definition using the + function
three = (1 + (1 + (1 + 0)))

-- Using our data type
three = (Successor (Successor (Successor Zero)))

When I attempted an explanation of this to my wife her question was a frustrating “Why?”. Of course, “because its cool” didn’t persuade her. First, it’s a definition for a set of numbers which involves no actual numbers, only the structure of our new data type. We’ve structurally defined natural numbers. Second, because we have a recursive representation we can define recursive functions for this data type, and more generic functions for other types that are similarly recursive.

The rest of the chapter is devoted to presenting the foldn function that provides a very generic way to perform operations over recursive data types like Nat.

-- In terms of numbers as you would use them normally
foldn c h 0 = c
foldn c h (n + 1) = h (foldn c h n)

-- In terms of our Nat data type
foldn c h Zero = c
foldn c h ( Successor n ) =  h (foldn c h n)

It should be noted here, as it confused me initially, that by providing (n + 1) or (Successor n) in the head of the function, n represents a value of one less than that which is passed in. So in the case that foldn was called with some c, some h and 6, n has the value 5 (since (5 + 1) is 6).

The fun part about this is that is provides a method by which you can define functions for addition, subtraction and exponentiation (and others) in terms of foldn. From the book:

-- Addition
plus m n = foldn m Successor n

-- Subtraction
mult m n = foldn 0 (plus m) n

-- Exponentiation
expn m n = foldn 1 (mult m) n

-- The more point free ("point-less"?) version, would be without the n's. 

If you’re a ruby developer you’ll recall the Comparable mixin. Each of the methods in Comparable is defined in terms of the method < =>, and once you’ve done that you get skads of additional functionality for free. Similarly here we’ve defined one function, significantly more generic than < =>, that can be used as the basis for many other functions.

Exercises

I’ve actually completed all the exercises save for the 1.4 and 1.6. For the first, I simply couldn’t provide h which requires knowing how to add n times in such a way that it results in the square of a number. As for the second, I haven’t taken the time. You can actually download the answers here, which has been wonderful for checking my answers and allowing me to enjoy the satisfaction of my failures and triumphs.

Elementary

Obviously this is only the first chapter and relatively simple (though not for me), but being able to go through it and grasp the concepts explained was extremely gratifying. Even more, seeing how those concepts apply to every day development gave me confidence that I can really get something out of this to apply to my personal projects. I hope to post here on each of the chapters so that I’m forced to verify my understanding of the material. Any corrections are greatly welcomed in the comments!