Implementing Powerlists
June 13th, 2008 by WouterI 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.