Read/write factorizable programs
summary
Claim: read/write factorization yields a clean syntactic class of programs over strings that exactly captures FP when recursion is non‑nested and FL for tail recursion. Construction: a simple type system partitions data into RW-factorizable read‑only and write‑only strings, uses counting modules to represent bounded integers, and gives a pairwise compilation between RW programs and cons‑free+counting bit/length programs. Surprise: nested recursion breaks the capture; paper also gives a concrete syntactic composition procedure that provably works.
AI-written summary · about
chapters (16)
- 0:00Introduction
- 1:05Programming language model
- 3:55Cons-free programs
- 5:41Functional complexity challenges
- 7:06RW factorization with types
- 9:14Limitations
- 10:41Non-nested recursion
- 11:22Beyond string programs
- 13:48Counting modules
- 16:14Polynomial time functions
- 17:36Compiling programs
- 19:04Compositionality
- 20:29Consequences
- 21:13Dedication
- 21:55Programming language indexing
- 23:04Q&A
related talks
36mConcrete Functional Programming
56mAn introduction to recursion schemes
34mPeeling the Banana: Recursion Schemes from First Principles
24mA Type-Based Approach to Divide-and-Conquer Recursion in Coq
25mRecursive Program Synthesis using Paramorphisms
33mEXPLAIN FP LIKE RICHARD FEYNMAN
01h 02mGoing bananas with recursion schemes for fixed point data types
53mY Not- Adventures in Functional Programming