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 JanDisplayed time zone: Saskatchewan, Central America change
15:35 - 17:45
|Frex: Free extensions for normalisation by evaluation (invited talk)|
Ohad Kammar University of EdinburghMedia Attached
|Symbolic Bisimulation for Open and Parameterized System|
PEPMDOI File Attached
|Mini Break 2|
|Acumen: A Domain-Specific Language for Cyber-Physical Systems (invited talk)|
|An approach to generating text-based IDEs with syntax completion from syntax specification|
Isao Sasano Shibaura Institute of TechnologyDOI