When is a container a comonad?

TL;DR

This paper introduces directed containers, a structure that captures when container-based data types can be endowed with a comonad structure, extending the container framework to account for additional data-structure relationships.

Contribution

It formalizes directed containers as a new structure linking containers and comonads, providing a characterization of when container functors can be equipped with a comonad structure.

Findings

Directed containers correspond exactly to containers that are comonads.

Every comonad with a container underlying functor can be represented by a directed container.

Formalization achieved in Agda.

Abstract

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. This paper 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 data-structure determines another data-structure, informally, the sub-data-structure rooted by that position. Some natural examples are non-empty lists and node-labelled trees, and data-structures 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 also describe some constructions of directed containers. We have formalized our development in the dependently typed programming language Agda.