Coeffects: typing context-dependent computations using comonads

Tomas Petricek, Dominic Orchard and Alan Mycroft

Submitted to FLOPS 2012

The literature describes various type systems which track how computations depend on some notion of context. A context-dependent computation might only execute in certain environments or in a sandbox that provides sufficient privileges. We refer to such context-dependent properties of computations as coeffects, dualising the concept of effects.

We show how to track different forms of coeffect in a uniform way using a type system based on comonads and describe how the system follows from a comonadic semantics of the lambda calculus. Applications include tracking dynamically-scoped implicit parameters and checking execution environments that specify where a computation may execute in a distributed programming setting.

While there is only one form of monadic effect systems, there are by contrast multiple variants of comonadic type systems for coeffects, one of which is equivalent to monadic effect systems. This is due to a different notion of context capture for functions in the comonadic semantics, and is discussed at the end of the paper.