Constraints to stop deforestation

Wadler's deforestation algorithm eliminates intermediate data structures from functional programs. To be suitable for inclusion in a compiler, deforestation must terminate on all programs. Several techniques exist to ensure termination of deforestation on all first-order programs, but general techniques for higher-order programs were introduced only recently first by Hamilton and then by Marlow. We present a new technique for ensuring termination of deforestation on all higher-order programs that allows useful transformation steps prohibited in Hamilton's and Marlow's techniques. The technique uses a constraint-based higher-order control-flow analysis. We also relate our technique to previous approaches to termination of first- and higher-order deforestation in some detail.