A Unifying Type-Theory for Higher-Order (Amortized) Cost Analysis

This paper presents lambda-amor, a new type-theoretic framework for amortized cost analysis of higher-order functional programs and shows that existing type systems for cost analysis can be embedded in it lambda-amor introduces a new modal type for representing potentials - costs that have been accounted for, but not yet incurred, which are central to amortized analysis. Additionally, lambda-amor relies on standard type-theoretic concepts like affineness, refinement types and an indexed cost monad lambda-amor is proved sound using a rather simple logical relation. We embed two existing type systems for cost analysis in lambda-amor showing that, despite its simplicity, lambda-amor can simulate cost analysis for different evaluation strategies (call-by-name and callby-value), in different styles (effect-based and coeffect-based), and with or without amortization. One of the embeddings also implies that lambda-amor is relatively complete for all terminating PCF programs.