Frex: indexing modulo equations with free extensions (Extended Abstract)
summary
An extensible Idris2 library implements equality-by-normalization for indices using free extensions, with a user tier (frexlets) and a developer tier (core frex). A key API function, frexify, normalizes indexed expressions modulo an algebraic theory (currently full support for commutative monoids) and returns constructive proofs when normal forms match. The implementation uses forwarding to hide index expressions, is sound and complete via normal forms, scales from half an hour to about 15 seconds typechecking on current hardware, and remains a work in progress.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 3:27Programming with Indices
- 6:07The problem
- 11:44Fording Alt
- 15:12Frex: Free Extensions of Algebras
- 18:16Frexlets
- 19:35Frexifying with Alt
- 23:46Summary
related talks
35mFrex: Free Extensions for Normalization-by-Evaluation
35mModular Construction of Multi-sorted Free Extensions
20mFirst-class Algebraic Presentations with Elaborator Reflection (Extended Abstract)
30megg: Fast and Extensible Equality Saturation
16mIndexed Streams: A Formal Intermediate Representation for Fused Contraction Programs
24mA Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F...
14mdxo: A System for Relational Algebra and Differentiation
22mEREQ: Regular Expressions with Quantifiers and Incremental Quantifier Elimination