Liquid Amortization: Proving Amortized Complexity with LiquidHaskell (Functional Pearl)
Jan van Brügge
TL;DR
This work addresses the challenge of proving amortized time bounds directly on production code in Haskell without translating to external theorem provers. It adopts LiquidHaskell refinement types to encode and mechanically verify amortized analyses using Banker's and Physicist's methods, demonstrated on stacks with multipop, binomial heaps, and finger trees. The results show that in-code, mechanically checked proofs can establish bounds such as $O(1)$ for certain operations and $O(\log n)$ for others, with proof automation via ple. It discusses practical trade-offs, noting LiquidHaskell limitations (e.g., partial support for DataKinds) and how this approach favors readability and teaching over full theorem-prover capabilities, while still offering immediate alignment with production code.
Abstract
Formal reasoning about the time complexity of algorithms and data structures is usually done in interactive theorem provers like Isabelle/HOL. This includes reasoning about amortized time complexity which looks at the worst case performance over a series of operations. However, most programs are not written within a theorem prover and thus use the data structures of the production language. To verify the correctness it is necessary to translate the data structures from the production language into the language of the prover. Such a translation step could introduce errors, for example due to a mismatch in features between the two languages. We show how to prove amortized complexity of data structures directly in Haskell using LiquidHaskell. Besides skipping the translation step, our approach can also provide a didactic advantage. Learners do not have to learn an additional language for proofs and can focus on the new concepts only. For this paper, we do not assume prior knowledge of amortized complexity as we explain the concepts and apply them in our first case study, a simple stack with multipop. Moving to more complicated (and useful) data structures, we show that the same technique works for binomial heaps which can be used to implement a priority queue. We also prove amortized complexity bounds for Claessen's version of the finger tree, a sequence-like data structure with constant-time cons/uncons on either end. Finally we discuss the current limitations of LiquidHaskell that made certain versions of the data structures not feasible.