Coeffects: The Essence of Context Dependence

Tomas Petricek, Dominic Orchard and Alan Mycroft

Submitted to ESOP 2013

Monadic typing provides a unified way of tracking effects of computations, but there is no unified mechanism for tracking how computations rely on the environment in which they are executed.

Since modern software runs in rich, distributed settings where each component executes on a different device, this is becoming an important problem. We need to track where a computation can run, what resources it accesses and how it uses other specific capabilities of the environment.

We consider three examples of context-dependence analysis: liveness analysis, tracking the use of rebindable resources, and calculating caching requirements for data-flow programs. Informed by these cases, we present a unified calculus for tracking context dependence in functional languages together with a categorical semantics based on indexed comonads.

Our work forms a foundation for constructing languages and type systems that track context dependence. We show how to use the model in a number of simple, yet intriguing applications. Finally, we also sketch a more detailed and powerful system.