The Art of Program Derivation and Parallel Computation
summary
Starts from the specification and mechanically derives efficient implementations, showing how the Algebra of Programming yields MapReduce ideas and concrete equational steps. It proves and codes identities like fold fusion, tails/scan fusion and the Banana Split theorem, then derives a linear algorithm for the maximum segment sum by stepwise rewrites and GHCI checks. Expect runnable examples, exercises in the GitHub repo, discussion of compiler rewrite rules (build/fold fusion) and when the transformations actually reduce work.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 4:13Origins of calculating with programs
- 16:18Equational reasoning with folds
- 28:22Fold fusion and transformations
- 37:18Banana split theorem
- 49:46List homomorphisms and map-reduce
- 1:00:35Maximum segment sum problem
- 1:10:49Efficiency theory
- 1:20:01Parallel prefix sum
- 1:28:40Current research
related talks
49mMetaphorisms Deriving Divide and Conquer Recursive Programs
01h 35mRecursion Schemes, Algebras, Finally Tagless, Data Types
46mThe path to declarative programming
59mBuilding an Intuition for Composition
01h 05mThe Imperatives Must Go!
26mThe Power Of Small Abstractions
59mThe Power of Function Composition
41mIdealized Commit Logs: Code Simplification via Program Slicing