Tail Recursion Modulo Context: An Equational Approach (extended version)

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.