Write a Blog >>
Mon 20 Jan 2020 15:35 - 16:10 at Frontenac - Sessions 3 & 4 Chair(s): Atsushi Igarashi, Jeremy Yallop

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

Displayed time zone: Saskatchewan, Central America change