Strict and lazy semantics for effects: layering monads and comonads
Article No.: 88, Pages 1 - 30
Abstract
Two particularly important classes of effects are those that can be given semantics using a monad and those that can be given semantics using a comonad. Currently, programs with both kinds of effects are usually given semantics using a technique that relies on a distributive law. While it is known that not every pair of a monad and a comonad has a distributive law, it was previously unknown if there were any realistic pairs of effects that could not be given semantics in this manner. This paper answers that question by giving an example of a pair of effects that cannot be given semantics using a distributive law. Our example furthermore is intimately tied to the duality of strictness and laziness. We discuss how to view this duality through the lens of effects.
Supplementary Material
References
[1]
Samson Abramsky. 1994. Proofs as Processes . Theoretical Computer Science 135, 1 (1994), 5–9.
[2]
Jean-Marc Andreoli. 1992. Logic Programming with Focusing Proofs in Linear Logic . Journal of Logic and Computation 2 (1992), 297–347.
[3]
Zena M. Ariola, Matthias Felleisen, John Maraist, Martin Odersky, and Philip Wadler. 1995. A Call-By-Need Lambda Calculus . In POPL. ACM, New York, NY, USA, 233–246.
[4]
Robert Atkey. 2009. Parameterised Notions of Computation . Journal of Functional Programming 19, 3-4 (2009), 335–376.
[5]
Emmanuel Beffara. 2006. A Concurrent Model for Linear Logic . ENTCS 155 (2006), 147–168.
[6]
G. Bellin and P. J. Scott. 1994. On the π -Calculus and Linear Logic . Theoretical Computer Science 135, 1 (1994), 11–65.
[7]
Jean Bénabou. 1963. Catégories avec Multiplication . Comptes Rendus de l’Académie des Sciences Paris 258 (1963), 771–774.
[8]
Stephen Brookes and Shai Geva. 1992. Computational Comonads and Intensional Semantics . In Applications of Categories in Computer Science. Cambridge University Press, Cambridge, UK, 1–44.
[9]
Stephen Brookes and Kathryn van Stone. 1993. Monads and Comonads in Intensional Semantics . Technical Report CMU-CS-93-140. Carnegie Mellon University Department of Computer Science.
[10]
Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. 2014. A Core Quantitative Coeffect Calculus . In Programming Languages and Systems. Springer Berlin Heidelberg, Berlin, Heidelberg, 351–370.
[11]
Alonzo Church and J. B. Rosser. 1936. Some Properties of Conversion . Trans. Amer. Math. Soc. 39, 3 (1936), 472–482.
[12]
Pierre-Louis Curien, Marcelo Fiore, and Guillaume Munch-Maccagnoni. 2016. A Theory of Effects and Resources: Adjunction Models and Polarised Calculi . In POPL. ACM, New York, NY, USA, 44–56.
[13]
Pierre-Louis Curien and Hugo Herbelin. 2000. The Duality of Computation . In ICFP. ACM, New York, NY, USA, 233–243.
[14]
Vincent Danos, Jean-Baptiste Joinet, and Harold Schellinx. 1997. A New Deconstructive Logic: Linear Logic . The Journal of Symbol Logic 62, 3 (1997), 755–807.
[15]
Henry DeYoung, Luís Caires, Frank Pfenning, and Bernardo Toninho. 2012. Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication . In CSL, Vol. 16. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 228–242.
[16]
Jeff Egger, Rasmus Ejlers Møgelberg, and Alex Simpson. 2014. The Enriched Effect Calculus: Syntax and Semantics . Journal of Logic and Computation 24, 3 (2014), 615–654.
[17]
Andrzej Filinski. 1999. Representing Layered Monads . In POPL. ACM, New York, NY, USA, 175–188.
[18]
Andrzej Filinski. 2010. Monads in Action . In POPL. ACM, New York, NY, USA, 483–494.
[19]
Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Flavien Breuvart, and Tarmo Uustalu. 2016. Combining Effects and Coeffects via Grading . In ICFP. ACM, New York, NY, USA, 476–489.
[20]
Gerhard Gentzen. 1934. Untersuchungen über das logische Schließen I . Mathematische Zeitschrift 39 (1934), 176–210.
[21]
Gerhard Gentzen. 1935. Untersuchungen über das logische Schließen II . Mathematische Zeitschrift 39 (1935), 405–431.
[22]
Jean-Yves Girard. 1987. Linear Logic . Theoretical Computer Science 50, 1 (1987), 1–101.
[23]
Jean-Yves Girard. 1991. A New Constructive Logic: Classical Logic . Research Report RR-1443. INRIA.
[24]
Michael Hicks, Gavin Bierman, Nataliya Guts, Daan Leijen, and Nikhil Swamy. 2014. Polymonadic Programming . EPTCS 153 (2014), 79–99.
[25]
Andrew K. Hirsch and Ross Tate. 2018. Strict and Lazy Semantics for Effects: Layering Monads and Comonads . In ICFP. ACM, New York, NY, USA, Technical Report.
[26]
Martin Hyland, Gordon Plotkin, and John Power. 2006. Combining Effects: Sum and Tensor . Theoretical Computer Science 357, 1 (2006), 70–99.
[27]
Joachim Lambek. 1969. Deductive Systems and Categories II. Standard Constructions and Closed Categories . In Category Theory, Homology Theory and Their Applications I. Springer Berlin Heidelberg, Berlin, Heidelberg, 76–122.
[28]
Tom Leinster. 1998. General Operads and Multicategories . (1998).
[29]
Paul Blain Levy. 1999. Call-By-Push-Value: A Subsuming Paradigm . In Typed Lambda Calculus and Applications. Springer Berlin Heidelberg, Berlin, Heidelberg, 228–243.
[30]
Paul Blain Levy. 2001. Call-By-Push-Value . Ph.D. Dissertation. Queen Mary and Westfield College University of London, London, UK.
[31]
Francisco J. López-Fraguas, Juan Rodríguez-Hortalá, and Jaime Sánchez-Hernández. 2007. A Simple Rewrite Notion for Call-time Choice Semantics . In PPDP. ACM, New York, NY, USA, 197–208.
[32]
John M. Lucassen and David K. Gifford. 1988. Polymorphic Effect Systems . In POPL. ACM, New York, NY, USA, 47–57.
[33]
Christoph Lüth and Neil Ghani. 2002. Composing Monads using Coproducts . In ICFP. ACM, New York, NY, USA, 133–144.
[34]
Saunders Mac Lane. 1963. Natural Associativiy and Commutativity . Rice University Studies 49, 4 (1963), 28–46.
[35]
John Maraist, Martin Odersky, David N. Turner, and Philip Wadler. 1995. Call-by-Name, Call-by-Value, Call-by-Need, and the Linear Lambda Calculus . ENTCS 1 (1995), 370–392.
[36]
Daniel Marino and Todd Millstein. 2009. A Generic Type-and-Effect System . In TLDI. ACM, New York, NY, USA, 39–50.
[37]
Robin Milner, Joachim Parrow, and David Walker. 1992. A Calculus of Mobile Processes, I . Information and Computation 100, 1 (1992), 1–40.
[38]
Eugenio Moggi. 1989. Computational Lambda-Calculus and Monads . In LICS. IEEE, Piscataway Township, NJ, USA, 14–23.
[39]
Flemming Nielson. 1996. Annotated Type and Effect Systems . Comput. Surveys 28, 2 (1996), 344–345.
[40]
Flemming Nielson and Hanne Riis Nielson. 1999. Type and Effect Systems . In Correct System Design: Recent Insights and Advances. Springer Berlin Heidelberg, Berlin, Heidelberg, 114–136.
[41]
Michel Parigot. 1992a. Free Deduction: An Analysis of “Computations” in Classical Logic . In Logic Programming. Springer Berlin Heidelberg, Berlin, Heidelberg, 361–380.
[42]
Michel Parigot. 1992b. λµ-Calculus: An Algorithmic Interpretation of Classical Natural Deduction . In Logic Programming and Automated Reasoning. Springer Berlin Heidelberg, Berlin, Heidelberg, 190–201.
[43]
Tomas Petricek, Dominic Orchard, and Alan Mycroft. 2013. Coeffects: Unified Static Analysis of Context-Dependence . In ICALP. Springer-Verlag, Berlin, Heidelberg, 385–397.
[44]
Tomas Petricek, Dominic Orchard, and Alan Mycroft. 2014. Coeffects: A Calculus of Context-Dependent Computation . In ICFP. ACM, New York, NY, USA, 123–135.
[45]
Simon L. Peyton Jones and Philip Wadler. 1993. Imperative Functional Programming . In POPL. ACM, New York, NY, USA, 71–84.
[46]
G. D. Plotkin. 1975. Call-By-Name, Call-By-Value, and the λ-Calculus . Theoretical Computer Science 1, 2 (1975), 125–159.
[47]
John Power and Hiroshi Watanabe. 2002. Combining a Monad and a Comonad . Theoretical Computer Science 280, 1 (2002), 137–162.
[48]
Amr Sabry and Philip Wadler. 1996. A Reflection on Call-by-Value . In ICFP. ACM, New York, NY, USA, 13–24.
[49]
Harold Schellinx. 1994. The Noble Art of Linear Decorating . Ph.D. Dissertation. Unerversiteit van Amsterdam, Amsterdam, Netherlands.
[50]
M. E. Szabo. 1975. Polycategories . Communications in Algebra 3, 8 (1975), 663–689.
[51]
Ross Tate. 2013. The Sequential Semantics of Producer Effect Systems . In POPL. ACM, New York, NY, USA, 15–26.
[52]
Tarmu Uustalu and Varmo Vene. 2005. Signals and Comonads . Journal of Universal Computer Science 11, 7 (2005), 1310–1326.
[53]
Tarmo Uustalu and Varmo Vene. 2008. Comonadic Notions of Computation . ENTCS 203, 5 (2008), 263–284.
[54]
Philip Wadler. 1990. Linear Types Can Change the World! . In Programming Concepts and Methods. North-Holland, Amsterdam, Netherlands, 1–21.
[55]
Philip Wadler. 2003. Call-by-Value is Dual to Call-by-Name . In ICFP. ACM, New York, NY, USA, 189–201.
[56]
Philip Wadler. 2012. Propositions as Sessions . In ICFP. ACM, New York, NY, USA, 273–286.
[57]
Philip Wadler and Peter Thiemann. 2003. The Marriage of Effects and Monads . Transactions on Computational Logic 4, 1 (2003), 1–32.
[58]
Noam Zeilberger. 2009. The Logical Basis of Evaluation Order and Pattern-Matching . Ph.D. Dissertation. Carnegie Mellon University, Pittsburgh, Pennsylvania, USA.
Index Terms
- Strict and lazy semantics for effects: layering monads and comonads
Recommendations
Monads and distributive laws for Rota-Baxter and differential algebras
In recent years, algebraic studies of the differential calculus and integral calculus in the forms of differential algebra and Rota-Baxter algebra have been merged together to reflect the close relationship between the two calculi through the First ...
Monads and Adjunctions for Global Exceptions
In this paper, we look at two categorical accounts of computational effects (strong monad as a model of the monadic metalanguage, adjunction as a model of call-by-push-value with stacks), and we adapt them to incorporate global exceptions. In each case, ...
Complete iterativity for algebras with effects
CALCO'09: Proceedings of the 3rd international conference on Algebra and coalgebra in computer scienceCompletely iterative algebras (cias) are those algebras in which recursive equations have unique solutions. In this paper we study complete iterativity for algebras with computational effects (described by a monad). First, we prove that for every ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2018 Owner/Author.
This work is licensed under a Creative Commons Attribution-NoDerivatives International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 30 July 2018
Published in PACMPL Volume 2, Issue ICFP
Check for updates
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 666Total Downloads
- Downloads (Last 12 months)81
- Downloads (Last 6 weeks)11
Reflects downloads up to 09 Jan 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in