Search Results

Documents authored by Purdy, Chris

Artifact
Software
DOI: 10.4230/artifacts.24062
chrisjpurdy/distr-laws-of-monadic-containers

Authors: Chris Purdy and Stefania Damato

Abstract
Cite as

Chris Purdy, Stefania Damato. chrisjpurdy/distr-laws-of-monadic-containers (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-24062,
   title = {{chrisjpurdy/distr-laws-of-monadic-containers}}, 
   author = {Purdy, Chris and Damato, Stefania},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:8d906ffab8f8a03982b563930c72ea835fd9d64a;origin=https://github.com/chrisjpurdy/distr-laws-of-monadic-containers;visit=swh:1:snp:053b593aa05da0a8be19fd62a74e2acaf9afad94;anchor=swh:1:rev:2c5f94536e8a52b98e3dc466b07511f106acb882}{\texttt{swh:1:dir:8d906ffab8f8a03982b563930c72ea835fd9d64a}} (visited on 2025-07-28)},
   url = {https://github.com/chrisjpurdy/distr-laws-of-monadic-containers},
   doi = {10.4230/artifacts.24062},
}
Artifact
Software
DOI: 10.4230/artifacts.24064
chrisjpurdy/distr-laws-of-monadic-containers HTML rendering

Authors: Chris Purdy and Stefania Damato

Abstract
Cite as

Chris Purdy, Stefania Damato. chrisjpurdy/distr-laws-of-monadic-containers HTML rendering (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-24064,
   title = {{chrisjpurdy/distr-laws-of-monadic-containers HTML rendering}}, 
   author = {Purdy, Chris and Damato, Stefania},
   note = {Software (visited on 2025-07-28)},
   url = {https://stefaniatadama.com/distr-law-mnd-cont-html/},
   doi = {10.4230/artifacts.24064},
}
Artifact
Software
DOI: 10.4230/artifacts.24065
stefaniatadama/cubical

Authors: Chris Purdy and Stefania Damato

Abstract
Cite as

Chris Purdy, Stefania Damato. stefaniatadama/cubical (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-24065,
   title = {{stefaniatadama/cubical}}, 
   author = {Purdy, Chris and Damato, Stefania},
   note = {Software (visited on 2025-07-28)},
   url = {https://github.com/stefaniatadama/cubical/tree/distr-laws},
   doi = {10.4230/artifacts.24065},
}
Document
DOI: 10.4230/LIPIcs.CALCO.2025.4
Distributive Laws of Monadic Containers

Authors: Chris Purdy and Stefania Damato

Published in: LIPIcs, Volume 342, 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Abstract
Containers are used to carve out a class of strictly positive data types in terms of shapes and positions. They can be interpreted via a fully-faithful functor into endofunctors on Set. Monadic containers are those containers whose interpretation as a Set functor carries a monad structure. The category of containers is closed under container composition and is a monoidal category, whereas monadic containers do not in general compose. In this paper, we develop a characterisation of distributive laws of monadic containers. Distributive laws were introduced as a sufficient condition for the composition of the underlying functors of two monads to also carry a monad structure. Our development parallels Ahman and Uustalu’s characterisation of distributive laws of directed containers, i.e. containers whose Set functor interpretation carries a comonad structure. Furthermore, by combining our work with theirs, we construct characterisations of mixed distributive laws (i.e. of directed containers over monadic containers and vice versa), thereby completing the "zoo" of container characterisations of (co)monads and their distributive laws. We have found these characterisations amenable to development of existence and uniqueness proofs of distributive laws, particularly in the mechanised setting of Cubical Agda, in which most of the theory of this paper has been formalised.
Cite as

Chris Purdy and Stefania Damato. Distributive Laws of Monadic Containers. In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 4:1-4:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{purdy_et_al:LIPIcs.CALCO.2025.4,
  author =	{Purdy, Chris and Damato, Stefania},
  title =	{{Distributive Laws of Monadic Containers}},
  booktitle =	{11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)},
  pages =	{4:1--4:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-383-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{342},
  editor =	{C\^{i}rstea, Corina and Knapp, Alexander},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2025.4},
  URN =		{urn:nbn:de:0030-drops-235633},
  doi =		{10.4230/LIPIcs.CALCO.2025.4},
  annote =	{Keywords: distributive laws, monadic containers, monads, dependent types, cubical agda}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact