University of Oxford Logo University of OxfordDepartment of Computer Science - Home
On Facebook
Facebook
Follow us on twitter
Twitter
Linked in
Linked in
Flickr
Flickr
Google plus
Google plus
Digg
Digg
Pinterest
Pinterest
Stumble Upon
Stumble Upon

Unifying Structured Recursion Schemes

Ralf Hinze‚ Nicolas Wu and Jeremy Gibbons

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. The link between the two schemes is provided by the fusion rule of categorical fixed-point calculus.

Details

Book Title

International Conference on Functional Programming

Month

March

Note

Accepted for publication

Year

2013

Links

BibTeX

Link (pdf)

Related pages

People

Projects

Activities

Themes