Automatic resource analysis derives provable bounds on memory and time usage from program types. The potential method — assigning a “budget” to each data structure that pays for future operations — has been automated for functional programs with lists, trees, and recursive types. But exceptions break the analysis. When a function throws, control jumps non-locally to a handler that may be many stack frames away. The budgets allocated along the normal execution path are stranded — they were assigned to operations that will never execute.
Rajani et al. (arXiv:2603.02260) extend Automatic Amortized Resource Analysis to programs with exceptions and effect handlers. The key innovation: the type system tracks resource transfers across non-local control flow. When a function might throw, its type includes a resource annotation that accounts for the budget that must be available at the handler site, not just at the throw site.
The soundness proof is relative to a stack-based abstract machine — not the standard reduction semantics used in most type-theoretic resource analyses. This is necessary because exception handling is fundamentally about the stack: throwing unwinds frames, each of which has allocated potential. The abstract machine makes these stack operations explicit, and the type soundness theorem ensures the derived bounds are valid against this concrete operational model.
The implementation handles Standard ML with polynomial potential functions and produces tight bounds on programs that previous systems couldn't analyze at all — programs where exceptions are part of the normal control flow, not just error handling.
The deeper issue: resource analysis works by relating a program's type structure to its execution cost. Exceptions disrupt the type-execution correspondence because the type says “this function returns A” but the execution says “this function jumped to a handler expecting B.” Bridging this gap requires the type system to model what happens when promises are broken.