More Web Proxy on the site http://driver.im/

research-article

Open access

Modular Models of Monoids with Operations

Authors:

Nicolas WuAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 7, Issue ICFP

Article No.: 208, Pages 566 - 603

https://doi.org/10.1145/3607850

Published: 31 August 2023 Publication History

Abstract

Inspired by algebraic effects and the principle of notions of computations as monoids, we study a categorical framework for equational theories and models of monoids equipped with operations. The framework covers not only algebraic operations but also scoped and variable-binding operations. Appealingly, in this framework both theories and models can be modularly composed. Technically, a general monoid-theory correspondence is shown, saying that the category of theories of algebraic operations is equivalent to the category of monoids. Moreover, more complex forms of operations can be coreflected into algebraic operations, in a way that preserves initial algebras. On models, we introduce modular models of a theory, which can interpret abstract syntax in the presence of other operations. We show constructions of modular models (i) from monoid transformers, (ii) from free algebras, (iii) by composition, and (iv) in symmetric monoidal categories.

References

[1]

Jiří Adámek. 1974. Free Algebras and Automata Realizations in the Language of Categories. Commentationes Mathematicae Universitatis Carolinae, 015, 4 (1974), 589–602. http://eudml.org/doc/16649

[2]

Jiří Adámek and Jiří Rosicky. 1994. Locally Presentable and Accessible Categories. Cambridge University Press. https://doi.org/10.1017/CBO9780511600579

[3]

Robert Atkey. 2009. Parameterised notions of computation. Journal of Functional Programming, 19, 3–4 (2009), 335–376. issn:09567968 https://doi.org/10.1017/S095679680900728X

Digital Library

[4]

Casper Bach Poulsen and Cas van der Rest. 2023. Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects. Proc. ACM Program. Lang., 7, POPL (2023), Article 62, Jan, 31 pages. https://doi.org/10.1145/3571255

Digital Library

[5]

Pietro Cenciarelli and Eugenio Moggi. 1993. A Syntactic Approach to Modularity in Denotational Semantics. In Proceedings of the Conference on Category Theory and Computer Science. https://doi.org/10.1.1.41.7807

[6]

Paul M. Cohn. 1981. Universal Algebra. Springer Dordrecht. https://doi.org/10.1007/978-94-009-8399-1

[7]

Brian Day. 1970. On Closed Categories of Functors. In Reports of the Midwest Category Seminar IV, S. MacLane, H. Applegate, M. Barr, B. Day, E. Dubuc, Phreilambud, A. Pultr, R. Street, M. Tierney, and S. Swierczkowski (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 1–38. isbn:978-3-540-36292-0

[8]

Andrzej Filinski. 1994. Representing Monads. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’94). Association for Computing Machinery, New York, NY, USA. 446–457. isbn:0897916360 https://doi.org/10.1145/174675.178047

Digital Library

[9]

Andrzej Filinski. 1999. Representing Layered Monads. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’99). Association for Computing Machinery, New York, NY, USA. 175–188. isbn:1581130953 https://doi.org/10.1145/292540.292557

Digital Library

[10]

Marcelo Fiore. 2008. Second-Order and Dependently-Sorted Abstract Syntax. In Proceedings of the 2008 23rd Annual IEEE Symposium on Logic in Computer Science (LICS ’08). IEEE Computer Society, USA. 57–68. isbn:9780769531830 https://doi.org/10.1109/LICS.2008.38

Digital Library

[11]

Marcelo Fiore and Chung-Kil Hur. 2007. Equational Systems and Free Constructions. In Proceedings of the 34th International Conference on Automata, Languages and Programming (ICALP’07). Springer-Verlag, Berlin, Heidelberg. 607–618. isbn:3540734198 https://doi.org/10.1007/978-3-540-73420-8_53

[12]

Marcelo Fiore and Chung-Kil Hur. 2009. On the Construction of Free Algebras for Equational Systems. Theoretical Computer Science, 410, 18 (2009), 1704–1729. issn:0304-3975 https://doi.org/10.1016/j.tcs.2008.12.052

Digital Library

[13]

Marcelo Fiore and Ola Mahmoud. 2014. Functorial Semantics of Second-Order Algebraic Theories. https://doi.org/10.48550/ARXIV.1401.4697

[14]

Marcelo Fiore, Gordon Plotkin, and Daniele Turi. 1999. Abstract Syntax and Variable Binding. In Proceedings. 14th Symposium on Logic in Computer Science. 193–202. https://doi.org/10.1109/LICS.1999.782615

[15]

Marcelo Fiore and Philip Saville. 2017. List Objects with Algebraic Structure. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), Dale Miller (Ed.) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 84). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany. 16:1–16:18. isbn:978-3-95977-047-7 issn:1868-8969 https://doi.org/10.4230/LIPIcs.FSCD.2017.16

[16]

Marcelo Fiore and Sam Staton. 2014. Substitution, jumps, and algebraic effects. Proceedings of the Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic, CSL 2014 and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2014, isbn:9781450328869 https://doi.org/10.1145/2603088.2603163

Digital Library

[17]

Marcelo Fiore and Dmitrij Szamozvancev. 2022. Formal Metatheory of Second-Order Abstract Syntax. Proc. ACM Program. Lang., 6, POPL (2022), Article 53, Jan, 29 pages. https://doi.org/10.1145/3498715

Digital Library

[18]

Neil Ghani and Patricia Johann. 2007. Monadic Augment and Generalised Short Cut Fusion. Journal of Functional Programming, 17, 6 (2007), 731–776. https://doi.org/10.1017/S0956796807006314

Digital Library

[19]

Neil Ghani and Tarmo Uustalu. 2004. Coproducts of Ideal Monads. RAIRO - Theoretical Informatics and Applications, 38, 4 (2004), Oct, 321–342. issn:0988-3754 https://doi.org/10.1051/ita:2004016

[20]

Neil Ghani, Tarmo Uustalu, and Makoto Hamana. 2006. Explicit Substitutions and Higher-Order Syntax. Higher-Order and Symbolic Computation, https://doi.org/10.1007/s10990-006-8748-4

Digital Library

[21]

Jeremy Gibbons, Donnacha Oisín Kidney, Tom Schrijvers, and Nicolas Wu. 2022. Breadth-First Traversal via Staging. In Mathematics of Program Construction, Ekaterina Komendantskaya (Ed.). Springer International Publishing, Cham. 1–33. isbn:978-3-031-16912-0 https://doi.org/10.1007/978-3-031-16912-0_1

Digital Library

[22]

Andy Gill and Edward Kmett. 2012. mtl: Monad classes, using functional dependencies. https://hackage.haskell.org/package/mtl

[23]

Andrew Gill, John Launchbury, and Simon L. Peyton Jones. 1993. A Short Cut to Deforestation. In Proceedings of the Conference on Functional Programming Languages and Computer Architecture (FPCA ’93). Association for Computing Machinery, New York, NY, USA. 223–232. isbn:089791595X https://doi.org/10.1145/165180.165214

Digital Library

[24]

Claudio Hermida. 2000. Representable Multicategories. Advances in Mathematics, 151, 2 (2000), 164–225. issn:0001-8708 https://doi.org/10.1006/aima.1999.1877

[25]

Ralf Hinze. 2012. Kan Extensions for Program Optimisation Or: Art and Dan Explain an Old Trick. In Mathematics of Program Construction, Jeremy Gibbons and Pablo Nogueira (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 324–362. https://doi.org/10.1007/978-3-642-31113-0_16

Digital Library

[26]

John Hughes. 1986. A Novel Representation of Lists and its Application to the Function "reverse". Inf. Process. Lett., 22 (1986), 01, 141–144.

Digital Library

[27]

John Hughes. 2000. Generalising Monads to Arrows. Science of Computer Programming, 37, 1 (2000), 67–111. issn:0167-6423 https://doi.org/10.1016/S0167-6423(99)00023-4

Digital Library

[28]

Martin Hyland. 2017. Classical Lambda Calculus in Modern Dress. Mathematical Structures in Computer Science, 27, 5 (2017), 762–781. https://doi.org/10.1017/S0960129515000377

[29]

Bart Jacobs. 1999. Categorical Logic and Type Theory (Studies in Logic and the Foundations of Mathematics). North Holland, Amsterdam.

[30]

Bart Jacobs, Chris Heunen, and Ichiro Hasuo. 2009. Categorical Semantics for Arrows. Journal of Functional Programming, 19, 3-4 (2009), 403–438. https://doi.org/10.1017/S0956796809007308

Digital Library

[31]

Mauro Jaskelioff and Eugenio Moggi. 2010. Monad Transformers as Monoid Transformers. Theoretical Computer Science, 411 (2010), 12, 4441–4466. https://doi.org/10.1016/j.tcs.2010.09.011

Digital Library

[32]

Shin-ya Katsumata. 2014. Parametric Effect Monads and Semantics of Effect Systems. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’14). Association for Computing Machinery, New York, NY, USA. 633–645. isbn:9781450325448 https://doi.org/10.1145/2535838.2535846

Digital Library

[33]

Shin-ya Katsumata, Dylan McDermott, Tarmo Uustalu, and Nicolas Wu. 2022. Flexible Presentations of Graded Monads. Proc. ACM Program. Lang., 6, ICFP (2022), Article 123, Aug, 29 pages. https://doi.org/10.1145/3547654

Digital Library

[34]

G.M. Kelly and John Power. 1993. Adjunctions whose counits are coequalizers, and presentations of finitary enriched monads. Journal of Pure and Applied Algebra, 89, 1 (1993), 163–179. issn:0022-4049 https://doi.org/10.1016/0022-4049(93)90092-8

[35]

G. M. Kelly. 1982. Structures defined by finite limits in the enriched context, I. Cahiers de Topologie et Géométrie Différentielle Catégoriques, 23, 1 (1982), 3–42.

[36]

Donnacha Oisín Kidney and Nicolas Wu. 2021. Algebras for Weighted Search. Proc. ACM Program. Lang., 5, ICFP (2021), Article 72, Aug, 30 pages. https://doi.org/10.1145/3473577

Digital Library

[37]

Oleg Kiselyov and Hiromi Ishii. 2015. Freer Monads, More Extensible Effects. SIGPLAN Not., 50, 12 (2015), Aug, 94–105. issn:0362-1340 https://doi.org/10.1145/2887747.2804319

Digital Library

[38]

Anders Kock. 1972. Strong Functors and Monoidal Monads. Archiv der Mathematik, 23 (1972), 12, 113–120. https://doi.org/10.1007/BF01304852

[39]

Satoshi Kura. 2020. Graded Algebraic Theories. In Foundations of Software Science and Computation Structures, Jean Goubault-Larrecq and Barbara König (Eds.). Springer International Publishing, Cham. 401–421. isbn:978-3-030-45231-5 https://doi.org/10.1007/978-3-030-45231-5_21

Digital Library

[40]

J. Lambek and P. J. Scott. 1986. Introduction to Higher Order Categorical Logic. Cambridge University Press. isbn:978-0-521-35653-4

[41]

F. William Lawvere. 1963. Functorial Semantics of Algebraic Theories. Proceedings of the National Academy of Sciences, 50, 5 (1963), 869–872. https://doi.org/10.1073/pnas.50.5.869

[42]

Sheng Liang, Paul Hudak, and Mark Jones. 1995. Monad Transformers and Modular Interpreters. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’95). ACM, 333–343. isbn:0-89791-692-1 https://doi.org/10.1145/199448.199528

Digital Library

[43]

F. E. J. Linton. 1966. Some Aspects of Equational Categories. In Proceedings of the Conference on Categorical Algebra, S. Eilenberg, D. K. Harrison, S. MacLane, and H. Röhrl (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 84–94. isbn:978-3-642-99902-4 https://doi.org/10.1007/978-3-642-99902-4_3

[44]

Fosco Loregian. 2021. (Co)end Calculus. Cambridge University Press. https://doi.org/10.1017/9781108778657

[45]

Saunders Mac Lane. 1998. Categories for the Working Mathematician, 2nd edn. Springer, Berlin.

[46]

Conor Mcbride and Ross Paterson. 2008. Applicative Programming with Effects. Journal of Functional Programming, 18, 1 (2008), Jan., 1–13. issn:0956-7968 https://doi.org/10.1017/S0956796807006326

Digital Library

[47]

Dylan McDermott and Tarmo Uustalu. 2022. Flexibly Graded Monads and Graded Algebras. In Mathematics of Program Construction, Ekaterina Komendantskaya (Ed.). Springer International Publishing, Cham. 102–128. isbn:978-3-031-16912-0 https://doi.org/10.1007/978-3-031-16912-0_4

Digital Library

[48]

Dylan McDermott and Tarmo Uustalu. 2022. What Makes a Strong Monad? Electronic Proceedings in Theoretical Computer Science, 360 (2022), Jun, 113–133. issn:2075-2180 https://doi.org/10.4204/EPTCS.360.6

[49]

Eugenio Moggi. 1989. An Abstract View of Programming Languages. Edinburgh University, Department of Computer Science.

[50]

Eugenio Moggi. 1989. Computational Lambda-Calculus and Monads. In Proceedings. Fourth Annual Symposium on Logic in Computer Science. 14–23. https://doi.org/10.1109/LICS.1989.39155

[51]

Eugenio Moggi. 1991. Notions of Computation and Monads. Information and Computation, 93, 1 (1991), 55 – 92. issn:0890-5401 https://doi.org/10.1016/0890-5401(91)90052-4 Selections from 1989 IEEE Symposium on Logic in Computer Science

Digital Library

[52]

Andrey Mokhov, Neil Mitchell, and Simon Peyton Jones. 2018. Build Systems à La Carte. Proc. ACM Program. Lang., 2, ICFP (2018), Article 79, Jul, 29 pages. https://doi.org/10.1145/3236774

Digital Library

[53]

Ross Paterson. 2012. Constructing applicative functors. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 7342 LNCS (2012), 300–323. isbn:9783642311123 issn:16113349 https://doi.org/10.1007/978-3-642-31113-0_15

Digital Library

[54]

Ruben P. Pieters, Exequiel Rivas, and Tom Schrijvers. 2020. Generalized Monoidal Effects and Handlers. Journal of Functional Programming, 30 (2020), e23. https://doi.org/10.1017/S0956796820000106

[55]

Maciej Piróg, Tom Schrijvers, Nicolas Wu, and Mauro Jaskelioff. 2018. Syntax and Semantics for Operations with Scopes. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, Anuj Dawar and Erich Grädel (Eds.).

Digital Library

[56]

Gordon Plotkin and John Power. 2001. Semantics for Algebraic Operations. Electronic Notes in Theoretical Computer Science, 45 (2001), 332–345. issn:1571-0661 https://doi.org/10.1016/S1571-0661(04)80970-8

[57]

Gordon Plotkin and John Power. 2002. Notions of Computation Determine Monads. In Foundations of Software Science and Computation Structures, 5th International Conference, Mogens Nielsen and Uffe Engberg (Eds.) (FOSSACS 2002). Springer, 342–356. https://doi.org/10.1007/3-540-45931-6_24

[58]

Gordon Plotkin and John Power. 2003. Algebraic Operations and Generic Effects. Applied Categorical Structures, 11, 1 (2003), Feb., 69–94. issn:1572-9095 https://doi.org/10.1023/A:1023064908962

[59]

Gordon Plotkin and John Power. 2004. Computational Effects and Operations: An Overview. Electr. Notes Theor. Comput. Sci., 73 (2004), 10, 149–163. https://doi.org/10.1016/j.entcs.2004.08.008

Digital Library

[60]

Gordon Plotkin and Matija Pretnar. 2013. Handling Algebraic Effects. Logical Methods in Computer Science, 9, 4 (2013), Dec, issn:1860-5974 https://doi.org/10.2168/lmcs-9(4:23)2013

[61]

John Power. 1999. Enriched Lawvere Theories. Theory and Applications of Categories, 6, 7 (1999), 83–93.

[62]

John C. Reynolds. 1983. Types, Abstraction and Parametric Polymorphism. In IFIP Congress.

[63]

Exequiel Rivas and Mauro Jaskelioff. 2017. Notions of Computation as Monoids. Journal of Functional Programming, 27, September (2017), Oct, issn:0956-7968 https://doi.org/10.1017/S0956796817000132 arxiv:1406.4823.

[64]

Ian Stark. 2008. Free-algebra models for the π -calculus. Theoretical Computer Science, 390, 2 (2008), 248–270. issn:0304-3975 https://doi.org/10.1016/j.tcs.2007.09.024 Foundations of Software Science and Computational Structures

Digital Library

[65]

Wouter Swierstra. 2008. Data types à la carte. Journal of Functional Programming, 18, 4 (2008), 423–436. https://doi.org/10.1017/S0956796808006758

Digital Library

[66]

Robert D Tennent. 1991. Semantics of programming languages. 1, Prentice Hall New York.

[67]

Janis Voigtländer. 2008. Asymptotic Improvement of Computations over Free Monads. In Mathematics of Program Construction, Philippe Audebaud and Christine Paulin-Mohring (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 388–403. isbn:978-3-540-70594-9 https://doi.org/10.1007/978-3-540-70594-9_20

Digital Library

[68]

Philip Wadler. 1995. Monads for Functional Programming. In Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques-Tutorial Text. Springer-Verlag, Berlin, Heidelberg. 24–52. isbn:3540594515 https://doi.org/10.5555/647698.734146

Digital Library

[69]

Nicolas Wu, Tom Schrijvers, and Ralf Hinze. 2014. Effect Handlers in Scope. Proceedings of the 2014 ACM SIGPLAN Symposium on Haskell - Haskell ’14, 1–12. isbn:9781450330411 issn:03621340 https://doi.org/10.1145/2633357.2633358

Digital Library

[70]

Zhixuan Yang, Marco Paviotti, Nicolas Wu, Birthe van den Berg, and Tom Schrijvers. 2022. Structured Handling of Scoped Effects. Springer-Verlag, Berlin, Heidelberg. 462–491. isbn:978-3-030-99335-1 https://doi.org/10.1007/978-3-030-99336-8_17

Digital Library

[71]

Zhixuan Yang and Nicolas Wu. 2021. Reasoning about Effect Interaction by Fusion. Proc. ACM Program. Lang., 5, ICFP (2021), Article 73, Aug., 29 pages. https://doi.org/10.1145/3473578

Digital Library

Cited By

Bunkenburg NWu NVazou NMorris J(2024)Making a Curry Interpreter using Effects and HandlersProceedings of the 17th ACM SIGPLAN International Haskell Symposium10.1145/3677999.3678279(68-82)Online publication date: 29-Aug-2024
https://dl.acm.org/doi/10.1145/3677999.3678279
Kidney DYang ZWu N(2024)Algebraic Effects Meet Hoare Logic in Cubical AgdaProceedings of the ACM on Programming Languages10.1145/36328988:POPL(1663-1695)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632898

Index Terms

Modular Models of Monoids with Operations

Index terms have been assigned to the content through auto-classification.

Recommendations

The lattice of L-ideals of a ring is modular

In this paper, we extend the notion of a tip-extended pair of fuzzy subgroups to L-ideals of a ring. We prove that the sum of two tip-extended L-ideals of an arbitrary pair of L-ideals of a ring is the least L-ideal containing the union of the given L-...
Monads, zippers and views: virtualizing the monad stack
ICFP '11

We make monadic components more reusable and robust to changes by employing two new techniques for virtualizing the monad stack: the monad zipper and monad views. The monad zipper is a higher-order monad transformer that creates virtual monad stacks by ...
Monads, zippers and views: virtualizing the monad stack
ICFP '11: Proceedings of the 16th ACM SIGPLAN international conference on Functional programming

We make monadic components more reusable and robust to changes by employing two new techniques for virtualizing the monad stack: the monad zipper and monad views. The monad zipper is a higher-order monad transformer that creates virtual monad stacks by ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 7, Issue ICFP

August 2023

981 pages

EISSN:2475-1421

DOI:10.1145/3554311

Editor:
Michael Hicks
Amazon, USA

Issue’s Table of Contents

Copyright © 2023 Owner/Author.

This work is licensed under a Creative Commons Attribution 4.0 International License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 31 August 2023

Published in PACMPL Volume 7, Issue ICFP

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Engineering and Physical Sciences Research Council

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
500
Total Downloads

Downloads (Last 12 months)306
Downloads (Last 6 weeks)29

Reflects downloads up to 06 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Bunkenburg NWu NVazou NMorris J(2024)Making a Curry Interpreter using Effects and HandlersProceedings of the 17th ACM SIGPLAN International Haskell Symposium10.1145/3677999.3678279(68-82)Online publication date: 29-Aug-2024
https://dl.acm.org/doi/10.1145/3677999.3678279
Kidney DYang ZWu N(2024)Algebraic Effects Meet Hoare Logic in Cubical AgdaProceedings of the ACM on Programming Languages10.1145/36328988:POPL(1663-1695)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632898

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents