kirancodes.me
To Proof Maintenance & Beyond!

Concatenate, reverse and map vanish for free

Janis Voigtländer

Abstract

We introduce a new transformation method to eliminate intermediate data structures occurring in functional programs due to repeated list concatenations and other data manipulations (additionally exemplified with list reversal and mapping of functions over lists).The general idea is to uniformly abstract from data constructors and manipulating operations by means of rank-2 polymorphic combinators that exploit algebraic properties of these operations to provide an optimized implementation. The correctness of transformations is proved by using the free theorems derivable from parametric polymorphic types.

Related papers