When is a container a comonad?

Abbott, Altenkirch, Ghani and others have taught us that many parameterizeddatatypes (set functors) can be usefully analyzed via container representationsin terms of a set of shapes and a set of positions in each shape. This paperbuilds on the observation that datatypes often carry additional structure thatcontainers alone do not account for. We introduce directed containers tocapture the common situation where every position in a data-structuredetermines another data-structure, informally, the sub-data-structure rooted bythat position. Some natural examples are non-empty lists and node-labelledtrees, and data-structures with a designated position (zippers). Whilecontainers denote set functors via a fully-faithful functor, directedcontainers interpret fully-faithfully into comonads. But more is true: everycomonad whose underlying functor is a container is represented by a directedcontainer. In fact, directed containers are the same as containers that arecomonads. We also describe some constructions of directed containers. We haveformalized our development in the dependently typed programming language Agda