The free extension (frex) offers a uniform theoretical foundation for the collection of partial-evaluation techniques known as partially-static data structures, proposed by Yallop et al. (2018). In the frex methodology, to define the partially static representation of a concrete semantic domain, we: (1) identify an algebraic signature for expressions in this semantic domain; (2) identify a collection of semantic equations with respect to which we wish to optimise expressions in this domain; and (3) design a data-structure, the partially-static reprsentation, satisfying the specification given by the universal property of the free extension of the concrete semantic domain with a set of varialbes. Since universal properties are given up-to a unique canonical isomorphism, such specifications allow us to formulate the way in which different partially-static representations compare or differ. This uniform identification of the partially-static representations allows Yallop et al. to treat them uniformly in a single library. We report about ongoing work for using existing free extensions (frexes) for component theories to construct frexes for combined theories.

We begin with a brief recourse of multi-sorted universal algebra and its application, through frex, to partial evaluation. Next, we describe a modular construction of an involutive algebra frex out of the frex of the underlying algebra. This construction encompasses situations such as: string concatenation and reversal; complex number addition/multiplication and conjugation; matrix addition/multiplication and transpose. The second modular construction concerns the free multi-sorted extension of a graph of algebras and homomorphisms between them, using the single-sorted frex for each algebra. Examples here cover monoids with (concrete) fold operators on them, as well as calculations that come up when mechanising the calculations involved in establishing the frex universal property (Allais et al. 2023). The key insight here is using the set of nodes from which we can reach each node in the graph. For the final construction, we describe ongoing work on Hyland and Power’s distributive combination of theories. These can account for the combinations of non-deterministic choice with probabilistic choice, and we offer a generalisation that accounts for non-affine theories. We conclude by outlining prospects and further direction.