Fulls seldom differ

Tools

Koch, Mark and Lawrence, Alan and McBride, Conor and Roy, Craig (2025) Fulls seldom differ. Proceedings of the ACM on Programming Languages (PACMPL), 9 (ICFP). pp. 616-642. ISSN 2475-1421 (https://doi.org/10.1145/3747526)

[thumbnail of Koch-etal-PACMPL-2025-Fulls-seldom-differ]
Preview
 Text. Filename: Koch-etal-PACMPL-2025-Fulls-seldom-differ.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (835kB)| Preview

Abstract

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.

ORCID iDs

Koch, Mark, Lawrence, Alan, McBride, Conor ORCID logoORCID: https://orcid.org/0000-0003-1487-0886 and Roy, Craig;
CORE (COnnecting REpositories)