Tail Recursion Modulo Context: An Equational Approach (extended version) - Leijen, Daan; Lorenzen, Anton (under submission to JFP., 2024)
The tail-recursion modulo _cons_ transformation can rewrite functions that are not quite tail-recursive into a tail-recursive form that can be executed efficiently. In this article we generalize tail recursion modulo _cons_ (TRMc) to modulo _contexts_ (TRMC), and calculate a general TRMC algorithm from its specification. We can instantiate our general algorithm by providing an implementation of application and composition on abstract contexts, and showing that our _context laws_ hold. We provide some known instantiations of TRMC, namely modulo _evaluation contexts_ (CPS), and _associative operations_, and further instantiations not so commonly associated with TRMC, such as _defunctionalized_ evaluation contexts, _monoids_, _semirings_, _exponents_, and _cons products_. We study the modulo _cons_ instantiation in particular and prove that an instantiation using Minamide's hole calculus is sound. We also calculate a second instantiation in terms of the Perceus heap semantics to precisely reason about the soundness of in-place update. While all previous approaches to TRMc fail in the presence of non-linear control (for example induced by call/cc, shift/reset or algebraic effect handlers), we can elegantly extend the heap semantics to a hybrid approach which dynamically adapts to non-linear control flow. We have a full implementation of hybrid TRMc in the Koka language and our benchmark shows the TRMc transformed functions are always as fast or faster than using manual alternatives.
This is an extended version of the POPL'23 publication under submission to a special issue of the Journal of Functional Programming (JFP). Extended topics include an improved TRMC algorithm, composing contexts, _field_ contexts, and first-class constructor contexts.