Looking Out To Sea

I’m in a new job. I’ve done one week, so my life has mostly been on hold while I work out how things will fit together. I’m working for Honeywell Security writing embedded software. Similar to before but in alarm systems instead of networking.

The job requires a hefty commute — at least two hours each way if things go well, but between delayed trains and poor weather it’s sometimes an extra half hour on top of that. Which means I get up at 5.30, leave the house before 6.30 and get home in the evening around 7 o’clock. You can see why the rest of my life has been a bit quiet. I’m having to rethink how I look at the week. The arrival of the weekend is important and precious!

I’m still learning the ins and outs of work but the people are all very friendly and helpful, which makes the travelling more bearable. Spending hours travelling to and from a hateful job would be horrible. I spend an hour on the train each way which has given me more time for other things. I’ve been splitting my travelling activities, so that in the morning I read the freebie Metro for a bit and then do some “thinking” to limber up for the day. Recently I’ve been doing simple program calculation exercises, deriving the fusion rules for fold/unfold or map/map and so on. I’m really interested in the idea of deriving correct and efficient programs from executable specification.

(Just to show you what I’m talking about, this is the fold/unfold fusion rule. Let us say there are two functions, foldr and unfoldr defined as follows:

foldr f z     [] = z
foldr f z (x:xs) = f (foldr f z xs)
 
unfoldr g s = case g s of
                Nothing     -> []
                Just (x,s') -> x : unfoldr g s'

The function foldr combines a list of elements according to the function f and unfoldr creates a list of elements from the seed s. We might use foldr to define a product function which combines the elements of the list by multiplying them together:

product = foldr (*) 1

And we might create a list of elements from 1 to n with an unfold.

enumTo n = unfoldr step 1
  where step s = if s>n then Nothing else Just (s, s+1)

The observant reader will have noticed that combining these two separate functions will give us factorial, the product of numbers from 1 to n — first we create the numbers 1 to n, then we multiply them all together.

factorial = product . enumTo

The inefficiency is that enumTo works on producing a list which is consumed by product. The elements are inserted into a list only to be removed straight away. Can we omit the redundant list production? It turns out we can, and we can do it for all cases where foldr operates on the result of unfoldr. The product and enumTo are specific instances of a general method which we can use to fuse production and consumption of values.

This fusion rule can be demonstrated by algebraic manipulation of the programs we’ve defined so far. We’ll call the unfoldr and then foldr by the name hylo, with the naive implementation shown:

hylo f z g = foldr f z . unfoldr g

The equational style here facilitates some nice rearrangements which help to assert their correctness from step to step. Let’s see how this works — each line will be justified by some comment in braces:

  hylo f z g s
= { definition from above }
  foldr f z (unfoldr g s)
= { definition of unfoldr }
  foldr f z (case g s of
                  Nothing     -> []
                  Just (x,s') -> x : unfoldr g s')
= { push foldr into result }
  case g s of
       Nothing     -> foldr f z []
       Just (x,s') -> foldr f z (x : unfoldr g s')
= { foldr on empty lists }
  case g s of
       Nothing     -> z
       Just (x,s') -> foldr f z (x : unfoldr g s')
= { foldr on non-empty lists }
  case g s of
       Nothing     -> z
       Just (x,s') -> f x (foldr f z (unfoldr g s'))
= { definition of hylo }
  case g s of
       Nothing     -> z
       Just (x,s') -> f x (hylo f z g s')

Each step should be clearly equivalent to the one before and the one after, but by the end we have a definition for hylo which doesn’t construct a useless list.

hylo f z g s = case g s of
                 Nothing     -> z
                 Just (x,s') -> f x (hylo f z g s')

Naturally we can use the original definitions of product and enumTo to create an optimised factorial using this logic. The result is that factorial doesn’t create a redundant list either:

factorial n = hylo (*) 1 step
  where step s = if s > n then Nothing else Just (s,s+1)

I think this is beautiful result despite its obvious simplicity. However this has been a long digression, so I’ll stop now. But if you found it interesting I encourage you to check out work on “program calculation”, “program derivation”, “algebra of programming”, “origami programming” and so on.)

My evening journeys have been spent unwinding with a book, though the evening trains are noisier. I’m reading Brighton Rock right now and it’s good though the story makes me feel quite uncomfortable at times. One of the characters seems close to doing something wild and dangerous and it’s a fight between “must find out what happens” and “can’t bear to read any more” on a daily basis.

I hope week two will be easier and I will start to feel like my routine is falling into place. Watch this space.