Nottingham FP Lab Blog

Implementing Powerlists

by Wouter on June 13, 2008.
Tagged as: Lunches.

I talked about a short program I wrote, inspired by a really nice paper by Jay Misra, Powerlist: A Structure for Parallel Recursion. The paper describes a common pattern underlying many divide-and-conquer algorithms on lists of length 2^k, for some k. There are two ways to divide such powerlists into two pieces:

Split the list down the middle;
Or separate the elements at odd and even indices

There is no clear ‘best’ choice—sometimes you want the one, sometimes you want the other.

I showed how to implement powerlists in Agda. The trick is, of course, to define a clever view. I’ve put the source code on my website, in case anyone wants to have a closer look.