# Nottingham FP Lab Blog

## Container eating

by Hancock on February 28, 2009.
Tagged as: Lunches.

I think some asked me to post a link to the slides I used
for my talk last Friday.
They’re at http://www.cs.nott.ac.uk/~pgh/cont-eating-talk.pdf
(There are some backup slides at the end I didn’t use.)

Eating: beyond streams

Abstract
Eating’ is about writing programs that implement functions on final
coalgebras, typically stream types. The crucial thing is to do it in
a composable way, as with Unix-style piping.

I’ll quickly canter through stream eating, pointing out the use of
nested fixedpoints, and of universal properties to define things.
inhabit the final coalgebras of container functors.

For a long time I was stuck on how to do this in a composable way;
a few days ago I cracked it, and would like to show you how.
You can regard it as a study in dependently typed programming,
in which quite a few interesting things emerge.

****
Finally, many thanks for a really fun three and a half years in
Nottingham. And for the Talisker and baccy!
xxx,
Hank