internalization and categorical algebra
algebra object (associative, Lie, …)
internal category ($\to$ more)
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
In computer science and specifically in type theory, a monad transformer is a type constructor which takes a monad as an argument and returns a monad as a result. The concept is typically treated in the literature on monads in computer science.
Monad transformers generally derive from ordinary monads and allow a modular composition, so that the action on the identity monad of the associated transform $M T$ of a monad $M$ is equivalent to $M$.
This construction is sometimes viewed (see HP07, Eff) as a complication resulting from passing to monads from the setting of Lawvere theories, where any two theories may be naturally combined.
Textbook account:
See also
Bryan O’Sullivan, Don Stewart, and John Goerzen, Monad transformers, Chapter 18 of Real World Haskell.
Chung-Chieh Shan, Monad transformers, blog post
Mauro Jaskelioff, Eugenio Moggi, Monad Transformers as Monoid Transformers, pdf
Oleksandr Manzyuk, Calculating monad transformers with category theory, pdf
Martin Hyland, John Power, The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads, Electronic Notes in Theoretical Computer Science (ENTCS) archive Volume 172, April, 2007 Pages 437-458 (pdf)
Last revised on May 19, 2021 at 11:36:44. See the history of this page for a list of all contributions to it.