Auto Merkleization: Where FP meets Algebra, Metaprogramming and OO
summary
Claims an automatic pipeline that generates zippers and merkle proofs from type definitions, using type-polynomial differentiation, zippers, content-addressing (SHA-256), and metaprogramming. Demonstrates two lines of code to produce merkle proofs for arbitrary recursive types, shows amortized O(1) focus access versus O(log n) from root traversal, and reports a Patricia Merkle trie prototype with 10× less code (Scheme/Haskell work) and deployment in skyrotocol.org, so the idea actually runs and compacts proofs.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 1:28What is Merkleization and why it matters
- 5:44Zippers for Merkle proofs
- 10:23Algebra of data types
- 17:07Differential calculus for recursion
- 22:11Automatic differentiation of types
- 27:14Zippers for algorithms
- 31:29Merkleization in 2 lines
- 34:40Manual zippers pitfalls
- 36:30Metaprogramming for types
- 38:17Zippers as primitives
- 40:02FP meets algebra and calculus
- 41:25Q&A
related talks
17mHow to Program like a Five Year Old in Haskell
01h 01mDiscussion
11mWriting Programs! That Write Other Programs!!
53mSemantics-based program manipulation in the age of LLMs
01h 17mProof-Carrying Code For the Age of AI: Machine-Checked Guarantees from(…)
19mAutomated Program Refinement: Guide and Verify Code Large Language Model with(…)
21mTowards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
30mToward Programming Languages for Reasoning -- Humans, Symbolic Systems, and AI ...