Monads need not be endofunctors

Thosten Altenkirch; James Chapman; Tarmo Uustalu

doi:10.2168/LMCS-11(1:3)2015

Thosten Altenkirch ; James Chapman ; Tarmo Uustalu - Monads need not be endofunctors

lmcs:928 - Logical Methods in Computer Science, March 6, 2015, Volume 11, Issue 1 - https://doi.org/10.2168/LMCS-11(1:3)2015

Monads need not be endofunctorsArticle

Authors: Thosten Altenkirch ; James Chapman ; Tarmo Uustalu

We introduce a generalization of monads, called relative monads, allowing for underlying functors between different categories. Examples include finite-dimensional vector spaces, untyped and typed lambda-calculus syntax and indexed containers. We show that the Kleisli and Eilenberg-Moore constructions carry over to relative monads and are related to relative adjunctions. Under reasonable assumptions, relative monads are monoids in the functor category concerned and extend to monads, giving rise to a coreflection between relative monads and monads. Arrows are also an instance of relative monads.

https://doi.org/10.2168/LMCS-11(1:3)2015

Source: arXiv.org:1412.7148

Volume: Volume 11, Issue 1

Published on: March 6, 2015

Imported on: May 4, 2011

Keywords: Computer Science - Programming Languages,Computer Science - Logic in Computer Science,Mathematics - Category Theory

Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

29 Documents citing this article

Niccolò Veltri, Lecture notes in computer science, Maximally Multi-focused Proofs for Skew Non-Commutative MILL, pp. 377-393, 2023, 10.1007/978-3-031-39784-4_24.

Philipp G. Haselwarter;Exequiel Rivas;Antoine Van Muylder;Théo Winterhalter;Carmine Abate;et al., 2023, SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq, ACM Transactions on Programming Languages and Systems, 45, 3, pp. 1-61, 10.1145/3594735, https://doi.org/10.1145/3594735.

Rory B. B. Lucyshyn-Wright;Jason Parker, 2023, Diagrammatic Presentations of Enriched Monads and Varieties for a Subcategory of Arities, Applied Categorical Structures, 31, 5, 10.1007/s10485-023-09735-y.

André Hirschowitz;Tom Hirschowitz;Ambroise Lafont;Marco Maggesi, Lecture notes in computer science, Variable binding and substitution for (nameless) dummies, pp. 389-408, 2022, 10.1007/978-3-030-99253-8_20, https://doi.org/10.1007/978-3-030-99253-8_20.

Daniel Marshall;Michael Vollmer;Dominic Orchard, Lecture notes in computer science, Linearity and Uniqueness: An Entente Cordiale, pp. 346-375, 2022, 10.1007/978-3-030-99336-8_13, https://doi.org/10.1007/978-3-030-99336-8_13.

Dylan McDermott;Tarmo Uustalu, Lecture notes in computer science, Flexibly Graded Monads and Graded Algebras, pp. 102-128, 2022, 10.1007/978-3-031-16912-0_4.

Shin-ya Katsumata;Dylan McDermott;Tarmo Uustalu;Nicolas Wu, 2022, Flexible presentations of graded monads, Proceedings of the ACM on Programming Languages, 6, ICFP, pp. 902-930, 10.1145/3547654, https://doi.org/10.1145/3547654.

Tarmo Uustalu;Niccolò Veltri;Cheng-Syuan Wan, 2022, Proof Theory of Skew Non-Commutative MILL, arXiv (Cornell University), 358, pp. 118-135, 10.4204/eptcs.358.9.

Vladimir Voevodsky, 2022, C-system of a module over a Jf-relative monad, Journal of Pure and Applied Algebra, 227, 6, pp. 107283, 10.1016/j.jpaa.2022.107283, https://doi.org/10.1016/j.jpaa.2022.107283.

Arjen Rouvoet;Robbert Krebbers;Eelco Visser, 2021, Intrinsically typed compilation with nameless labels, Proceedings of the ACM on Programming Languages, 5, POPL, pp. 1-28, 10.1145/3434303, https://doi.org/10.1145/3434303.

GUILLAUME ALLAIS;ROBERT ATKEY;JAMES CHAPMAN;CONOR MCBRIDE;JAMES MCKINNA, 2021, A type- and scope-safe universe of syntaxes with binding: their semantics and proofs, Edinburgh Research Explorer (University of Edinburgh), 31, 10.1017/s0956796820000076, https://www.research.ed.ac.uk/en/publications/e7211deb-a004-4aba-b7d0-31a697c0e1b9.

Richard Garner;Jean-Simon Pacaud Lemay, 2021, Cartesian Differential Categories as Skew Enriched Categories, Applied Categorical Structures, 29, 6, pp. 1099-1150, 10.1007/s10485-021-09649-7, https://doi.org/10.1007/s10485-021-09649-7.

André Hirschowitz;Tom Hirschowitz;Ambroise Lafont, Modules over monads and operational semantics, 2020, 10.4230/lipics.fscd.2020.12, https://hal.archives-ouvertes.fr/hal-02338144.

Arjen Rouvoet;Casper Bach Poulsen;Robbert Krebbers;Eelco Visser, Research Repository (Delft University of Technology), Intrinsically-typed definitional interpreters for linear, session-typed languages, 2020, New Orleans LA USA, 10.1145/3372885.3373818, http://resolver.tudelft.nl/uuid:913a5c7f-d521-445e-82af-a7771849f964.

Peio Borthelle;Tom Hirschowitz;Ambroise Lafont, A Cellular Howe Theorem, 84, pp. 273-286, 2020, Saarbrücken Germany, 10.1145/3373718.3394738, https://hal.science/hal-02880876/file/main.pdf.

Tarmo Uustalu;Niccolò Veltri;Noam Zeilberger, 2020, Eilenberg-Kelly Reloaded, Electronic Notes in Theoretical Computer Science, 352, pp. 233-256, 10.1016/j.entcs.2020.09.012, https://doi.org/10.1016/j.entcs.2020.09.012.

ANDREAS ABEL;GUILLAUME ALLAIS;ALIYA HAMEER;BRIGITTE PIENTKA;ALBERTO MOMIGLIANO;et al., 2019, POPLMark reloaded: Mechanizing proofs by logical relations, Archivio Istituzionale della Ricerca (Universita Degli Studi Di Milano), 29, 10.1017/s0956796819000170, https://hdl.handle.net/2434/695543.

Arthur Azevedo de Amorim;Marco Gaboardi;Justin Hsu;Shin-ya Katsumata, arXiv (Cornell University), Probabilistic Relational Reasoning via Metrics, 2019, Vancouver, BC, Canada, 10.1109/lics.2019.8785715, https://arxiv.org/abs/1807.05091.

Benedikt Ahrens;André Hirschowitz;Ambroise Lafont;Marco Maggesi, 2019, Reduction monads and their signatures, Proceedings of the ACM on Programming Languages, 4, POPL, pp. 1-29, 10.1145/3371099, https://doi.org/10.1145/3371099.

Härmel Nestra, Lecture notes in computer science, Laws of Monadic Error Handling, pp. 372-391, 2019, 10.1007/978-3-030-32505-3_21.

James Chapman;Roman Kireev;Chad Nester;Philip Wadler, Edinburgh Research Explorer (University of Edinburgh), System F in Agda, for Fun and Profit, pp. 255-297, 2019, 10.1007/978-3-030-33636-3_10, http://hdl.handle.net/20.500.11820/62107dbc-a5b7-4361-a28d-7ce0635f73c8.

Kenji Maillard;Cătălin Hriţcu;Exequiel Rivas;Antoine Van Muylder, 2019, The next 700 relational program logics, Proceedings of the ACM on Programming Languages, 4, POPL, pp. 1-33, 10.1145/3371072, https://doi.org/10.1145/3371072.

Makoto Hamana;Tatsuya Abe;Kentaro Kikuchi, 2019, Polymorphic computation systems: Theory and practice of confluence with call-by-value, Science of Computer Programming, 187, pp. 102322, 10.1016/j.scico.2019.102322, https://doi.org/10.1016/j.scico.2019.102322.

Oleg Kiselyov, 2019, Effects Without Monads: Non-determinism – Back to the Meta Language, arXiv (Cornell University), 294, pp. 15-40, 10.4204/eptcs.294.2.

Dusko Pavlovic;Muzamil Yahia, arXiv (Cornell University), Monoidal Computer III: A Coalgebraic View of Computability and Complexity (Extended Abstract), pp. 167-189, 2018, 10.1007/978-3-030-00389-0_10, https://arxiv.org/abs/1704.04882.

Exequiel Rivas, 2018, Relating Idioms, Arrows and Monads from Monoidal Adjunctions, arXiv (Cornell University), 275, pp. 18-33, 10.4204/eptcs.275.3.

Tarmo Uustalu;Niccolò Veltri;Noam Zeilberger, 2018, The Sequent Calculus of Skew Monoidal Categories, Electronic Notes in Theoretical Computer Science, 341, pp. 345-370, 10.1016/j.entcs.2018.11.017, https://doi.org/10.1016/j.entcs.2018.11.017.

Marcelo Fiore, 2017, On the concrete representation of discrete enriched abstract clones, Tbilisi Mathematical Journal, 10, 3, 10.1515/tmj-2017-0115, https://doi.org/10.1515/tmj-2017-0115.

Danel Ahman;Tarmo Uustalu, 2016, Directed Containers as Categories, arXiv (Cornell University), 207, pp. 89-98, 10.4204/eptcs.207.5.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 2770 times.

This article's PDF has been downloaded 809 times.