University of Cambridge > > Computer Laboratory Programming Research Group Seminar > Coeffect Systems and Typing (Preliminary report)

Coeffect Systems and Typing (Preliminary report)

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Dominic Orchard.

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.

This talk is part of the Computer Laboratory Programming Research Group Seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2022, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity