Modular Construction of Multi-sorted Free Extensions
summary
Defines how to build combined free extensions by composing existing frexes and gives three modular constructions: a concrete involutive algebra frex (covers string concat+reverse, complex conjugation, matrix transpose), a multi-sorted frex for a graph of algebras using single-sorted frexes (covers monoids with concrete fold), and a generalisation of Hyland–Power distributive combinations for non-affine theories. Claims a compositional procedure that preserves universal properties, uses the reachability set trick to assemble node-wise data, and reports prototype mechanisation and Idris examples validating the constructions.
AI-written summary · about
chapters (16)
- 0:00Introduction
- 1:18Free extensions from partial evaluation
- 2:25Action box example
- 4:11Action box state and commands
- 5:15Automating action box
- 7:42Scripts to monoid actions
- 10:54Abstracting commands and states
- 15:29Partially static data structures
- 18:31Implementing partial evaluator
- 21:05Algebraic structure
- 22:50Free extensions framework
- 24:56Partially static data as free extensions
- 26:41Modularity in partial evaluation
- 28:47Beyond single evaluators
- 30:11Conclusions
- 31:04Q&A
related talks
27mFrex: indexing modulo equations with free extensions (Extended Abstract)
35mFrex: Free Extensions for Normalization-by-Evaluation
17mHefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects
27mPractical Extensions for Graded Monads
20mFormalizing polynomial laws and the universal divided power algebra
21mCompositions for Free: Reasoning about Effectful Lenses
21mFlexibly graded monads and graded algebras
27mFunctorial Semantics for Partial Theories