@article{leijen2024tail,
author = {Leijen, Daan and Lorenzen, Anton},
title = {Tail Recursion Modulo Context: An Equational Approach (extended version)},
year = {2024},
month = {May},
abstract = {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.},
url = {http://approjects.co.za/?big=en-us/research/publication/tail-recursion-modulo-context-an-equational-approach-extended-version/},
journal = {under submission to JFP.},
note = {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.},
}