research-article

The sequential semantics of producer effect systems

Author:

Ross TateAuthors Info & Claims

POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 15 - 26

https://doi.org/10.1145/2429069.2429074

Published: 23 January 2013 Publication History

Abstract

Effects are fundamental to programming languages. Even the lambda calculus has effects, and consequently the two famous evaluation strategies produce different semantics. As such, much research has been done to improve our understanding of effects. Since Moggi introduced monads for his computational lambda calculus, further generalizations have been designed to formalize increasingly complex computational effects, such as indexed monads followed by layered monads followed by parameterized monads. This succession prompted us to determine the most general formalization possible. In searching for this formalization we came across many surprises, such as the insufficiencies of arrows, as well as many unexpected insights, such as the importance of considering an effect as a small component of a whole system rather than just an isolated feature. In this paper we present our semantic formalization for producer effect systems, which we call a productor, and prove its maximal generality by focusing on only sequential composition of effectful computations, consequently guaranteeing that the existing monadic techniques are specializations of productors.

Supplementary Material

JPG File (r1d1_talk4.jpg)

Download
10.84 KB

MP4 File (r1d1_talk4.mp4)

Download
175.31 MB

References

[1]

Martín Abadi. Access control in a core calculus of dependency. In ICFP, 2006.

Digital Library

[2]

Robert Atkey. Parameterised notions of computation. JFP, 19:335--376, July 2009.

Digital Library

[3]

Nick Benton, John Hughes, and Eugenio Moggi. Monads and effects. In International Summer School on Applied Semantics, 2000.

Digital Library

[4]

Olivier Danvy and Andrzej Filinski. A functional abstraction of typed contexts. Technical report, University of Copenhagen, 1989.

[5]

Andrzej Filinski. Representing layered monads. In POPL, 1999.

Digital Library

[6]

Andrzej Filinski. Monads in action. In POPL, 2010.

Digital Library

[7]

Roger Godement. Topologie Algébrique et Théorie des Faisceaux. Hermann, 1958.

[8]

John Hughes. Generalising monads to arrows. Science of Computer Programming, 37(1--3):67--111, May 2000.

Digital Library

[9]

Martin Hyland, Gordon Plotkin, and John Power. Combining effects: Sum and tensor. Theoretical Computer Science, 357(1):70--99, 2006.

Digital Library

[10]

Bart Jacobs, Chris Heunen, and Ichiro Hasuo. Categorical semantics for arrows. JFP, 19:403--438, 2009.

Digital Library

[11]

Mark P. Jones and Luc Duponcheel. Composing monads. Technical report, Yale University, New Haven, CT, USA, December 1993.

[12]

Simon Peyton Jones and Philip Wadler. Imperative functional programming. In POPL, 1993.

Digital Library

[13]

Richard B. Kieburtz. Taming effects with monadic typing. In ICFP, 1998.

Digital Library

[14]

David J. King and Philip Wadler. Combining monads. In ETAPS, 1992.

[15]

Tom Leinster. Higher Operads, Higher Categories. Cambridge University Press, 2004.

[16]

Sheng Liang, Paul Hudak, and Mark Jones. Monad transformers and modular interpreters. In POPL, 1995.

Digital Library

[17]

John M. Lucassen and David K. Gifford. Polymorphic effect systems. In POPL, 1988.

Digital Library

[18]

Christoph Lüth and Neil Ghani. Composing monads using coproducts. ACM SIGPLAN Notices, 37(9):133--144, 2002.

Digital Library

[19]

Daniel Marino and Todd Millstein. A generic type-and-effect system. In TLDI, 2009.

Digital Library

[20]

Eugenio Moggi. Computational lambda-calculus and monads. In LICS, 1989.

Digital Library

[21]

Iulian Neamtiu, Michael Hicks, Jeffrey S. Foster, and Polyvios Pratikakis. Contextual effects for version-consistent dynamic software updating and safe concurrent programming. In POPL, 2008.

Digital Library

[22]

Flemming Nielson and Hanne Riis Nielson. Type and effect systems. In ACM Computing Surveys, 1999.

[23]

Hanne Riis Nielson, Flemming Nielson, and Torben Amtoft. Polymorphic subtyping for effect analysis: The static semantics. In LOMAPS, 1997.

[24]

Gordon Plotkin and John Power. Notions of computation determine monads. In FoSSaCS, 2002.

Digital Library

[25]

John Power and Edmund Robinson. Premonoidal categories and notions of computation. Mathematical Structures in Computer Science, 7:453--468, October 1997.

Digital Library

[26]

John Power and Hayo Thielecke. Environments, continuation semantics and indexed categories. In TACS, 1997.

Digital Library

[27]

John Power and Hayo Thielecke. Closed Freyd- and κ-categories. In ICAL, 1999.

Digital Library

[28]

John C. Reynolds. Using category theory to design implicit conversions and generic operators. LNCS, 94:211--258, 1980.

Digital Library

[29]

Nikhil Swamy, Nataliya Guts, Daan Leijen, and Michael Hicks. Lightweight monadic programming in ML. Technical report, Microsoft Research, 2011.

[30]

Jean-Pierre Talpin. Theoretical and Practical Aspects of Type and Effect Inference. PhD thesis, École des Mines de Paris and University Paris VI, Paris, France, 1993.

[31]

Jean-Pierre Talpin and Pierre Jouvelot. Polymorphic type, region and effect inference. JFP, 2:245--271, 1992.

[32]

Jean-Pierre Talpin and Pierre Jouvelot. The type and effect discipline. Information and Computation, 111(2):245--296, 1994.

Digital Library

[33]

Ross Tate. The sequential semantics of producer effect systems. Technical report, Cornell University, 2012.

[34]

Andrew P. Tolmach. Optimizing ML using a hierarchy of monadic types. In Types in Compilation, 1998.

Digital Library

[35]

Philip Wadler. Comprehending monads. In LISP and Functional Programming, 1990.

Digital Library

[36]

Philip Wadler. The essence of functional programming. In POPL, 1992.

Digital Library

[37]

Philip Wadler. Monads and composable continuations. LISP and Symbolic Computation, 7:39--56, January 1994.

Digital Library

[38]

Philip Wadler and Peter Thiemann. The marriage of effects and monads. Transactions on Computational Logic, 4(1):1--32, 2003.

Digital Library

[39]

Andrew K. Wright. Simple imperative polymorphism. LISP and Symbolic Computation, 8(4):343--355, 1995.

Digital Library

Cited By

Yoshioka TSekiyama TIgarashi A(2024)Abstracting Effect Systems for Algebraic Effect HandlersProceedings of the ACM on Programming Languages10.1145/36746418:ICFP(455-484)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674641
Zhou ZYe QDelaware BJagannathan S(2024)A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite AutomataProceedings of the ACM on Programming Languages10.1145/36564338:PLDI(1387-1411)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656433
MOY CFELLEISEN M(2023)Trace contractsJournal of Functional Programming10.1017/S095679682300009633Online publication date: 13-Dec-2023
https://doi.org/10.1017/S0956796823000096
Show More Cited By

Index Terms

The sequential semantics of producer effect systems
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
      1. Semantics
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

Parametric effect monads and semantics of effect systems
POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

We study fundamental properties of a generalisation of monad called parametric effect monad, and apply it to the interpretation of general effect systems whose effects have sequential composition operators. We show that parametric effect monads admit ...
The sequential semantics of producer effect systems
POPL '13

Effects are fundamental to programming languages. Even the lambda calculus has effects, and consequently the two famous evaluation strategies produce different semantics. As such, much research has been done to improve our understanding of effects. ...
Combining effects and coeffects via grading
ICFP '16

Effects and coeffects are two general, complementary aspects of program behaviour. They roughly correspond to computations which change the execution context (effects) versus computations which make demands on the context (coeffects). Effectful ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2013

586 pages

ISBN:9781450318327

DOI:10.1145/2429069

General Chair:
Roberto Giacobazzi
Università di Verona, Italy
,
Program Chair:
Radhia Cousot
École normale supérieure CNRS & INRIA, France

ACM SIGPLAN Notices Volume 48, Issue 1
POPL '13
January 2013
561 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2480359
Issue’s Table of Contents

Copyright © 2013 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2013

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '13

Sponsor:

SIGPLAN

POPL '13: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 23 - 25, 2013

Rome, Italy

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

30
Total Citations
View Citations
588
Total Downloads

Downloads (Last 12 months)12
Downloads (Last 6 weeks)3

Reflects downloads up to 23 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Yoshioka TSekiyama TIgarashi A(2024)Abstracting Effect Systems for Algebraic Effect HandlersProceedings of the ACM on Programming Languages10.1145/36746418:ICFP(455-484)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674641
Zhou ZYe QDelaware BJagannathan S(2024)A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite AutomataProceedings of the ACM on Programming Languages10.1145/36564338:PLDI(1387-1411)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656433
MOY CFELLEISEN M(2023)Trace contractsJournal of Functional Programming10.1017/S095679682300009633Online publication date: 13-Dec-2023
https://doi.org/10.1017/S0956796823000096
Gordon CYun C(2023)Error Localization for Sequential Effect SystemsStatic Analysis10.1007/978-3-031-44245-2_16(343-370)Online publication date: 24-Oct-2023
https://doi.org/10.1007/978-3-031-44245-2_16
de Ferro CCogumbreiro TMartins F(2023)Shelley: A Framework for Model Checking Call Ordering on Hierarchical SystemsCoordination Models and Languages10.1007/978-3-031-35361-1_5(93-114)Online publication date: 15-Jun-2023
https://doi.org/10.1007/978-3-031-35361-1_5
Dagnino F(2022)A Meta-theory for Big-step SemanticsACM Transactions on Computational Logic10.1145/352272923:3(1-50)Online publication date: 6-Apr-2022
https://dl.acm.org/doi/10.1145/3522729
Gordon C(2021)Polymorphic Iterable Sequential Effect SystemsACM Transactions on Programming Languages and Systems10.1145/345027243:1(1-79)Online publication date: 17-Apr-2021
https://dl.acm.org/doi/10.1145/3450272
Hirsch ACecchetti E(2021)Giving semantics to program-counter labels via secure effectsProceedings of the ACM on Programming Languages10.1145/34343165:POPL(1-29)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434316
Nester C(2021)A Variety Theorem for Relational Universal AlgebraRelational and Algebraic Methods in Computer Science10.1007/978-3-030-88701-8_22(362-377)Online publication date: 22-Oct-2021
https://doi.org/10.1007/978-3-030-88701-8_22
Gaboardi MKatsumata SOrchard DSato T(2021)Graded Hoare Logic and its Categorical SemanticsProgramming Languages and Systems10.1007/978-3-030-72019-3_9(234-263)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-72019-3_9
Show More Cited By

View Options

Get Access

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 Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents