[TyDe'22] Normalization by Evaluation with Free Extensions (Extended Abstract)

Normalization by Evaluation with Free Extensions (Extended Abstract) Nathan Corbyn (University of Oxford) Ohad Kammar (University of Edinburgh) Sam Lindley (The University of Edinburgh, UK) Nachiappan Valliappan (Chalmers University of Technology) Jeremy Yallop (University of Cambridge) Normalization-by-Evaluation (NbE) is a well-established technique for normalizing terms via an interpretation in a semantic domain. NbE provides a unified treatment of the implementation and verification of normalization algorithms, but extending it to support new features requires a certain amount of ingenuity and is often achieved in an ad hoc manner. Free extensions (frex) are a new technique for partial evaluation based on concepts from universal algebra. We present NbE for a language with higher-order functions and an algebraic structure over a primitive type. Augmenting NbE with a frex for the algebraic structure yields a generic NbE algorithm that works for all such instantiations, and thus for all primitive types with this structure. We show that this implementation also seamlessly extends to the inclusion of a monadic construct for information-flow control. We outline ongoing work extending frex to deal with higher-order features, programmatically in OCaml and semantically through Cartmell's generalised algebraic theories.