Combining Effects and Coeffects via Grading
Accepted version
Peer-reviewed
Repository URI
Repository DOI
Change log
Authors
Abstract
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
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
Description
This is the author accepted manuscript. It is currently under an indefinite embargo pending publication by the Association for Computing Machinery.