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
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.
Complete and easy bidirectional typechecking for higher-rank polymorphism dunfield-2013-complete
Dependent types in practical programming xi-1999-dependent
External (19)
- Artefact for Fulls Seldom Differ ICFP 2025 (2025)
- Fulls Seldom Differ Artefact (GitHub repository) (2025)
- Batcher’s Bitonic Sorter (2024)
- Improving Haskell types with SMT (2015)
- C?aSH: Structural Descriptions of Synchronous Hardware Using Haskell (2010)
- Type inference in context (2010)
- Hands-on Introduction to Bluespec System Verilog (BSV) (2008)
- Fast Reflexive Arithmetic Tactics the Linear Case and Beyond (2006)
- Eliminating Dependent Pattern Matching (2006)
- ATS: A Language That Combines Programming with Theorem Proving (2005)
- Formalising Bitonic Sort in Type Theory (2004)
- Eliminating array bound checking through dependent types (1998)
- Using Reflection to Build Efficient and Certified Decision Procedures (1997)
- Information Processing 83: Proceedings of the IFIP 9th World Computer Congress, Paris, France, September 19-23 (1984)
- Principal type-schemes for functional programs (1982)
- A Theory of Type Polymorphism in Programming (1978)
- Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur (1972)
- An intuitionistic theory of types (1972)
- Sorting networks and their applications (1968)