Rebound: Efficient, expressive, and well-scoped binding
summary
Rebound provides well-scoped Haskell term representations using first-class environments that map variables into a fresh scope and statically track scope indices, plus binder-level delayed substitutions that fuse at instantiation. The library implements alpha/subst/instantiate generically, supports pattern-telescopes and source-level names, and powers a pi-forall tutorial type checker. Benchmarks show the delayed approach recovers interpreter speed (e.g. naive closure eval 0.2 ms, naive parallel-subst 3 s, delayed-subst 0.7 ms) and outperforms Unbound and others on several workloads.
AI-written summary · about
chapters (20)
- 0:00Rebound library intro
- 1:38Variables with de Bruijn indices
- 2:41Lambda calculus evaluator
- 5:51Big-step evaluator
- 7:16Parallel substitutions
- 9:02Double traversal costs
- 10:46Delayed substitutions
- 12:09Reusable library design
- 14:17Complex binding patterns
- 16:49Surface syntax with names
- 18:37Reader monad for environments
- 18:59Rebound expressiveness
- 20:03Pyfall case study
- 21:07Benchmarking libraries
- 23:56Optimizing environments
- 24:17Q&A: Delayed substitutions
- 26:24Q&A: Intrinsic vs extrinsic
- 27:50Q&A: Weak explicit subs
- 28:10Q&A: Benchmark behavior
- 28:55Q&A: Explicit substitution
related talks
29mThe Essence of Reactivity
20mInteractive Haskell Type Inference Exploration (Extended Abstract)
42mFunctional interpreters and you
20mTowards Generic Type Checking Implementations in Haskell via Second-Order Abstract Syntax
24mCatching space leaks at compile-time using th-deepstrict
41mFunctional Programming for Dummies*
30mMore Fixpoints!
33mRethinking Effects with Effect Systems