Reference. Folding domain-specific languages: deep and shallow embeddings (functional Pearl)

Cite

Cite as @gibbons-2014-folding (helia, typst) · \cite{gibbons-2014-folding} (LaTeX)
BibTeX
bibtex · 1 line
@inproceedings{gibbons-2014-folding, series={ICFP′14}, title={Folding domain-specific languages: deep and shallow embeddings (functional Pearl)}, url={http://dx.doi.org/10.1145/2628136.2628138}, DOI={10.1145/2628136.2628138}, booktitle={Proceedings of the 19th ACM SIGPLAN international conference on Functional programming}, publisher={ACM}, author={Gibbons, Jeremy and Wu, Nicolas}, year={2014}, month=Aug, pages={339–347}, collection={ICFP′14} }
hayagriva YAML (typst)
yaml · 18 lines
gibbons-2014-folding:
  type: article
  title: 'Folding domain-specific languages: deep and shallow embeddings (functional Pearl)'
  author:
  - Gibbons, Jeremy
  - Wu, Nicolas
  date: 2014-08
  page-range: 339-347
  url: http://dx.doi.org/10.1145/2628136.2628138
  serial-number:
    doi: 10.1145/2628136.2628138
  parent:
    type: proceedings
    title: Proceedings of the 19th ACM SIGPLAN international conference on Functional programming
    publisher: ACM
    parent:
      type: proceedings
      title: ICFP′14
Cited by (2)

Intrinsically Correct Sorting in Cubical Agda alexandruIntrinsicallyCorrectSorting2025

The paper “Sorting with Bialgebras and Distributive Laws” by Hinze et al. uses the framework of bialgebraic semantics to define sorting algorithms. From distributive laws between functors they construct pairs of sorting algorithms using both folds and unfolds. Pairs of sorting algorithms arising this way include insertion/selection sort and quick/tree sort. We extend this work to define intrinsically correct variants in cubical Agda. Our key idea is to index our data types by multisets, which concisely captures that a sorting algorithm terminates with an ordered permutation of its input list. By lifting bialgebraic semantics to the indexed setting, we obtain the correctness of sorting algorithms purely from the distributive law.
PDF · DOI · arXiv · pldb

Fantastic Morphisms and Where to Find Them: A Guide to Recursion Schemes yang-2022-fantastic

DOI · arXiv
Cites 31 works (2 here)
With notes (2)

Adjoint folds and unfolds—An extended study hinze-2013-adjoint

DOI

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
External (29)
gibbons-2014-folding reference entries/refs/gibbons-2014-folding/gibbons-2014-folding.hel