research-article

Parametric effect monads and semantics of effect systems

Author:

Shin-ya KatsumataAuthors Info & Claims

POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Pages 633 - 645

https://doi.org/10.1145/2535838.2535846

Published: 08 January 2014 Publication History

Abstract

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 analogues of the structures and concepts that exist for monads, such as Kleisli triples, the state monad and the continuation monad, Plotkin and Power's algebraic operations, and the categorical ┬┬-lifting. We also show a systematic method to generate both effects and a parametric effect monad from a monad morphism. Finally, we introduce two effect systems with explicit and implicit subeffecting, and discuss their denotational semantics and the soundness of effect systems.

Supplementary Material

MP4 File (d3_right_t7.mp4)

Download
286.63 MB

References

[1]

R. M. Amadio and P.-L. Curien. Domains and lambda-calculi. Cambridge University Press, New York, NY, USA, 1998.

Digital Library

[2]

R. Atkey. Parameterised notions of computation. J. Funct. Program., 19(3--4):335--376, 2009.

Digital Library

[3]

G. Barthe, P. Dybjer, L. Pinto, and J. Saraiva, editors. Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures, volume 2395 of LNCS. Springer, 2002.

Digital Library

[4]

N. Benton and P. Buchlovsky. Semantics of an effect analysis for exceptions. In Proceedings of 2007 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, pages 15--26. ACM, 2007.

Digital Library

[5]

N. Benton, J. Hughes, and E. Moggi. Monads and effects. In Barthe et al. {3}, pages 42--122.

Digital Library

[6]

N. Benton, A. Kennedy, L. Beringer, and M. Hofmann. Relational semantics for effect-based program transformations with dynamic allocation. In Proceedings of the 9th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, pages 87--96. ACM, 2007.

Digital Library

[7]

N. Benton, A. Kennedy, L. Beringer, and M. Hofmann. Relational semantics for effect-based program transformations: higher-order store. In Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, pages 301--312. ACM, 2009.

Digital Library

[8]

N. Benton, A. Kennedy, M. Hofmann, and L. Beringer. Reading, writing and relations. In Programming Languages and Systems, 4th Asian Symposium, APLAS 2006, Proceedings, volume 4279 of LNCS, pages 114--130. Springer, 2006.

Digital Library

[9]

A. Filinski. Representing layered monads. In Proc. POPL 1999, pages 175--188, 1999.

Digital Library

[10]

J.-C. Filliǎtre. A theory of monads parameterized by effects. Research Report 1367, LRI, Université Paris Sud, November 1999.

[11]

B. Jacobs. Categorical Logic and Type Theory. Elsevier, 1999.

[12]

B. Jacobs. Coalgebraic trace semantics for combined possibilitistic and probabilistic systems. Electr. Notes Theor. Comput. Sci., 203(5):131--152, 2008.

Digital Library

[13]

O. Kammar and G. D. Plotkin. Algebraic foundations for effectdependent optimisations. In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 349--360. ACM, 2012.

Digital Library

[14]

S. Katsumata. A semantic formulation of ΤΤ-lifting and logical predicates for computational metalanguage. In Proc. CSL '05, volume 3634 of LNCS, pages 87--102. Springer, 2005.

Digital Library

[15]

S. Katsumata. Relating computational effects by ΤΤ-lifting. Inf. Comput., 222:228--246, 2013.

Digital Library

[16]

S. Katsumata and T. Sato. Preorders on monads and coalgebraic simulations. In Foundations of Software Science and Computation Structures - 16th International Conference, Proceedings, volume 7794 of LNCS, pages 145--160. Springer, 2013.

Digital Library

[17]

G.M. Kelly and G. Janelidze. A note on actions of a monoidal category. Theory and Applications of Categories, 9(4):61--91, 2001.

[18]

A. Kock. Strong functors and monoidal monads. Archiv der Mathe-matik, 23(1):113--120, 1972.

[19]

S. Lack and R. Street. The formal theory of monads ii. Journal of Pure and Applied Algebra, 175(1-3):243--265, 2002.

[20]

T. Leinster. Higher Operads, Higher Categories. London Mathematical Society Lecture Note Series. Cambridge University Press, 2004.

[21]

P. B. Levy. Call-by-Push-Value A Functiona/Imperative Synthesis. Springer, 2004.

Digital Library

[22]

J. M. Lucassen and D. K. Gifford. Polymorphic effect systems. In Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 47--57. ACM, 1988.

Digital Library

[23]

S. MacLane. Categories for the Working Mathematician (Second Edition), volume 5 of Graduate Texts in Mathematics. Springer, 1998.

[24]

P.-A. Mellies. Parametric monads and enriched adjunctions. Manuscript.

[25]

P.-A. Mellies. The parametric continuation monad. Mathematical Structures in Computer Science, Festschrift in honor of Corrado Böhm for his 90th birthday, 2013.

[26]

E. Moggi. Notions of computation and monads. Inf. Comput., 93(1):55--92, 1991.

Digital Library

[27]

F. Nielson and H. R. Nielson. From CML to its process algebra. Theor. Comput. Sci., 155:179--219, February 1996.

Digital Library

[28]

F. Nielson, H. R. Nielson, and C. Hankin. Principles of program analysis (2. corr. print). Springer, 2005.

[29]

T. Petricek, D. A. Orchard, and A. Mycroft. Coeffects: Unified static analysis of context-dependence. In Automata, Languages, and Programming - 40th International Colloquium, Proceedings, volume 7966 of LNCS, pages 385--397. Springer, 2013.

Digital Library

[30]

G. Plotkin and J. Power. Algebraic operations and generic effects. Applied Categorical Structures, 11(1):69--94, 2003.

[31]

L. Solberg, H. R. Nielson, and F. Nielson. Strictness and totality analysis. In Static Analysis, volume 864 of LNCS, pages 408--422. Springer Berlin Heidelberg, 1994.

[32]

J.-P. Talpin and P. Jouvelot. The type and effect discipline. Inf. Comput., 111(2):245--296, 1994.

Digital Library

[33]

R. Tate. The sequential semantics of producer effect systems. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 15--26. ACM, 2013.

Digital Library

[34]

J. Thamsborg and L. Birkedal. A kripke logical relation for effectbased program transformations. In Proceeding of the 16th ACM SIG- PLAN International Conference on Functional Programming, pages 445--456. ACM, 2011.

Digital Library

[35]

M. Tofte and J.-P. Talpin. Implementation of the typed call-by-value lambda-calculus using a stack of regions. In Proceedings of the 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 188--201, 1994.

Digital Library

[36]

D. Varacca and G. Winskel. Distributing probability over nondeterminism. Mathematical Structures in Computer Science, 16(1):87--113, 2006.

Digital Library

[37]

P. Wadler. The marriage of effects and monads. In Proceedings of the third ACM SIGPLAN International Conference on Functional Programming (ICFP '98), pages 63--74. ACM, 1998.

Digital Library

[38]

P.Wadler and P. Thiemann. The marriage of effects and monads. ACM Trans. Comput. Log., 4(1):1--32, 2003.

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
Paquet HSaville PSobocinski PLago UEsparza J(2024)Effectful semantics in bicategories: strong, commutative, and concurrent pseudomonadsProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662130(1-15)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662130
Kellison AHsu J(2024)Numerical Fuzz: A Type System for Rounding Error AnalysisProceedings of the ACM on Programming Languages10.1145/36564568:PLDI(1954-1978)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656456
Show More Cited By

Index Terms

Parametric effect monads and semantics of 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 constructs
      1. Type structures
    2. Program semantics

Recommendations

Flexible presentations of graded monads

A large class of monads used to model computational effects have natural presentations by operations and equations, for example, the list monad can be presented by a constant and a binary operation subject to unitality and associativity. Graded monads ...
Parametric effect monads and semantics of effect systems
POPL '14

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 ...
Observationally-induced Effect Monads: Upper and Lower Powerspace Constructions

Alex Simpson has suggested to use an observationally-induced approach towards modelling computational effects in denotational semantics. The principal idea is that a single observation algebra is used for defining the computational type structure. He ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 2014

702 pages

ISBN:9781450325448

DOI:10.1145/2535838

General Chair:
Suresh Jagannathan
Purdue University, USA
,
Program Chair:
Peter Sewell
University of Cambridge, UK

ACM SIGPLAN Notices Volume 49, Issue 1
POPL '14
January 2014
661 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2578855
Editor:
Mark W. Bailey
Hamilton College, Clinton, NY
Issue’s Table of Contents

Copyright © 2014 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 the author(s) 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: 08 January 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '14

Sponsor:

SIGPLAN

POPL '14: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 22 - 24, 2014

California, San Diego, USA

Acceptance Rates

POPL '14 Paper Acceptance Rate 51 of 220 submissions, 23%;

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

80
Total Citations
View Citations
1,249
Total Downloads

Downloads (Last 12 months)94
Downloads (Last 6 weeks)21

Reflects downloads up to 10 Nov 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
Paquet HSaville PSobocinski PLago UEsparza J(2024)Effectful semantics in bicategories: strong, commutative, and concurrent pseudomonadsProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662130(1-15)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662130
Kellison AHsu J(2024)Numerical Fuzz: A Type System for Rounding Error AnalysisProceedings of the ACM on Programming Languages10.1145/36564568:PLDI(1954-1978)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656456
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
Lopez FWalton C(2024)Twists of graded algebras in monoidal categoriesJournal of Algebra10.1016/j.jalgebra.2024.07.051Online publication date: Aug-2024
https://doi.org/10.1016/j.jalgebra.2024.07.051
Hughes JOrchard D(2024)Program Synthesis from Graded TypesProgramming Languages and Systems10.1007/978-3-031-57262-3_4(83-112)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57262-3_4
Paquet HSaville P(2023)Effectful Semantics in 2-Dimensional Categories: Premonoidal and Freyd BicategoriesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.397.12397(190-209)Online publication date: 14-Dec-2023
https://doi.org/10.4204/EPTCS.397.12
Breuvart FMcDermott DUustalu T(2023)Canonical Gradings of MonadsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.380.1380(1-21)Online publication date: 7-Aug-2023
https://doi.org/10.4204/EPTCS.380.1
Capobianco SUustalu T(2023)Additive Cellular Automata Graded-MonadicallyProceedings of the 25th International Symposium on Principles and Practice of Declarative Programming10.1145/3610612.3610625(1-9)Online publication date: 22-Oct-2023
https://dl.acm.org/doi/10.1145/3610612.3610625
Yang ZWu N(2023)Modular Models of Monoids with OperationsProceedings of the ACM on Programming Languages10.1145/36078507:ICFP(566-603)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607850
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