Tail Recursion Modulo Context — An Equational Approach

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 novel instantiations as suggested by our generic approach, such as _defunctionalized_ evaluation contexts, _monoids_, _semirings_, and _exponents_. 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.