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.
The main content of the talk is about eating `infinite’ objects that
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