When is a container a comonad?

DOI10.2168/LMCS-10(3:14)2014MaRDI QIDQ2878762zbMATH OpenOpenAlexFDO

Authors Danel Ahman, James Chapman, Tarmo Uustalu

Publication date 5 September 2014

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1408.5809

zbMATH Keywords

Agdacomonadsdatatypesdependently typed programmingcontainers

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

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.

Recommendations

• When is a container a comonad?
• Directed containers as categories
• Container combinatorics: monads and lax monoidal functors
• Complexity bounds for container functors and comonads
• Higher-order containers

Cited in

(13)

• Partiality and Container Monads
• No go theorems: directed containers that do not distribute over distribution monads
• Protocol choice and iteration for the free cornering
• Coalgebraic update lenses
• scientific article; zbMATH DE number 2061699 (Why is no real title available?)
• Complexity bounds for container functors and comonads
• Container combinatorics: monads and lax monoidal functors
• Internal split opfibrations and cofunctors
• Update monads: cointerpreting directed containers
• Decomposing Comonad Morphisms.
• Directed containers as categories
• When is a container a comonad?
• Quotienting the delay monad by weak bisimilarity

Describes a project that uses

Uses Software

• Agda

This page was built for publication: When is a container a comonad?

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2878762)