Potential Functions as Types
2026-07-09 • Programming Languages
Programming LanguagesData Structures and Algorithms
AI summaryⓘ
The authors combine two ways to analyze how much work programs do: one is a detailed, manual approach (the physicist's view) and the other is an automatic approach using credits (the banker's view). They create a system called Calf that connects these views using math in a type system, ensuring programs behave consistently and their costs add up properly. They then build Giralf, a simpler language within Calf, to manage costs with credits and debits. Finally, they design a way to automatically turn some Calf programs into Giralf ones to analyze their costs without manual effort.
Amortized analysisDependent type theoryPotential functionsSubstructural type theoryCost verificationAbstraction functionType-level credit annotationsGraded type theoryInference algorithm
Authors
Harrison Grodin, Ethan Chu, Runming Li, Jan Hoffmann, Robert Harper
Abstract
Amortized analysis can be framed from the physicist's view, amenable to manual verification in dependent type theory using potential functions, and the banker's view, amenable to automated inference in substructural type theory using type-level credit annotations. In this work, we synthesize these perspectives in Calf, a dependent type theory cost verification. From the physicist's view, we present a fracture and gluing theorem that renders every type as containing a fusion of an abstraction function and a potential function. By construction, every program between two such types must preserve abstraction, to facilitate modularity of behavior, and conserve potential, to facilitate modularity of cost. Incorporating the banker's view, we synthetically construct type operators for credits and debits. We then define Giralf, a graded substructural dependent type theory for programming with credits and debits, which is semantically interpreted as a sub-language of Calf. Finally, we adapt an inference algorithm to transform a limited class of Calf programs into Giralf counterparts, automating the cost analysis of common algorithms in Calf.