The Scenic Route to Deforestation
summary
Proves that foldr/build deforestation is correct for Curry in most cases by translating Curry to cumin then to the deterministic Salt language and using free theorems (including applying a free theorem twice); finds the optimization is valid about 95% of the time, breaks on partial application and recursive let induced sharing, and shows a trivial transformation K → K' restores correctness for the remaining cases; ties the result to an existing compiler implementation and notes Haskell results with up to 3× speedups on heavy list programs.
AI-written summary · about
chapters (12)
- 0:00Foldar build deforestation intro
- 2:28How foldar build deforestation works
- 4:57Proving foldar build with free theorems
- 6:21Curry’s functional logic challenges
- 8:10Breaking foldar build in Curry
- 12:32Adapting free theorems for Curry
- 15:02Proving foldar build deterministically
- 16:04Handling non-determinism in proofs
- 17:34Fixing partial application with K Prime
- 19:22Key takeaways and implications
- 21:31Curry’s non-determinism history
- 23:44Q&A
related talks
30mRICE: An Optimizing Curry Compiler
55mDeforestation and Program Fusion
01h 38mGHC Core Optimisations
20mEquivalence by Canonicalization for Synthesis-Backed Refactoring
14mOne Down, 699 to Go: or, synthesising compositional desugarings
40mReasoning Under Uncertainty in SMT Solving, Research, and Life
38mRefactoring Recursion
01h 34mFormal Logic Undressed