Thursday, 22 September 2011, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101
Abstract: From the work of Abbott, Altenkirch and Ghani, we know that it is possible to characterise many datatypes in terms of containers. A container is defined as a set of shapes and a family of positions for each shape corresponding to the intuition that datastructures often consist of templates where the actual data payload is mapped into. It is also known that an interpretation of a container is a functor from a set to a set of pairs of shapes and assignments of elements from the given set to every position and that container morphisms can be interpreted as natural transformations between such functors.
Our work is based on the observation that datatypes sometimes carry additional structure that the container structure alone does not account for. We introduce the notion of directed containers where every position fixes another (sub)container to be able to talk about such datastructures. We illustrate the theory on datastructures such as lists, streams, trees and zippers.
We also show that directed containers are closely related to comonads - every directed container can be interpreted as a comonad and every comonad whose underlying functor is an interpretation of a container represents a directed container. In addition, we show a similar relationship between directed container morphisms and comonad morphisms.
(Joint work with James Chapman and Tarmo Uustalu.)