Implementing Powerlists

June 13th, 2008 by Wouter

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.

Leave a Reply