Tail Recursion Modulo Context: An Equational Approach
summary
Generalizes tail recursion modulo cons into a general TRMC algorithm derived from an equational specification, requiring four instantiation operations and proofs of two simple context laws. Provides concrete instantiations (evaluation/CPS, defunctionalized contexts, monoids/semirings/exponents, cons products), proves modulo-cons soundness via Minamide's hole calculus and a Perceus-style heap semantics for safe in-place update under unique ownership, offers a hybrid runtime for non-linear control, ships a Koka implementation, and benchmarks (e.g. billion-element map) that always match or beat manual variants.
AI-written summary · about
chapters (12)
- 0:00Intro
- 2:19Reversing a List
- 4:26Example: Integer addition (length)
- 5:53Example: List Concatenation (reverse)
- 7:08Wait! how do we know the new function is equivalent to the old one? Besides defining the abstract context, and its operations, we need to show that the context laws hold
- 8:32Tail Recursion Modulo Context
- 10:35Modulo Cons: Mapping a Function
- 15:55Executing Modulo Cons Map
- 18:35Wait! How can in-place update be safe?
- 19:27Modulo Cons with Non-Linear Control is Unsafe!
- 20:25Dynamic Copy using Reference Counts
- 22:18Benchmarks: red-black tree insertion
related talks
21mTail Modulo Cons, OCaml, and Relational Separation Logic
56mAn introduction to recursion schemes
30mTail Modulo Async/Await
31mUniRec: A Unimodular-Like Framework for Nested Recursions and Loops
44m(Recursive) Functions Decoded
21mWell-founded recursion done right
19mExtensible Metatheory Mechanization via Family Polymorphism
20mA Tail of TwoTails: The Second Act