Reference. Partially-static data as free extension of algebras
Partially-static data structures are a well-known technique for improving binding times. However, they are often defined in an ad-hoc manner, without a unifying framework to ensure full use of the equations associated with each operation. We present a foundational view of partially-static data structures as free extensions of algebras for suitable equational theories, i.e. the coproduct of an algebra and a free algebra in the category of algebras and their homomorphisms. By precalculating these free extensions, we construct a high-level library of partially-static data representations for common algebraic structures. We demonstrate our library with common use-cases from the literature: string and list manipulation, linear algebra, and numerical simplification.
Cite
Cited by (1)
Frex: Dependently Typed Algebraic Simplification allais-2025-frex
We present a new design for an algebraic simplification library structured around concepts from universal algebra: theories, models, homomorphisms, and universal properties of free algebras and free extensions of algebras. The library’s dependently typed interface guarantees that both built-in and user-defined simplification modules are terminating, sound, and complete with respect to a well-specified class of equations. We have implemented the design in the Idris 2 and Agda dependently typed programming languages and shown that it supports modular extension to new theories, proof extraction and certification, goal extraction via reflection, and interactive development.
Cites 25 works (1 here)
With notes (1)
Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages carette-2009-finally
We have built the first family of tagless interpretations for a higher-order typed object language in a typed metalanguage (Haskell or ML) that require no dependent types, generalized algebraic data types, or postprocessing to eliminate tags. The statically type-preserving interpretations include an evaluator, a compiler (or staged evaluator), a partial evaluator, and call-by-name and call-by-value continuation-passing style (CPS) transformers. Our principal technique is to encode de Bruijn or higher-order abstract syntax using combinator functions rather than data constructors. In other words, we represent object terms not in an initial algebra but using the coalgebraic structure of the λ-calculus. Our representation also simulates inductive maps from types to types, which are required for typed partial evaluation and CPS transformations. Our encoding of an object term abstracts uniformly over the family of ways to interpret it, yet statically assures that the interpreters never get stuck. This family of interpreters thus demonstrates again that it is useful to abstract over higher-kinded types.
External (24)
- Staged generic programming (2017)
- Generic partially-static data (extended abstract) (2016)
- Template Haskell, 14 years on (2016)
- The Essence of Multi-stage Evaluation in LMS (2016)
- Programming with algebraic effects and handlers (2015)
- Supercompilation via staging (2014)
- The Design and Implementation of BER MetaOCaml (2014)
- Shonan challenge for generative programming (2013)
- Optimizing data structures in high-level programs (2013)
- Partially static operations (2013)
- Multi-stage programming with functors and monads: Eliminating abstraction overhead from generic code (Sci. Comput. Program.) (2011)
- On typing delimited continuations: three new solutions to the printf problem (2009)
- Multi-stage Programming with Functors and Monads: Eliminating Abstraction Overhead from Generic Code (2005)
- Associated types with class (2005)
- A methodology for generating verified combinatorial circuits (2004)
- A Gentle Introduction to Multi-stage Programming (2004)
- Staging Algebraic Datatypes (2002)
- A Type Specialisation Tutorial (1999)
- Functional unparsing (1998)
- An Automatic Program Generator for Multi-Level Specialization (1997)
- Multi-stage programming with explicit annotations (1997)
- Binding-time analysis applied to mathematical algorithms (1996)
- Partial Evaluation and Automatic Program Generation (1993)
- Partially Static Structures in a Self-Applicable Partial Evaluator (1988)