Yaffle: A New Core for Idris 2
summary
Yaffle is a new core for Idris 2 implemented in Idris 2 itself, built to fix core bottlenecks and simplify checking. It compiles via Chez Scheme and bootstraps in a few minutes (~3–5), runs roughly an order of magnitude faster than Idris 1, and is about 95% compatible with Idris 2. Key ideas: terms indexed by names in scope to prevent scope bugs, QTT quantities (notably quantity zero for erasable proofs), and a glued evaluation strategy that speeds hard unifications while keeping readable errors.
AI-written summary · about
chapters (7)
- 0:00Introduction to Yaffle
- 2:14Implementation details
- 4:18Compilation and performance
- 8:10Syntax and elaborator
- 14:21Core representation
- 20:47Glued evaluation strategy
- 26:16Lessons and future outlook
related talks
43mIdris 2: Type-driven development of Idris
01h 06mKeynote – Edwin Brady
39mDependent Type Driven Program Synthesis in Idris
12mIdris2-Table: Evaluating dependently-typed tables with... (Extended Abstract)
20mFirst-class Algebraic Presentations with Elaborator Reflection (Extended Abstract)
01h 38mGHC Core Optimisations
28mSSA CFG Yul A new viaIR backend
13mBootstrapping a Compiler with Yul