Sealing Pointer-Based Optimizations Behind Pure Functions
summary
Shows how dependent types seal pointer tricks behind pure interfaces to turn exponential tree traversals into linear-time algorithms, implemented for Lean v4 and used on Mathlib where a 20,000-node DAG can expand to ~2 billion tree nodes. Combines withPtrEq (recursive pointer-equality short-circuiting), intrusive constant-time hashing, and a runtime shareCommon primitive to canonicalize equal subterms, plus withPtrAddr for address-based primitives. Claims negligible extra trust and reports practical, large speedups in real libraries.
AI-written summary · about
chapters (10)
- 0:00Intro
- 0:37FP shines for ITP
- 1:46Purity's Achilles Heal
- 3:45Our contribution
- 6:33Recursive pointer equality tests
- 7:28Traversing terms in linear time
- 8:14Intrusive hashing
- 9:35Semi-naive traversal
- 10:33Sharing the common data
- 12:24Sealing other low-level optimizations
related talks
52mDotty Linker: Precise Types Bring Performance
32mBeyond the &: A Future for Native Smart Pointers in Rust
37mA Tour of Program Optimization
16mHow (Not) to Write Java Pointer Analyses after 2020
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
50mExpression Templates: Past, Present, Future
08mCompiling pattern matching to in-place modifications
01h 26mImplementing Dependent Pattern Matching and Type Unification Part 2