Categorical Models of Amortized Cost: An Adjoint Relationship between Cost and Potential
David Binder, David Corfield, Dominic Orchard, Vineet Rajani
cs.PL
Aug 10, 2026 · v1
cs.LO
TL;DR
Mechanizes the λ-amor core type system in Lean and verifies that the Rajani et al. Kripke logical relations model is an instance of the general adjoint categorical model.
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.
Problem
Type systems such as λ-amor track amortized cost using a graded cost monad together with a potential type. The abstract properties that denotational models of such cost-and-potential type theories must satisfy had not been identified.
Approach
The authors propose a refined core calculus, λ-amor Core, with new primitives pay, plet and split. Its models are characterized by an adjoint pair of graded functors, where the cost functor is both a graded monad and a compatible graded comonad. Three instances are given: a set-theoretic model, the original Kripke logical relations model, and a copresheaf model built from Day convolution. The type system and the Kripke model instance are mechanized in Lean.
Results
The original λ-amor logical relations model is shown to be a sound instance of the adjoint model. λ-amor's release construct is shown to be derivable from pay, split and plet. Several of the theorems are fully mechanized in Lean, and the copresheaf model and Theorem 6.9 are left as future formalization work.
