What Makes a Strong Monad?

Dylan McDermott
Tarmo Uustalu

Strong monads are important for several applications, in particular, in the denotational semantics of effectful languages, where strength is needed to sequence computations that have free variables. Strength is non-trivial: it can be difficult to determine whether a monad has any strength at all, and monads can be strong in multiple ways. We therefore review some of the most important known facts about strength and prove some new ones. In particular, we present a number of equivalent characterizations of strong functor and strong monad, and give some conditions that guarantee existence or uniqueness of strengths. We look at strength from three different perspectives: actions of a monoidal category V, enrichment over V, and powering over V. We are primarily motivated by semantics of effects, but the results are also useful in other contexts.

In Jeremy Gibbons and Max S. New: Proceedings Ninth Workshop on Mathematically Structured Functional Programming (MSFP 2022), Munich, Germany, 2nd April 2022, Electronic Proceedings in Theoretical Computer Science 360, pp. 113–133.
Published: 30th June 2022.

ArXived at: http://dx.doi.org/10.4204/EPTCS.360.6 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org