Reference. Fulls Seldom Differ

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.

Cite

Cite as @koch-2025-fulls (helia, typst) · \cite{koch-2025-fulls} (LaTeX)
BibTeX
bibtex · 1 line
@article{koch-2025-fulls, title={Fulls Seldom Differ}, volume={9}, ISSN={2475-1421}, url={http://dx.doi.org/10.1145/3747526}, DOI={10.1145/3747526}, number={ICFP}, journal={Proceedings of the ACM on Programming Languages}, publisher={Association for Computing Machinery (ACM)}, author={Koch, Mark and Lawrence, Alan and McBride, Conor and Roy, Craig}, year={2025}, month=Aug, pages={616–642} }
hayagriva YAML (typst)
yaml · 20 lines
koch-2025-fulls:
  type: article
  title: Fulls Seldom Differ
  author:
  - Koch, Mark
  - Lawrence, Alan
  - McBride, Conor
  - Roy, Craig
  date: 2025-08
  page-range: 616-642
  url: http://dx.doi.org/10.1145/3747526
  serial-number:
    doi: 10.1145/3747526
    issn: 2475-1421
  parent:
    type: periodical
    title: Proceedings of the ACM on Programming Languages
    publisher: Association for Computing Machinery (ACM)
    issue: ICFP
    volume: 9
Cites 22 works (3 here)
With notes (3)

Everybody’s Got To Be Somewhere mcbrideEverybodysGotToBeSomewhere2018

The key to any nameless representation of syntax is how it indicates the variables we choose to use and thus, implicitly, those we discard. Standard de Bruijn representations delay discarding maximally till the leaves of terms where one is chosen from the variables in scope at the expense of the rest. Consequently, introducing new but unused variables requires term traversal. This paper introduces a nameless ‘co-de-Bruijn’ representation which makes the opposite canonical choice, delaying discarding minimally, as near as possible to the root. It is literate Agda: dependent types make it a practical joy to express and be driven by strong intrinsic invariants which ensure that scope is aggressively whittled down to just the support of each subterm, in which every remaining variable occurs somewhere. The construction is generic, delivering a universe of syntaxes with higher-order metavariables, for which the appropriate notion of substitution is hereditary. The implementation of simultaneous substitution exploits tight scope control to avoid busywork and shift terms without traversal. Surprisingly, it is also intrinsically terminating, by structural recursion alone.
DOI

Complete and easy bidirectional typechecking for higher-rank polymorphism dunfield-2013-complete

PDF · DOI · arXiv · pldb

Dependent types in practical programming xi-1999-dependent

PDF · DOI · pldb
koch-2025-fulls reference entries/refs/koch-2025-fulls/koch-2025-fulls.hel