First-class Algebraic Presentations with Elaborator Reflection (Extended Abstract)
summary
Library for Idris 2 that reinterprets fragments of host syntax at compile time to give user-definable deeply embedded many-sorted algebras without changing Idris 2. Uses elaborator reflection to quote code, infer missing pieces, and expand syntax into constructors and operations including sized monoid with technically infinitely many operations. Provides interp interface and model proofs so terms evaluate to vectors, theories yield proof obligations using heterogeneous equality, and the library compiles and runs.
AI-written summary · about
chapters (16)
- 0:00Introduction
- 0:23Motivation for embedded languages
- 1:27Algebraic presentations overview
- 3:12Encoding algebraic syntax challenges
- 4:39Ergonomic syntax with elaborator reflection
- 5:00Elaboration in Idris 2
- 6:28Elaborator reflection and syntax quoting
- 7:09Embedded syntax with elaboration scripts
- 8:14Defining terms in algebraic syntax
- 9:40Idris 2 level functions
- 11:05Interpreting terms with interp
- 12:53Evaluating terms in a model
- 13:37Equation proofs with theories
- 15:24Modeling theories with dependent types
- 15:44Summary and library availability
- 16:48Q&A
related talks
31mDependent tagless final
17mHefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects
24mImperative Syntax for Dependent Types
27mFrex: indexing modulo equations with free extensions (Extended Abstract)
01h 06mKeynote – Edwin Brady
43mIdris 2: Type-driven development of Idris
15mElaboration with First-Class Implicit Function Types
18mCompiling with Abstract Interpretation