Abstract

Lists are used throughout functional programming and the idea of defining lists with multiple heads for optimisation is almost as old as the subject itself. We present a theoretical justification for $\mathbb{N}$-indexed (multi-headed) lists as the natural datatypes that comes from unrolling the defining equation $X = 1 + A \times X$ for lists, and give $\mathbb{N}$-indexed implementations of functions that normally use intermediate lists and that satisfy certain conditions.

We then discuss staged metaprogramming and use this to speed up these functions so that they are at least as fast as their usual list counterparts. Our guiding examples will be tail-recursive $\map$ and $\filter$ for lists in OCaml.