Many programs process lists by recursing in a wide variety of sequential and/or divide-and-conquer patterns. Reasoning about the correctness and completeness of these programs requires reasoning about the lengths of the lists, techniques for which are typically undecidable or at least NP-complete. In this paper we show how introducing a relatively simple (sub-)language for expressions describing list lengths, whilst not completely general, covers a great number of these patterns. It includes not only doubling but also exponentiation (iterated doubling), and moreover admits a simple length-checking algorithm that is complete over a predictable problem domain. We prove termination of the algorithm via category-theoretic pullbacks, formalized in Agda, as well as providing a more realistic implementation in Rocq, and a toy language Fulbourn with interpreter in Haskell.

@article{paperbot3032,
  title = {Fulls Seldom Differ},
  author = {Mark Koch and Alan Lawrence and Conor McBride and Craig Roy},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {ICFP},
  year = {2025},
  doi = {10.1145/3747526}
}