Coeffects A calculus of context-dependent computation
Tomas Petricek, Dominic Orchard and Alan Mycroft
In Proceedings of ICFP 2014
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.
Watch the talk
Thanks to the ICFP workshop organizers, the video from my talk, Coeffects: A Calculus of Context-Dependent Computation is on YouTube!
Paper and more information
If you want to cite the paper, you can use the following BibTeX information, or get full details from the paper paper page on ACM.
1: 2: 3: 4: 5: 6: 7:
Published: Friday, 29 August 2014, 12:00 AM
Author: Tomas Petricek
Typos: Send me pull request!