Categorical Models of Amortized Cost: An Adjoint Relationship between Cost and Potential
2026-08-10 • Programming Languages
Programming LanguagesLogic in Computer Science
AI summaryⓘ
The authors study ways to track how much 'cost' a computer program uses while it runs, not just the worst case but also the average case over time (called amortized cost). They focus on a system called λ-amor that uses types to record cost and potential, which is like stored-up cost. The paper identifies the key mathematical structures needed to model this system correctly, involving special functions called adjoint graded functors that represent costs and potentials. They provide three example models demonstrating their abstract framework, including one new model using advanced categorical concepts.
type systemcost-tracking monadamortized costλ-amoradjoint functorsgraded monadgraded comonadKripke logical relationsDay convolutioncopresheaves
Authors
David Binder, David Corfield, Dominic Orchard, Vineet Rajani
Abstract
Various type systems have been developed to track the cost $κ$ of a computation using a cost-tracking monad $M\ κτ$. On its own, this only tracks the worst-case cost of a computation. If we also want to track amortized cost, then we can add a type $[κ]τ$ which stores potential $κ$ with a type $τ$, together with operations for storing and releasing potential. In this work, we build on one such system, $λ$-amor: $λ$-amor allows to track cost and potential in the type system and subsumes effect and coeffect-based systems, call-by-value and call-by-name based languages. In this paper, we identify the abstract properties that denotational models of type theories for cost and potential have to satisfy: Cost and potential must be modelled by an adjoint pair of graded functors, where the functor modelling cost forms both a graded monad and a compatible graded comonad. We present three concrete instances of this general abstract scheme: (1) A simple set-theoretic model that ignores the cost tracked by the type system, (2) the Kripke logical relations model in the original $λ$-amor paper (which we show can be turned into an instance of the adjoint model), and (3) a novel model based on copresheaves on a monoidal category of costs, where we model pairs and functions by Day convolution and its right-adjoint.