Towards a Performance Comparison of Syntax and Type-Directed NbE
summary
Implements a forked Smalltt to add a type-directed judgmental-equality procedure and compares it against Andreas Kovác’s syntax-directed Smalltt using Smalltt’s existing benchmark suite (Church encodings). Benchmarks show the syntax-directed variant normalized to 1 and the type-directed variant slower, with one large benchmark running out of memory; the type-directed version includes a new unit-type equality rule and attempts to port Smalltt’s micro-optimizations (mutable IO monad). Results are preliminary and performance differences remain unexplained. benchmarks normalize syntax to 1
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:03Dependently typed crash course
- 5:00Type checking algorithms
- 8:35Syntax vs type-directed equality
- 11:31Motivation for comparison
- 13:17Implementing type-directed equality
- 14:42Benchmarking algorithms
- 16:08Initial performance results
- 17:12Usability trade-offs
- 18:15Takeaways
- 18:35Q&A
related talks
26mType Narrowing the Hard Way
24mScoped and Typed Staging by Evaluation
02h 50mIntro to Type Systems and Operational Semantics
19mIll-Typed Programs Don't Evaluate
15mStaged Compilation with Two-Level Type Theory
28mEta conversion for the unit type (is still not that simple)
58mPanel discussion: Types for All: From weak to strong, from static to dynamic
23mPerformant Dynamically Typed E-Graphs in Pure Julia