Practical Normalization by Evaluation for EDSLs
summary
Provides a practical recipe using Normalization by Evaluation to get the fusion benefits of shallow embeddings while keeping deep-syntax for codegen: implemented as a Haskell typeclass with a semantic domain and reflect/reify operations, evaluator and reifier. Works on integers, arrays and stateful effects to eliminate intermediate arrays and collapse redundant puts/gets, even delaying case analysis to avoid extra allocations. Adds a gluing trick to avoid unwanted eta-expansion; sums and effects need extra care. Code and larger instance choices live on the project GitHub and the approach proves modular and effective on realistic examples.
AI-written summary · about
chapters (7)
- 0:00Introduction and setup
- 4:26Deep vs shallow embedding
- 11:19Normalization by evaluation
- 17:32Implementing array normalization
- 20:40Examples and fusion results
- 24:14Practical considerations and summary
- 28:12Q&A session
related talks
35mFrex: Free Extensions for Normalization-by-Evaluation
29mEfficient Evaluation with Controlled Definition Unfolding
30mYin-Yang: Concealing the Deep Embedding of DSLs (Most Influential Paper)
28mBridging Syntax and Semantics of Lean Expressions in E-Graphs
28mEta conversion for the unit type (is still not that simple)
01h 04mEDSL Infinity Wars: Mainstreaming Symbolic Computation
16mThe Normalization Barrier Revisited
01h 01mChallenges in the Design and Implementation of Teaching Languages for EDSLs