Frex: Free extensions for normalisation by evaluation (invited talk)
The primitives of abstract algebra are: set (or type) with structure subject to equational properties (an algebra); and structure preserving functions (algebra homomorphisms). We traditionally interpret these primitives computationally:
data and library interfaces form a term algebra;
(algebraic) invariants are equations specifying the allowed implementations;
library implementations, compilers, and run-times may manipulate data under-the-hood, so long as they respect the equations; and
strict adherence to the specification amounts to a universal property, by ranging all possible algebra homomorphisms.
In this talk, I propose extending this methodology to equational partial specifications with an exposed implementation:
Partially-static data: data structures for partial evaluation/optimisation of multi-staged code; and
Type-indexing modulo-algebraic equations: how to ease dependently-typed programming with types that depend on values with equational properties.
whose common denominator is:
- Normalisation-by-evaluation: computing normal forms of (typically higher-order) programs with open terms.
I’ll recall the concept of a free extension (frex): a coproduct of an algebra with a free algebra. Empirically, the frex concretises to familiar algebraic representations in these problem domains such as polynomials and dictionaries. I’ll report on our existing and on-going research on putting frex to work. We develop techniques for specifying extensible libraries for normalisation-by-evaluation/type-directed partial evaluation. I’ll describe how we applied the resulting techniques in a Template Haskell and Meta-OCaml libraries for partially-static data representation. I’ll also report about our ongoing development of an Idris2 library for type-indexing modulo-equation.
Based on joint work with Jeremy Yallop, Tamara von Glehn, Philip Saville, and Edwin Brady.
Mon 20 Jan (GMT-06:00) Saskatchewan, Central America change
|15:35 - 16:10|
Ohad KammarUniversity of EdinburghMedia Attached
|16:10 - 16:35|
|DOI File Attached|
|16:35 - 16:50|
|16:50 - 17:25|
|17:25 - 17:45|
Isao SasanoShibaura Institute of TechnologyDOI