University of Birmingham > Talks@bham > Lab Lunch > When is a Container a Comonad?

When is a Container a Comonad?

Add to your list(s) Download to your calendar using vCal

  • UserDanel Ahman, University of Cambridge
  • ClockTuesday 13 December 2011, 12:00-13:00
  • HouseCS 217.

If you have a question about this talk, please contact Dan Ghica.

Abbott, Altenkirch, Ghani and others have taught us that many parameterized datatypes (set functors) can be usefully analyzed via container representations in terms of a set of shapes and a set of positions in each shape.

Our work builds on the observation that datatypes often carry additional structure that containers alone do not account for. We introduce directed containers to capture the common situation where every position in a datastructure determines another datastructure, informally, the sub-datastructure rooted by that position. Some natural examples are non-empty lists and node-labelled trees, and datastructures with a designated position (zippers).

While containers denote set functors via a fully-faithful functor, directed containers interpret fully-faithfully into comonads. But more is true: every comonad whose underlying functor is a container is represented by a directed container. In fact, directed containers are the same as containers that are comonads.

We have formalized our development in the dependently typed programming language Agda.

This talk is part of the Lab Lunch series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.