Abstract

Effect systems are a class of static program analyses tracking information about side effects in a program, such as read/write effects and exceptions. The traditional approach to describing effect systems is to augment the typing rules of a language with effect judgements.

In semantics and functional programming, monads are popularly used as a means of structuring side effecting computations. Both monads and effect systems can be combined into one uniform system, where monadic types are “tagged” with effect information (see The Marriage of Monads and Effects by Wadler and Thiemann). The standard operations of a monad, providing compositional semantics, are augmented so that effect information is composed, matching the rules of an effect system.

This work considers the dual situation, of “coeffect” systems structured by comonads and comonadic-typing.

Numerous type systems have been proposed to track how computations depend on the “context” of execution. A context-dependent computation may only execute in certain environments or in a sandbox that provides sufficient privileges. We term such context-dependence coeffects.

In this talk, we show how to track different kinds of context-dependence in a uniform way using a type system based on comonads.

This is a talk on preliminary results and ideas, and is by no means polished.