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

lmcs:894 - Logical Methods in Computer Science, September 3, 2014, Volume 10, Issue 3
When is a container a comonad?

Authors: Ahman, Danel and Chapman, James and Uustalu, Tarmo

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.


Source : oai:arXiv.org:1408.5809
DOI : 10.2168/LMCS-10(3:14)2014
Volume: Volume 10, Issue 3
Published on: September 3, 2014
Submitted on: June 25, 2015
Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science,Mathematics - Category Theory


Share

Browsing statistics

This page has been seen 52 times.
This article's PDF has been downloaded 19 times.