Directed containers

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 work 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 datastructure determines another datastructure, informally, the sub-datastructure rooted by that position. Some natural examples are non-empty lists and node-labelled trees, and datastructures 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.

Involved in the project

• Danel Ahman
• James Chapman
• Tarmo Uustalu

Publications

• D. Ahman, T. Uustalu. Taking Updates Seriously
  In R. Eramo, M. Johnson, eds., Proc. of 6th Int. Wksh. on Bidirectional Transformations, BX 2017 (Uppsala, April 2017), v. 1827 of CEUR Workshop Proceedings, pp. 59-73. CEUR-WS, 2017. (pdf)
• D. Ahman, T. Uustalu. Directed containers as categories
  In R. Atkey, N. Krishnaswami, eds., Proc. of 6th Wksh. on Mathematically Structured Functional Programming, MSFP 2016 (Eindhoven, April 2016), v. 207 of Electron. Proc. in Theor. Comput. Sci., pp. 89-98. Open Publishing Assoc., 2016. (doi link, pdf)
• D. Ahman, T. Uustalu. Coalgebraic update lenses
  In B. Jacobs, A. Silva, S. Staton, eds., Proc. of 30th Conf. on Mathematical Foundations of Programming Semantics, MFPS XXX (Ithaca, NY, June 2014), Electron. Notes in Theor. Comput. Sci., v. 308, pp. 25-48. Elsevier, 2014. (doi link, pdf © Elsevier)
• D. Ahman, T. Uustalu. Update Monads: Cointerpreting Directed Containers
  In R. Matthes, A. Schubert, eds., Post-proc. of the 19th Meeting "Types for Proofs and Programs", TYPES 2013, Leibniz International Proceedings in Informatics, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Dagstuhl Publishing, pp. 1--23, 2014 (doi link , pdf)
  
• D. Ahman, T. Uustalu. Distributive laws of directed containers
  Progress in Informatics, v. 10, pp. 3-18, 2013. (doi link, pdf)
  
• D. Ahman, J. Chapman, T. Uustalu. When is a container a comonad?
  Logical Methods in Computer Science, v. 10, n. 3, article 14, 2014. (doi link, pdf)
  Conference version in L. Birkedal, ed., Proc. of 15th Int. Conf. on Foundations of Software Science and Computation Structures, FoSSaCS 2012 (Tallinn, March 2012), v. 7213 of Lect. Notes in Comput. Sci., pp. 74-88. Springer, 2012. (doi link, pdf © Springer)

GitHub repository of our Agda formalisation

• GitHub repository

• Containers, container morphisms
• Directed containers, directed container morphisms*
• Functors, comonads
• Containers interpretation to functors and its fully faithfulness
• Directed containers interpretation to comonads and its fully faithfulness
• Examples of directed containers: Binary trees, lists, streams, morphisms