Unifying Structured Recursion Schemes

by Nicolas Wu

Posted on 20 March 2014

Last year at ICFP 2013 I presented Unifying Structured Recursion Schemes, which was joint work with Ralf Hinze and Jeremy Gibbons. A few people asked me if I would be able to make the presentation available online, so here it is on youtube:

The talk dances over a lot of the interesting details, so I hope that if you’re interested, you’ll read the paper. You can download a copy here.

Here’s the 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.

I’m just about done with an extended version of the paper that goes into some more details about unfolds, and also shows how monadic folds arise out of the Kleisli adjunction.