More Web Proxy on the site http://driver.im/

research-article

Unifying structured recursion schemes

Authors:

Jeremy GibbonsAuthors Info & Claims

ACM SIGPLAN Notices, Volume 48, Issue 9

Pages 209 - 220

https://doi.org/10.1145/2544174.2500578

Published: 25 September 2013 Publication History

Abstract

Folds over inductive datatypes are well understood and widely used. In their plain form, they are quite restricted; but many disparate generalisations have been proposed that enjoy similar calculational benefits. There have also been attempts to unify the various generalisations: two prominent such unifications are the 'recursion schemes from comonads' of Uustalu, Vene and Pardo, and our own 'adjoint folds'. Until now, these two unified schemes have appeared incompatible. We show that this appearance is illusory: in fact, adjoint folds subsume recursion schemes from comonads. The proof of this claim involves standard constructions in category theory that are nevertheless not well known in functional programming: Eilenberg-Moore categories and bialgebras.

References

[1]

R. Backhouse, M. Bijsterveld, R. van Geldrop, and J. van der Woude, "Categorical fixed point calculus," in CTCS, ser. LNCS, vol. 953. Springer, 1995, pp. 159--179.

Digital Library

[2]

F. Bartels, "Generalised coinduction," Mathematical Structures in Computer Science, vol. 13, pp. 321--348, 2003.

Digital Library

[3]

R. Bird and O. de Moor, Algebra of Programming. London: Prentice Hall, 1997.

Digital Library

[4]

R. Bird and R. Paterson, "Generalised folds for nested datatypes," Formal Aspects of Computing, vol. 11, no. 2, pp. 200--222, 1999.

Digital Library

[5]

V. Capretta, T. Uustalu, and V. Vene, "Recursive coalgebras from comonads," Information and Computation, vol. 204, no. 4, pp. 437--468, 2006.

Digital Library

[6]

S. Eilenberg and J. C. Moore, "Adjoint functors and triples," Illinois J. Math, vol. 9, no. 3, pp. 381--398, 1965.

[7]

M. M. Fokkinga, "Law and order in algorithmics," Ph.D. dissertation, University of Twente, Feb. 1992.

[8]

----, "Tupling and mutumorphisms," The Squiggolist, vol. 1, no. 4, pp. 81--82, Jun. 1990.

[9]

J. Gibbons, "Generic downwards accumulations," Science of Computer Programming, vol. 37, no. 1--3, pp. 37--65, 2000.

Digital Library

[10]

T. Hagino, "Category theoretic approach to data types," Ph.D. dissertation, University of Edinburgh, 1987.

[11]

R. Hinze, "Adjoint folds and unfolds--an extended study," Science of Computer Programming, Aug. 2012.

Digital Library

[12]

R. Hinze and D. W. James, "Proving the unique fixed-point principle correct: an adventure with category theory," in ICFP. ACM, 2011, pp. 359--371.

Digital Library

[13]

P. J. Huber, "Homotopy theory in general categories," Math. Ann., vol. 144, pp. 361--385, 1961.

[14]

D. M. Kan, "Adjoint functors," Trans. AMS, vol. 87, no. 2, pp. 294--329, 1958.

[15]

H. Kleisli, "Every standard construction is induced by a pair of adjoint functors," Proc. AMS, vol. 16, no. 3, pp. 544--546, Jun. 1965.

[16]

J. Lambek, "A fixpoint theorem for complete categories," Math. Zeitschr., vol. 103, pp. 151--161, 1968.

[17]

S. Mac Lane, Categories for the Working Mathematician, 2nd ed., ser. Graduate Texts in Mathematics. Berlin: Springer-Verlag, 1998.

[18]

G. Malcolm, "Algebraic data types and program transformation," Ph.D. dissertation, University of Groningen, 1990.

[19]

----, "Data structures and program transformation," Science of Computer Programming, vol. 14, no. 2-3, pp. 255--280, 1990.

Digital Library

[20]

R. Matthes and T. Uustalu, "Substitution in non-wellfounded syntax with variable binding," TCS, vol. 327, no. 1-2, pp. 155--174, 2004.

Digital Library

[21]

L. Meertens, "Paramorphisms," Formal Aspects of Computing, vol. 4, pp. 413--424, 1992.

Digital Library

[22]

E. Meijer, M. Fokkinga, and R. Paterson, "Functional programming with bananas, lenses, envelopes and barbed wire," in FPLCA, ser. LNCS, vol. 523. Springer, 1991, pp. 124--144.

Digital Library

[23]

N. P. Mendler, "Inductive types and type constraints in the second-order lambda calculus," Ann. Pure Appl. Logic, vol. 51, no. 1-2, pp. 159--172, 1991.

[24]

P. H. Palmquist, "The double category of adjoint squares," in Midwest Category Seminar V, ser. LNM. Springer, 1971, vol. 195, pp. 123--153.

[25]

A. Pardo, "Generic accumulations," in Working Conference on Generic Programming, vol. 243. Kluwer Academic Publishers, Jul. 2002, pp. 49--78.

Digital Library

[26]

T. Uustalu and V. Vene, "Primitive (co)recursion and course-of-value (co)iteration, categorically," Informatica, Lith. Acad. Sci., vol. 10, no. 1, pp. 5--26, 1999.

[27]

----, "Comonadic notions of computation," in CMCS, ser. ENTCS, vol. 203(5), 2008, pp. 263--284.

Digital Library

[28]

----, "Mendler-style inductive types, categorically," Nordic J. Comput., vol. 6, pp. 343--361, 1999.

Digital Library

[29]

----, "The recursion scheme from the cofree recursive comonad," ENTCS, vol. 229, no. 5, pp. 135--157, 2011, proceedings of the Second Workshop on Mathematically Structured Functional Programming (MSFP 2008).

Digital Library

[30]

T. Uustalu, V. Vene, and A. Pardo, "Recursion schemes from comonads," Nordic J. Comput., vol. 8, pp. 366--390, Sep. 2001.

Digital Library

[31]

V. Vene and T. Uustalu, "Functional programming with apomorphisms (corecursion)," Proceedings of the Estonian Academy of Sciences: Physics, Mathematics, vol. 47, no. 3, pp. 147--161, 1998.

[32]

J. C. Vidal and J. S. Tur, "Kleisli and Eilenberg-Moore constructions as parts of biadjoint situations," Extracta Mathematicae, vol. 25, no. 1, pp. 1--61, 2010.

Cited By

De Angelis EFioravanti FPettorossi AProietti M(2023)Constrained Horn Clauses Satisfiability via Catamorphic AbstractionsLogic-Based Program Synthesis and Transformation10.1007/978-3-031-45784-5_4(39-57)Online publication date: 16-Oct-2023
https://doi.org/10.1007/978-3-031-45784-5_4
DE ANGELIS EPROIETTI MFIORAVANTI FPETTOROSSI A(2022)Verifying Catamorphism-Based Contracts using Constrained Horn ClausesTheory and Practice of Logic Programming10.1017/S147106842200017522:4(555-572)Online publication date: 7-Jul-2022
https://doi.org/10.1017/S1471068422000175
Nguyen MWu N(2022)Folding over Neural NetworksMathematics of Program Construction10.1007/978-3-031-16912-0_5(129-150)Online publication date: 26-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-16912-0_5
Show More Cited By

Index Terms

Unifying structured recursion schemes
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Functional languages

Recommendations

Unifying structured recursion schemes
ICFP '13: Proceedings of the 18th ACM SIGPLAN international conference on Functional programming

Folds over inductive datatypes are well understood and widely used. In their plain form, they are quite restricted; but many disparate generalisations have been proposed that enjoy similar calculational benefits. There have also been attempts to unify ...
Recursion schemes from comonads

Within the setting of the categorical approach to total functional programming, we introduce a "many-in-one" recursion scheme that neatly unifies a variety of seemingly diverging strengthenings of the basic recursion scheme of iteration. The new scheme ...
Recursive coalgebras from comonads
Special issue: Seventh workshop on coalgebraic methods in computer science 2004

The concept of recursive coalgebra of a functor was introduced in the 1970s by Osius in his work on categorical set theory to discuss the relationship between wellfounded induction and recursively specified functions. In this paper, we motivate the use ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 48, Issue 9

ICFP '13

September 2013

457 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2544174

Editor:
Mark W. Bailey
Hamilton College, Clinton, NY

Issue’s Table of Contents

ICFP '13: Proceedings of the 18th ACM SIGPLAN international conference on Functional programming
September 2013
484 pages
ISBN:9781450323260
DOI:10.1145/2500365
General Chair:
Greg Morrisett
Harvard University, USA
,
Program Chair:
Tarmo Uustalu
Institute of Cybernetics at TUT, Estonia

Copyright © 2013 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 September 2013

Published in SIGPLAN Volume 48, Issue 9

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

16
Total Citations
View Citations
334
Total Downloads

Downloads (Last 12 months)33
Downloads (Last 6 weeks)4

Reflects downloads up to 09 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

De Angelis EFioravanti FPettorossi AProietti M(2023)Constrained Horn Clauses Satisfiability via Catamorphic AbstractionsLogic-Based Program Synthesis and Transformation10.1007/978-3-031-45784-5_4(39-57)Online publication date: 16-Oct-2023
https://doi.org/10.1007/978-3-031-45784-5_4
DE ANGELIS EPROIETTI MFIORAVANTI FPETTOROSSI A(2022)Verifying Catamorphism-Based Contracts using Constrained Horn ClausesTheory and Practice of Logic Programming10.1017/S147106842200017522:4(555-572)Online publication date: 7-Jul-2022
https://doi.org/10.1017/S1471068422000175
Nguyen MWu N(2022)Folding over Neural NetworksMathematics of Program Construction10.1007/978-3-031-16912-0_5(129-150)Online publication date: 26-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-16912-0_5
Murata KEmoto K(2019)Recursion Schemes in CoqProgramming Languages and Systems10.1007/978-3-030-34175-6_11(202-221)Online publication date: 18-Nov-2019
https://doi.org/10.1007/978-3-030-34175-6_11
Barwell ABrown CHammond K(2018)Finding parallel functional pearlsFuture Generation Computer Systems10.1016/j.future.2017.07.02479:P2(669-686)Online publication date: 1-Feb-2018
https://dl.acm.org/doi/10.1016/j.future.2017.07.024
DE ANGELIS EFIORAVANTI FPETTOROSSI APROIETTI M(2024)Catamorphic Abstractions for Constrained Horn Clause SatisfiabilityTheory and Practice of Logic Programming10.1017/S147106842400019X(1-28)Online publication date: 29-Oct-2024
https://doi.org/10.1017/S147106842400019X
DOWNEN PARIOLA Z(2023)Classical (co)recursion: MechanicsJournal of Functional Programming10.1017/S095679682200016833Online publication date: 4-Apr-2023
https://doi.org/10.1017/S0956796822000168
De Angelis EFioravanti FPettorossi AProietti M(2023)Multiple Query Satisfiability of Constrained Horn ClausesPractical Aspects of Declarative Languages10.1007/978-3-031-24841-2_9(125-143)Online publication date: 16-Jan-2023
https://dl.acm.org/doi/10.1007/978-3-031-24841-2_9
Yang ZWu N(2022)Fantastic Morphisms and Where to Find ThemMathematics of Program Construction10.1007/978-3-031-16912-0_9(222-267)Online publication date: 26-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-16912-0_9
Willis JWu NPickering M(2020)Staged selective parser combinatorsProceedings of the ACM on Programming Languages10.1145/34090024:ICFP(1-30)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3409002
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents