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

Cite as @yallop-2018-partially (helia, typst) · \cite{yallop-2018-partially} (LaTeX)
BibTeX
bibtex · 1 line
@article{yallop-2018-partially, title={Partially-static data as free extension of algebras}, volume={2}, ISSN={2475-1421}, url={http://dx.doi.org/10.1145/3236795}, DOI={10.1145/3236795}, number={ICFP}, journal={Proceedings of the ACM on Programming Languages}, publisher={Association for Computing Machinery (ACM)}, author={Yallop, Jeremy and von Glehn, Tamara and Kammar, Ohad}, year={2018}, month=July, pages={1–30} }
hayagriva YAML (typst)
yaml · 19 lines
yallop-2018-partially:
  type: article
  title: Partially-static data as free extension of algebras
  author:
  - Yallop, Jeremy
  - name: Glehn
    given-name: Tamara
    prefix: von
  - Kammar, Ohad
  date: 2018-07
  page-range: 1-30
  serial-number:
    doi: 10.1145/3236795
  parent:
    type: periodical
    title: Proceedings of the ACM on Programming Languages
    publisher: Association for Computing Machinery (ACM)
    issue: ICFP
    volume: 2
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.
PDF · DOI · pldb
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.
PDF · DOI · pldb
yallop-2018-partially reference entries/refs/yallop-2018-partially/yallop-2018-partially.hel