{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:03:27Z","timestamp":1767927807266,"version":"3.49.0"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2018,7,30]],"date-time":"2018-07-30T00:00:00Z","timestamp":1532908800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nd\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,7,30]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/3236783","type":"journal-article","created":{"date-parts":[[2018,7,31]],"date-time":"2018-07-31T19:41:18Z","timestamp":1533066078000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Strict and lazy semantics for effects: layering monads and comonads"],"prefix":"10.1145","volume":"2","author":[{"given":"Andrew K.","family":"Hirsch","sequence":"first","affiliation":[{"name":"Cornell University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ross","family":"Tate","sequence":"additional","affiliation":[{"name":"Cornell University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,7,30]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00103-0"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199507"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680900728X"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.055"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00104-9"},{"key":"e_1_2_2_7_1","volume-title":"Cat\u00e9gories avec Multiplication . Comptes Rendus de l\u2019Acad\u00e9mie des Sciences Paris 258","author":"B\u00e9nabou Jean","year":"1963","unstructured":"Jean B\u00e9nabou . 1963. Cat\u00e9gories avec Multiplication . Comptes Rendus de l\u2019Acad\u00e9mie des Sciences Paris 258 ( 1963 ), 771\u2013774. Jean B\u00e9nabou. 1963. Cat\u00e9gories avec Multiplication . Comptes Rendus de l\u2019Acad\u00e9mie des Sciences Paris 258 (1963), 771\u2013774."},{"key":"e_1_2_2_8_1","volume-title":"Applications of Categories in Computer Science","author":"Brookes Stephen","unstructured":"Stephen Brookes and Shai Geva . 1992. Computational Comonads and Intensional Semantics . In Applications of Categories in Computer Science . Cambridge University Press , Cambridge, UK , 1\u201344. Stephen Brookes and Shai Geva. 1992. Computational Comonads and Intensional Semantics . In Applications of Categories in Computer Science. Cambridge University Press, Cambridge, UK, 1\u201344."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1936-1501858-0"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837652"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351262"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275572"},{"key":"e_1_2_2_15_1","volume-title":"CSL","volume":"16","author":"DeYoung Henry","year":"2012","unstructured":"Henry DeYoung , Lu\u00eds Caires , Frank Pfenning , and Bernardo Toninho . 2012 . Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication . In CSL , Vol. 16 . Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 228\u2013242. Henry DeYoung, Lu\u00eds Caires, Frank Pfenning, and Bernardo Toninho. 2012. Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication . In CSL, Vol. 16. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 228\u2013242."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exs025"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292557"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706354"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951939"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201353"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201363"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.153.7"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.03.013"},{"key":"e_1_2_2_27_1","volume-title":"Category Theory","author":"Lambek Joachim","unstructured":"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\u2013122. 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\u2013122."},{"key":"e_1_2_2_28_1","unstructured":"Tom Leinster. 1998. General Operads and Multicategories . (1998).  Tom Leinster. 1998. General Operads and Multicategories . (1998)."},{"key":"e_1_2_2_29_1","volume-title":"Typed Lambda Calculus and Applications","author":"Levy Paul Blain","unstructured":"Paul Blain Levy . 1999. Call-By-Push-Value: A Subsuming Paradigm . In Typed Lambda Calculus and Applications . Springer Berlin Heidelberg , Berlin, Heidelberg , 228\u2013243. Paul Blain Levy. 1999. Call-By-Push-Value: A Subsuming Paradigm . In Typed Lambda Calculus and Applications. Springer Berlin Heidelberg, Berlin, Heidelberg, 228\u2013243."},{"key":"e_1_2_2_30_1","volume-title":"Queen Mary and Westfield College University of London","author":"Levy Paul Blain","unstructured":"Paul Blain Levy . 2001. Call-By- Push-Value . Ph . D. Dissertation . Queen Mary and Westfield College University of London , London, UK . Paul Blain Levy. 2001. Call-By-Push-Value . Ph.D. Dissertation. Queen Mary and Westfield College University of London, London, UK."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273920.1273947"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73564"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581492"},{"key":"e_1_2_2_34_1","first-page":"28","article-title":"Natural Associativiy and Commutativity","volume":"49","author":"Lane Saunders Mac","year":"1963","unstructured":"Saunders Mac Lane . 1963 . Natural Associativiy and Commutativity . Rice University Studies 49 , 4 (1963), 28 \u2013 46 . Saunders Mac Lane. 1963. Natural Associativiy and Commutativity . Rice University Studies 49, 4 (1963), 28\u201346.","journal-title":"Rice University Studies"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00022-2"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481868"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"e_1_2_2_38_1","volume-title":"Computational Lambda-Calculus and Monads","author":"Moggi Eugenio","unstructured":"Eugenio Moggi . 1989. Computational Lambda-Calculus and Monads . In LICS. IEEE , Piscataway Township, NJ, USA , 14\u201323. Eugenio Moggi. 1989. Computational Lambda-Calculus and Monads . In LICS. IEEE, Piscataway Township, NJ, USA, 14\u201323."},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/234528.234745"},{"key":"e_1_2_2_40_1","volume-title":"Correct System Design: Recent Insights and Advances","author":"Nielson Flemming","unstructured":"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\u2013136. 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\u2013136."},{"key":"e_1_2_2_41_1","volume-title":"Free Deduction: An Analysis of \u201cComputations","author":"Parigot Michel","year":"1992","unstructured":"Michel Parigot . 1992 a. Free Deduction: An Analysis of \u201cComputations \u201d in Classical Logic . In Logic Programming. Springer Berlin Heidelberg , Berlin, Heidelberg, 361\u2013380. Michel Parigot. 1992a. Free Deduction: An Analysis of \u201cComputations\u201d in Classical Logic . In Logic Programming. Springer Berlin Heidelberg, Berlin, Heidelberg, 361\u2013380."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/645706.663989"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39212-2_35"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628160"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158524"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00024-X"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/232627.232631"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1080\/00927877508822067"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429074"},{"key":"e_1_2_2_52_1","first-page":"1310","article-title":"Signals and Comonads","volume":"11","author":"Uustalu Tarmu","year":"2005","unstructured":"Tarmu Uustalu and Varmo Vene . 2005 . Signals and Comonads . Journal of Universal Computer Science 11 , 7 (2005), 1310 \u2013 1326 . Tarmu Uustalu and Varmo Vene. 2005. Signals and Comonads . Journal of Universal Computer Science 11, 7 (2005), 1310\u20131326.","journal-title":"Journal of Universal Computer Science"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.05.029"},{"key":"e_1_2_2_54_1","volume-title":"Programming Concepts and Methods. North-Holland","author":"Wadler Philip","unstructured":"Philip Wadler . 1990. Linear Types Can Change the World! . In Programming Concepts and Methods. North-Holland , Amsterdam, Netherlands , 1\u201321. Philip Wadler. 1990. Linear Types Can Change the World! . In Programming Concepts and Methods. North-Holland, Amsterdam, Netherlands, 1\u201321."},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944723"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364568"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/601775.601776"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236783","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3236783","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T21:41:28Z","timestamp":1750282888000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236783"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,30]]},"references-count":53,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2018,7,30]]}},"alternative-id":["10.1145\/3236783"],"URL":"https:\/\/doi.org\/10.1145\/3236783","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,7,30]]},"assertion":[{"value":"2018-07-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}