research-article

Coeffects: a calculus of context-dependent computation

Authors:

Tomas Petricek,

Dominic Orchard,

Alan MycroftAuthors Info & Claims

ICFP '14: Proceedings of the 19th ACM SIGPLAN international conference on Functional programming

Pages 123 - 135

https://doi.org/10.1145/2628136.2628160

Published: 19 August 2014 Publication History

Abstract

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 resources or properties of the execution environment (rebindable resources; platform version in a cross-platform application). The recently introduced notion of coeffects captures the latter, whole-context properties, but it failed to capture fine-grained per-variable properties.

We remedy this by developing a generalized coeffect system with annotations indexed by a coeffect shape. By instantiating a concrete shape, our system captures previously studied flat (whole-context) coeffects, but also structural (per-variable) coeffects, making coeffect analyses more useful. We show that the structural system enjoys desirable syntactic properties and we give a categorical semantics using extended notions of indexed comonad.

The examples presented in this paper are based on analysis of established language features (liveness, linear logics, dataflow, dynamic scoping) and we argue that such context-aware properties will also be useful for future development of languages for increasingly heterogeneous and distributed platforms.

References

[1]

M. Abbott, T. Altenkirch, and N. Ghani. Containers: constructing strictly positive types. Theor. Comput. Sci., 342 (1): 3--27, 2005.

Digital Library

[2]

G. M. Bierman and V. C. de Paiva. On an intuitionistic modal logic. Studia Logica, 65 (3): 383--416, 2000.

[3]

A. Brunel, M. Gaboardi, D. Mazza, and S. Zdancewic. A core quantitative coeffect calculus. In Proceedings of ESOP, volume 8410 of Lecture Notes in Computer Science, pages 351--370. Springer, 2014.

[4]

C. Flanagan and S. Qadeer. A type and effect system for atomicity. In Prooceedings of PLDI, pages 338--349. ACM, 2003.

Digital Library

[5]

D. R. Ghica and A. I. Smith. Bounded linear types in a resource semiring. In Proceedings of ESOP, volume 8410 of Lecture Notes in Computer Science, pages 331--350. Springer, 2014.

[6]

D. K. Gifford and J. M. Lucassen. Integrating functional and imperative programming. In Proceedings of Conference on LISP and func. prog., LFP '86, 1986. ISBN 0-89791-200-4.

Digital Library

[7]

J.-Y. Girard, A. Scedrov, and P. J. Scott. Bounded linear logic: a modular approach to polynomial-time computability. Theoretical computer science, 97 (1): 1--66, 1992.

Digital Library

[8]

S. Katsumata. Parametric effect monads and semantics of effect systems. In Proceedings of POPL, pages 633--646. ACM, 2014.

Digital Library

[9]

J. Lewis, J. Launchbury, E. Meijer, and M. Shields. Implicit parameters: Dynamic scoping with static types. In Proceedings of POPL, page 118, 2000.

Digital Library

[10]

E. Moggi. Notions of computation and monads. Inf. Comput., 93 (1), 1991. ISSN 0890-5401.

Digital Library

[11]

A. Nanevski, F. Pfenning, and B. Pientka. Contextual modal type theory. ACM Trans. Comput. Logic, 9 (3): 23:1--23:49, June 2008.

Digital Library

[12]

P. O'Hearn. On bunched typing. J. Funct. Program., 13 (4): 747--796, July 2003. ISSN 0956-7968.

Digital Library

[13]

D. Orchard. Programming contextual computations (PhD dissertation). Technical Report UCAM-CL-TR-854, University of Cambridge, Computer Laboratory, 2014. URL http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-854.pdf.

[14]

T. Petricek. Context-aware programming languages (PhD thesis), 2014. Forthcoming.

[15]

T. Petricek, D. A. Orchard, and A. Mycroft. Coeffects: Unified static analysis of context-dependence. In F. V. Fomin, R. Freivalds, M. Z. Kwiatkowska, and D. Peleg, editors, ICALP (2), volume 7966 of Lecture Notes in Computer Science, pages 385--397. Springer, 2013.

Digital Library

[16]

F. Pfenning and R. Davies. A judgmental reconstruction of modal logic. Mathematical. Structures in Comp. Sci., 11 (4): 511--540, 2001.

Digital Library

[17]

P. Sewell, J. J. Leifer, K. Wansbrough, F. Z. Nardelli, M. Allen-Williams, P. Habouzit, and V. Vafeiadis. Acute: High-level programming language design for distributed computation. J. Funct. Program., 17 (4-5): 547--612, July 2007.

Digital Library

[18]

R. Tate. The sequential semantics of producer effect systems. In Proceedings of POPL 2013, pages 15--26, 2013.

Digital Library

[19]

T. Uustalu and V. Vene. Comonadic notions of computation. Electron. Notes Theor. Comput. Sci., 203 (5): 263--284, 2008. http://dx.doi.org/10.1016/j.entcs.2008.05.029.

Digital Library

[20]

W. W. Wadge and E. A. Ashcroft. LUCID, the dataflow programming language. Academic Press Professional, Inc., San Diego, CA, USA, 1985. ISBN 0-12-729650-6.

Digital Library

[21]

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

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
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://dl.acm.org/doi/10.1145/3674642
Show More Cited By

Index Terms

Coeffects: a calculus of context-dependent computation
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
2. Theory of computation
  1. Formal languages and automata theory

Recommendations

A relational theory of effects and coeffects

Graded modal types systems and coeffects are becoming a standard formalism to deal with context-dependent, usage-sensitive computations, especially when combined with computational effects. From a semantic perspective, effectful and coeffectful languages ...
Combining effects and coeffects via grading
ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming

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 ...
Coeffects: a calculus of context-dependent computation
ICFP '14

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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP '14: Proceedings of the 19th ACM SIGPLAN international conference on Functional programming

August 2014

390 pages

ISBN:9781450328739

DOI:10.1145/2628136

General Chair:
Johan Jeuring
Universiteit Utrecht, The Netherlands
,
Program Chair:
Manuel M.T. Chakravarty
University of New South Wales, Australia

ACM SIGPLAN Notices Volume 49, Issue 9
ICFP '14
September 2014
361 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2692915
Editors:
Mark W. Bailey
Hamilton College, Clinton, NY
,
Rajeev Balasubramonian
University of Utah
,
Al Davis
University of Utah
,
Sarita Adve
University of Illinois at Urbana-Champ
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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 19 August 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

CHESS

Conference

ICFP'14

Sponsor:

SIGPLAN

ICFP'14: ACM SIGPLAN International Conference on Functional Programming

September 1 - 6, 2014

Gothenburg, Sweden

Acceptance Rates

ICFP '14 Paper Acceptance Rate 28 of 85 submissions, 33%;

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

69
Total Citations
View Citations
623
Total Downloads

Downloads (Last 12 months)57
Downloads (Last 6 weeks)13

Reflects downloads up to 16 Nov 2024

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
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://dl.acm.org/doi/10.1145/3674642
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
Lee EZhao YLhoták OYou JSatheeskumar KBrachthäuser J(2024)Qualifying System F<:: Some Terms and Conditions May ApplyProceedings of the ACM on Programming Languages10.1145/36498328:OOPSLA1(583-612)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649832
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
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
Boruch-Gruszecki AOdersky MLee ELhoták OBrachthäuser J(2023)Capturing TypesACM Transactions on Programming Languages and Systems10.1145/361800345:4(1-52)Online publication date: 20-Nov-2023
https://dl.acm.org/doi/10.1145/3618003
Abel ADanielsson NEriksson O(2023)A Graded Modal Dependent Type Theory with a Universe and Erasure, FormalizedProceedings of the ACM on Programming Languages10.1145/36078627:ICFP(920-954)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607862
Bianchini RAncona DAudrito G(2023)Monitoring for Resource-AwarenessProceedings of the 6th International Workshop on Verification and Monitoring at Runtime Execution10.1145/3605159.3605856(13-16)Online publication date: 18-Jul-2023
https://dl.acm.org/doi/10.1145/3605159.3605856
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