Ohad Kammar: Frex: indexing modulo equations with free extensions
Ohad Kammar (University of Edinburgh)
(joint work with Guillaume Allais, Edwin Brady, and Jeremy Yallop)
Abstract: I'll 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 I'll 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'). I'll report and demonstrate our implementation in Brady's upcoming Idris2 programming language.
