Danel Ahman ; James Chapman ; Tarmo Uustalu - When is a container a comonad?

lmcs:894 - Logical Methods in Computer Science, September 3, 2014, Volume 10, Issue 3 - https://doi.org/10.2168/LMCS-10(3:14)2014
When is a container a comonad?Article

Authors: Danel Ahman ORCID; James Chapman ORCID; Tarmo Uustalu ORCID

    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.

    Volume: Volume 10, Issue 3
    Published on: September 3, 2014
    Imported on: December 5, 2012
    Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science,Mathematics - Category Theory

    9 Documents citing this article

    Consultation statistics

    This page has been seen 1716 times.
    This article's PDF has been downloaded 472 times.