Coeffects: a calculus of context-dependent computation

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.
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.
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.
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.
8. S. Katsumata. Parametric effect monads and semantics of effect systems. In Proceedings of POPL, pages 633--646. ACM, 2014.
9. J. Lewis, J. Launchbury, E. Meijer, and M. Shields. Implicit parameters: Dynamic scoping with static types. In Proceedings of POPL, page 118, 2000.
10. E. Moggi. Notions of computation and monads. Inf. Comput., 93 (1), 1991. ISSN 0890-5401.
11. A. Nanevski, F. Pfenning, and B. Pientka. Contextual modal type theory. ACM Trans. Comput. Logic, 9 (3): 23:1--23:49, June 2008.
12. P. O'Hearn. On bunched typing. J. Funct. Program., 13 (4): 747--796, July 2003. ISSN 0956-7968.
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.
16. F. Pfenning and R. Davies. A judgmental reconstruction of modal logic. Mathematical. Structures in Comp. Sci., 11 (4): 511--540, 2001.
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.
18. R. Tate. The sequential semantics of producer effect systems. In Proceedings of POPL 2013, pages 15--26, 2013.
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.
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.
21. P. Wadler and P. Thiemann. The marriage of effects and monads. ACM Trans. Comput. Logic, 4: 1--32, January 2003.

Index Terms

• Software and its engineering

  • Software notations and tools

    • Formal language definitions

• Theory of computation

  • Formal languages and automata theory