Reference. Folding domain-specific languages: deep and shallow embeddings (functional Pearl)
Cite
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.
Fantastic Morphisms and Where to Find Them: A Guide to Recursion Schemes yang-2022-fantastic
Cites 31 works (2 here)
With notes (2)
Adjoint folds and unfolds—An extended study hinze-2013-adjoint
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 (29)
- Personal communication (Richard Boulton) (2014)
- Combining Deep and Shallow Embedding for EDSL (2013)
- Making EDSLs fly (2012)
- Domain-Specific Languages (2011)
- CUFP write-up (2007)
- Dealing with large bananas (2000)
- Synthesizing object-oriented and functional design to promote re-use (1998)
- The expression problem (1998)
- Experience with embedding hardware description languages in HOL (1992)
- Tupling and mutumorphisms (1990)
- Programming: The Derivation of Algorithms (1990)
- User-defined types and procedural data structures as complementary approaches to data abstraction (1975)
- Combinatory Logic, volume 2 (1972)
- 10.1145/1596638.1596644
- 10.1145/1780.1781
- 10.1016/0304-3975(85)90135-5
- 10.1145/800141.804666
- 10.1007/978-3-319-15940-9_1
- 10.1145/289423.289455
- 10.1007/978-3-540-27764-4_11
- 10.1017/s0956796804005313
- 10.1145/2500365.2500578
- 10.1145/256167.256201
- 10.1145/242224.242477
- 10.1007/978-3-642-32202-0_3
- 10.1145/2503778.2503791
- 10.1017/s0956796808006758
- 10.1145/99370.99404
- 10.1145/75277.75283