Skip to main content

Combining Effects and Coeffects via Grading

Gaboardi, Marco, Katsumata, Shin-ya, Orchard, Dominic A., Breuvart, Flavien, Uustalu, Tarmo (2016) Combining Effects and Coeffects via Grading. ACM SIGPLAN Notices, 51 (9). pp. 476-489. ISSN 0362-1340. E-ISSN 1558-1160. (doi:10.1145/2951913.2951939) (KAR id:57480)

PDF Publisher pdf
Language: English
Download (369kB) Preview
[thumbnail of bieffects.pdf]
Preview
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL
http://dx.doi.org/10.1145/2951913.2951939

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.

Item Type: Article
DOI/Identification number: 10.1145/2951913.2951939
Uncontrolled keywords: effects, coeffects, monads, comonads, distributive laws, grading, types, categorical semantics
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 9 Formal systems, logics
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Dominic Orchard
Date Deposited: 28 Sep 2016 09:08 UTC
Last Modified: 16 Feb 2021 13:37 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/57480 (The current URI for this page, for reference purposes)
Orchard, Dominic A.: https://orcid.org/0000-0002-7058-7842
  • Depositors only (login required):

Downloads

Downloads per month over past year