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.