Frex: indexing modulo equations with free extensions (Extended Abstract)
We report about ongoing work on an extensible dependently-typed library of algebraic solvers for common algebraic structures based on free extensions (frex): the coproduct of an algebra with a free algebra. One challenge arising when programming with types indexed by values involves convincing the type-checker that two open terms are equal, as variables appearing in open terms get in the way of standard normalisation procedures like beta-reduction.
Here we focus on indexing by terms malleable to equational reasoning. When the indexing type is the carrier for an algebraic structure, we hypothesise that type-checking modulo this theory amounts to representing the free extension of the algebra structure of this type with a finite set of variables. We propose a library involving two tiers: a user-facing tier for indexing types with algebraic values (‘frexlets’), and a library-developer-facing tier for extending the library to support new algebraic theories (‘core frex’). We report and demonstrate our implementation in Brady’s upcoming Idris2 programming language.
Conference DaySun 23 AugDisplayed time zone: Eastern Time (US & Canada) change
12:30 - 14:00
|Graded Modal Dependent Type Theory (Extended Abstract)|
Benjamin MoonSchool of Computing, University of Kent, Harley D. Eades IIIAugusta University, Dominic OrchardUniversity of Kent, UKFile Attached
|Frex: indexing modulo equations with free extensions (Extended Abstract)|
|Retrofitting Symbolic Holes to LLVM IR (Extended Abstract)|