Reference. Adjoint folds and unfolds—An extended study
Cite
Cited by (6)
Fantastic Morphisms and Where to Find Them: A Guide to Recursion Schemes yang-2022-fantastic
Structured Handling of Scoped Effects yang-2022-structured
Algebraic effects offer a versatile framework that covers a wide variety of effects. However, the family of operations that delimit scopes are not algebraic and are usually modelled as handlers, thus preventing them from being used freely in conjunction with algebraic operations. Although proposals for scoped operations exist, they are either ad-hoc and unprincipled, or too inconvenient for practical programming. This paper provides the best of both worlds: a theoretically-founded model of scoped effects that is convenient for implementation and reasoning. Our new model is based on an adjunction between a locally finitely presentable category and a category of functorial algebras . Using comparison functors between adjunctions, we show that our new model, an existing indexed model, and a third approach that simulates scoped operations in terms of algebraic ones have equal expressivity for handling scoped operations. We consider our new model to be the sweet spot between ease of implementation and structuredness. Additionally, our approach automatically induces fusion laws of handlers of scoped effects, which are useful for reasoning and optimisation.
Algorithmics bird-2021-algorithmics
Conjugate Hylomorphisms -- Or: The Mother of All Structured Recursion Schemes hinze-2015-conjugate
Folding domain-specific languages: deep and shallow embeddings (functional Pearl) gibbons-2014-folding
Kan Extensions for Program Optimisation Or: Art and Dan Explain an Old Trick hinze-2012-kan
Cites 69 works (0 here)
External (69)
- Concrete stream calculus—an extended study (2011)
- Type Fusion (2011)
- Factorising folds for faster functions (2010)
- Reason isomorphically! (2010)
- Haskell 2010 Language Report (2010)
- The Coq proof assistant reference manual (2010)
- Corecursive algebras: A study of general structured corecursion (2009)
- Parametric datatype-genericity (2009)
- Complete and decidable type inference for gadts (2009)
- Foundations for structured programming with gadts (2008)
- Programming in ωmega (2008)
- Recursive coalgebras of finitary functors (2007)
- Stream fusion: from lists to streams to nothing at all (2007)
- Initial algebra semantics is enough! (2007)
- Recursive coalgebras from comonads (2006)
- Iteration and coiteration schemes for higher-order and nested datatypes (2005)
- Scrap your boilerplate with class: extensible generic functions (2005)
- Disciplined, efficient, generalised folds for nested datatypes (2004)
- Substitution in non-wellfounded syntax with variable binding (2004)
- Two-level types and parameterized modules (2004)
- Generalised coinduction (2003)
- Fun with phantom types (2003)
- Simulating quantified class constraints (2003)
- Haskell 98 Language and Libraries: The Revised Report (2003)
- Generic Accumulations (2002)
- Representations of first order function types as terminal coalgebras (2001)
- Derivable type classes (2001)
- Recursion schemes from comonads (2001)
- Generic downwards accumulations (2000)
- Functional Pearl: perfect trees and bit-reversal permutations (2000)
- Generalizing generalized tries (2000)
- Efficient generalized folds (2000)
- Memo functions, polytypically! (2000)
- Coding recursion à la Mendler (extended abstract) (2000)
- Generalised folds for nested datatypes (1999)
- An extensional characterization of lambda-lifting and lambda-dropping (1999)
- Book review: the algebra of programming (1999)
- Primitive (co)recursion and course-of-value (co)iteration, categorically (1999)
- Category Theory for Computing Science (1999)
- The under-appreciated unfold (1998)
- Functional programming with apomorphisms (corecursion) (1998)
- Introduction to Functional Programming using Haskell (1998)
- Nested datatypes (1998)
- The Art of Computer Programming, Volume 3: Sorting and Searching (1998)
- Categories for the Working Mathematician (1998)
- Catenable double-ended queues (1997)
- Algebra of Programming (1997)
- Type specialisation for the λ-calculus; or, A new paradigm for partial evaluation based on type inference (1996)
- Charitable thoughts (class notes) (1996)
- Categorical fixed point calculus (1995)
- A generalization of the trie data structure (1995)
- Codifying guarded definitions with recursive schemes (1995)
- Inductive types in constructive languages (1995)
- Category theory as coherently constructive lattice theory (1994)
- Monadic maps and folds for arbitrary datatypes (1994)
- Paramorphisms (1992)
- Law and order in algorithmics (1992)
- Algebraically complete categories (1991)
- Functional programming with bananas, lenses, envelopes and barbed wire (1991)
- Inductive types and type constraints in the second-order lambda calculus (1991)
- Data structures and program transformation (1990)
- A typed lambda calculus with categorical type constructors (1987)
- Polymorphic type schemes and recursive definitions (1984)
- The category-theoretic solution of recursive domain equations (1982)
- Algebraic specification of data types: a synthetic approach (1981)
- From lambda-calculus to cartesian closed categories (1980)
- Initial algebra semantics and continuous algebras (1977)
- A fixpoint theorem for complete categories (1968)
- Über die gegenseitige Lage gleicher Teile gewisser Zeichenreihen (1912)