Verified tail-recursive folds through dissection

Abstract

The functional programming paradigm advocates a style of programming based on higher-order functions over inductively defined datatypes. A fold, which captures their common pattern of recursion, is the prototypical example of such a function. However, its use comes at a price. The definition of a fold is not tail-recursive which means that the size of the stack during execution grows proportionally to the size of the input. McBride has proposed a method called dissection, to transform a fold into its tail-recursive counterpart. Nevertheless, it is not clear why the resulting function terminates, nor it is clear that the transformation preserves the fold’s semantics. In this thesis, we formalize the construction of such tail-recursive function and prove that it is both terminating and equivalent to the fold. In addition, using McBride’s dissection, we generalize the tail-recursive function to work on any algebra over any regular datatype.