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

research-article

Combining effects and coeffects via grading

Authors:

Marco Gaboardi,

Shin-ya Katsumata,

Dominic Orchard,

Flavien Breuvart,

Tarmo UustaluAuthors Info & Claims

ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming

Pages 476 - 489

https://doi.org/10.1145/2951913.2951939

Published: 04 September 2016 Publication History

Abstract

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 features include partiality, non-determinism, input-output, state, and exceptions. Coeffectful features include resource demands, variable access, notions of linearity, and data input requirements. The effectful or coeffectful behaviour of a program can be captured and described via type-based analyses, with fine grained information provided by monoidal effect annotations and semiring coeffects. Various recent work has proposed models for such typed calculi in terms of graded (strong) monads for effects and graded (monoidal) comonads for coeffects. Effects and coeffects have been studied separately so far, but in practice many computations are both effectful and coeffectful, e.g., possibly throwing exceptions but with resource requirements. To remedy this, we introduce a new general calculus with a combined effect-coeffect system. This can describe both the changes and requirements that a program has on its context, as well as interactions between these effectful and coeffectful features of computation. The effect-coeffect system has a denotational model in terms of effect-graded monads and coeffect-graded comonads where interaction is expressed via the novel concept of graded distributive laws. This graded semantics unifies the syntactic type theory with the denotational model. We show that our calculus can be instantiated to describe in a natural way various different kinds of interaction between a program and its evaluation context.

References

[1]

M. Abadi, A. Banerjee, N. Heintze, and J. Riecke. A core calculus of dependency. In POPL ’99, pp. 147–160. ACM, 1999.

Digital Library

[2]

D. Ahman and T. Uustalu. Distributive laws of directed containers. Progr. in Inf., 10, pp. 3–18, 2013.

[3]

D. Ahman and T. Uustalu. Update monads: cointerpreting directed containers. In TYPES 2013, v. 13 of Leibniz Int. Proc. in Comput. Sci., pp. 1–23. Dagstuhl Publishing, 2014.

[4]

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

Digital Library

[5]

N. Benton, A. Kennedy, M. Hofmann, and V. Nigam. Counting successes: effects and transformations for non-deterministic programs. In A List of Successes That Can Change the World, v. 9600 of LNCS, pp. 56–72. Springer, 2016.

[6]

F. Breuvart and M. Pagani. Modelling coeffects in the relational semantics of linear logic. In CSL 2015, v. 41 of Leibniz Int. Proc. in Comput. Sci., pp. 567–581. Dagstuhl Publishing, 2015.

[7]

S. Brookes and K. V. Stone. Monads and comonads in intensional semantics. Techn. rep. CMU-CS-93-140. Carnegie-Mellon Univ., 1993.

Digital Library

[8]

A. Brunel, M. Gaboardi, D. Mazza, and S. Zdancewic. A core quantitative coeffect calculus. In ESOP 2014, v. 8410 of LNCS, pp. 351–370. Springer, 2014.

Digital Library

[9]

P. Curien, M. P. Fiore, and G. Munch-Maccagnoni. A theory of effects and resources: adjunction models and polarised calculi. In POPL ’16, pp. 44–56. ACM, 2016.

Digital Library

[10]

U. Dal Lago and M. Gaboardi. Linear dependent types and relative completeness. In LICS ’11, pp. 133–142. IEEE, 2011.

Digital Library

[11]

A. Filinski. Representing layered monads. In POPL ’99, pp. 175–188. ACM, 1999.

Digital Library

[12]

S. Fujii, S.-y. Katsumata, and P.-A. Melliès. Towards a formal theory of graded monads. In FoSSaCS 2016, v. 9634 of LNCS, pp. 513–530. Springer, 2016.

[13]

M. Gaboardi, A. Haeberlen, J. Hsu, A. Narayan, and B. C. Pierce. Linear dependent types for differential privacy. In POPL ’13, pp. 357– 370. ACM, 2013.

Digital Library

[14]

M. Gaboardi, S. Katsumata, D. Orchard, F. Breuvart, T. Uustalu. Combining Effects and Coeffects via Grading: Technical Report http: //dx.doi.org/10.17863/CAM.730

[15]

D. R. Ghica and A. I. Smith. Bounded linear types in a resource semiring. In ESOP 2014, v. 8410 of LNCS, pp. 331–350. Springer, 2014.

Digital Library

[16]

J. Gibbons. Comprehending ringads. In A List of Successes That Can Change the World, v. 9600 of LNCS, pp. 132–151. Springer, 2016.

[17]

D. K. Gifford and J. M. Lucassen. Integrating functional and imperative programming. In LISP and Funct. Prog. ’86, pp. 28–38. ACM, 1986.

Digital Library

[18]

J.-Y. Girard. Linear logic. Theor. Comput. Sci., 50, pp. 1–102, 1987.

Digital Library

[19]

J.-Y. Girard, A. Scedrov, and P. J. Scott. Bounded linear logic: a modular approach to polynomial-time computability. Theor. Comput. Sci., 97(1), pp. 1–66, 1992.

Digital Library

[20]

R. Harmer, M. Hyland, and P.-A. Melliès. Categorical combinatorics for innocent strategies. In LICS ’07, pp. 379–388. IEEE, 2007.

Digital Library

[21]

M. Hicks, G. M. Bierman, N. Guts, D. Leijen, and N. Swamy. Polymonadic programming. In MSFP 2014, v. 153 of Electron. Proc. in Theor. Comput. Sci., pp. 79–99. Open Publ. Assoc., 2014.

[22]

P. Jouvelot and D. Gifford. Algebraic reconstruction of types and effects. In POPL ’91, pp. 303–310. ACM, 1991.

Digital Library

[23]

C. Kassel. Quantum Groups. Graduate Texts in Mathematics. Springer, 1994.

[24]

S. Katsumata. Parametric effect monads and semantics of effect systems. In POPL ’14, pp. 633–646. ACM, 2014.

Digital Library

[25]

J. Lucassen and D. Gifford. Polymorphic effect systems. In POPL ’98, pp. 47–57. ACM, 1988.

Digital Library

[26]

C. McBride. I Got Plenty o’ Nuttin’. In A List of Successes That Can Change the World, v. 9600 of LNCS, pp. 207–233. Springer, 2016.

[27]

P. Melliès, N. Tabareau, and C. Tasson. An explicit formula for the free exponential modality of linear logic. In ICALP 2009, Part II, v. 5556 of LNCS, pp. 247–260. Springer, 2009.

Digital Library

[28]

P.-A. Melliès. Parametric monads and enriched adjunctions. Draft, 2012. http://www.pps.univ-paris-diderot.fr/~mellies/ tensorial-logic/.

[29]

S. Milius, D. Pattinson, and L. Schröder. Generic trace semantics and graded monads. In CALCO 2015, v. 35 of Leibniz Int. Proc. in Comput. Sci., pp. 253–269. Dagstuhl Publishing, 2015.

[30]

E. Moggi. Computational lambda-calculus and monads. In LICS ’89, pp. 14–23. IEEE, 1989.

Digital Library

[31]

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

Digital Library

[32]

A. Mycroft, D. Orchard, and T. Petricek. Effect systems revisited – control-flow algebra and semantics. In Semantics, Logics, and Calculi, v. 9560 of LNCS pp. 1–32. Springer, 2016.

Digital Library

[33]

A. Nanevski. From dynamic binding to state via modal possibility. In PPDP 2003, pp. 207–218. ACM, 2003.

Digital Library

[34]

A. Nanevski, F. Pfenning, and B. Pientka. Contextual modal type theory. ACM Trans. on Comput. Log., 9(3), article 23, 2008.

Digital Library

[35]

F. Nielson, H. R. Nielson, and C. L. Hankin. Principles of Program Analysis. Springer, 1999.

Digital Library

[36]

D. Orchard. Programming Contextual Computations. PhD thesis, Univ. of Cambridge, 2014.

[37]

D. Orchard and T. Petricek. Embedding effect systems in Haskell. In Haskell 2014, pp. 13–24. ACM, 2014.

Digital Library

[38]

D. Orchard, T. Petricek, and A. Mycroft. The semantic marriage of monads and effects. arXiv preprint 1401.5391, 2014.

[39]

T. Petricek. Context-Aware Programming Languages. Forthcoming PhD thesis, Univ. of Cambridge, 2016.

[40]

T. Petricek, D. Orchard, and A. Mycroft. Coeffects: unified static analysis of context-dependence. In ICALP 2013, Part II, v. 7966 of LNCS, pp. 385–397. Springer, 2013.

Digital Library

[41]

T. Petricek, D. Orchard, and A. Mycroft. Coeffects: a calculus of context-dependent computation. In ICFP ’14, pp. 123–135. ACM, 2014.

Digital Library

[42]

G. Plotkin and J. Power. Adequacy for algebraic effects. In FOSSACS 2001, v. 2030 of LNCS, pp. 1–24. Springer, 2001.

Digital Library

[43]

G. Plotkin and J. Power. Algebraic operations and generic effects. Appl. Categ. Struct., 11(1), pp. 69–94, 2003.

[44]

G. D. Plotkin and M. Pretnar. Handlers of algebraic effects. In ESOP 2009, v. 5502 of LNCS, pp. 80–94. Springer, 2009.

Digital Library

[45]

J. Power and H. Watanabe. Combining a monad and a comonad. Theor. Comput. Sci., 280(1–2), pp. 137–162, 2002.

Digital Library

[46]

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

Digital Library

[47]

R. Tate. The sequential semantics of producer effect systems. In POPL ’13, pp. 15–26. ACM, 2013.

Digital Library

[48]

K. Terui. Light affine lambda calculus and polytime strong normalization. In LICS ’01, pp. 209–220. IEEE, 2001.

[49]

T. Uustalu and V. Vene. Comonadic notions of computation. Electron. Notes in Theor. Comput. Sci., 203(5), pp. 263–284, 2008.

Digital Library

[50]

T. Uustalu and V. Vene. The essence of dataflow programming. In CEFP 2005, v. 4164 of LNCS, pp. 135–167. Springer, 2006.

Digital Library

[51]

P. Wadler. The essence of functional programming. In POPL ’92, pp. 1–14. ACM, 1992.

Digital Library

[52]

P. Wadler. The marriage of effects and monads. In ICFP ’98, pp. 63–74. ACM, 1998.

Digital Library

[53]

P. Wadler and P. Thiemann. The marriage of effects and monads. ACM Trans. on Comput. Logic, 4(1), pp. 1–32, 2003.

Digital Library

[54]

H. Xi and F. Pfenning. Dependent types in practical programming. In POPL ’99, pp. 214–227. ACM, 1999.

Digital Library

Cited By

Torczon CSuárez Acevedo EAgrawal SVelez-Ginorio JWeirich S(2024)Effects and Coeffects in Call-by-Push-ValueProceedings of the ACM on Programming Languages10.1145/36897508:OOPSLA2(1108-1134)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689750
Rajani VBarthe GGarg D(2024)A Modal Type Theory of Expected Cost in Higher-Order Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36897258:OOPSLA2(389-414)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689725
Giannini PDuso GDi Stefano L(2024)Coeffects for MiniJava: Cf-MjProceedings of the 26th ACM International Workshop on Formal Techniques for Java-like Programs10.1145/3678721.3686232(30-36)Online publication date: 20-Sep-2024
https://dl.acm.org/doi/10.1145/3678721.3686232
Show More Cited By

Index Terms

Combining effects and coeffects via grading
1. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

Coeffects: a calculus of context-dependent computation
ICFP '14: Proceedings of the 19th ACM SIGPLAN international conference on Functional programming

The notion of context in functional languages no longer refers just to variables in scope. Context can capture additional properties of variables (usage patterns in linear logics; caching requirements in dataflow languages) as well as additional ...
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 ...
No Go Theorems: Directed Containers That Do Not Distribute Over Distribution Monads
LICS '24: Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science

Monads and comonads are important constructions from category theory which find widespread application in computer science and other related disciplines. Distributive laws allow these constructions to interact compositionally. Such laws are not ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming

September 2016

501 pages

ISBN:9781450342193

DOI:10.1145/2951913

General Chairs:
Jacques Garrigue
Nagoya University, Japan
,
Gabriele Keller
University of New South Wales, Australia
,
Program Chair:
Eijiro Sumii
Tohoku University, Japan

ACM SIGPLAN Notices Volume 51, Issue 9
ICFP '16
September 2016
501 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/3022670
Editor:
Matthew Fluet
Issue’s Table of Contents

Copyright © 2016 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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 September 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Engineering and Physical Sciences Research Council
JSPS KAKENHI
Estonian Ministry of Education and Research
Estonian Science Foundation

Conference

ICFP'16

Sponsor:

SIGPLAN

ICFP'16: ACM SIGPLAN International Conference on Functional Programming

September 18 - 24, 2016

Nara, Japan

Acceptance Rates

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

42
Total Citations
View Citations
735
Total Downloads

Downloads (Last 12 months)118
Downloads (Last 6 weeks)18

Reflects downloads up to 06 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Torczon CSuárez Acevedo EAgrawal SVelez-Ginorio JWeirich S(2024)Effects and Coeffects in Call-by-Push-ValueProceedings of the ACM on Programming Languages10.1145/36897508:OOPSLA2(1108-1134)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689750
Rajani VBarthe GGarg D(2024)A Modal Type Theory of Expected Cost in Higher-Order Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/36897258:OOPSLA2(389-414)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689725
Giannini PDuso GDi Stefano L(2024)Coeffects for MiniJava: Cf-MjProceedings of the 26th ACM International Workshop on Formal Techniques for Java-like Programs10.1145/3678721.3686232(30-36)Online publication date: 20-Sep-2024
https://dl.acm.org/doi/10.1145/3678721.3686232
Lorenzen AWhite LDolan SEisenberg RLindley S(2024)Oxidizing OCaml with Modal Memory ManagementProceedings of the ACM on Programming Languages10.1145/36746428:ICFP(485-514)Online publication date: 15-Aug-2024
https://doi.org/10.1145/3674642
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
Marshall DOrchard D(2024)Functional Ownership through Fractional UniquenessProceedings of the ACM on Programming Languages10.1145/36498488:OOPSLA1(1040-1070)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649848
Marshall DOrchard D(2024)Non-Linear Communication via Graded Modal Session TypesInformation and Computation10.1016/j.ic.2024.105234(105234)Online publication date: Nov-2024
https://doi.org/10.1016/j.ic.2024.105234
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
Bianchini RDagnino FGiannini PZucca E(2023)Resource-Aware Soundness for Big-Step SemanticsProceedings of the ACM on Programming Languages10.1145/36228437:OOPSLA2(1281-1309)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622843
Gavazzo FDi Florio C(2023)Elements of Quantitative RewritingProceedings of the ACM on Programming Languages10.1145/35712567:POPL(1832-1863)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571256
Show More Cited By

View Options

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