Towards comonadic coeffect systems
Tomas Petricek
Computing Laboratory
University of Cambridge
Wednesday, 4 April 2012, 14:00 (note the unusual weekday)
Cybernetica Bldg (Akadeemia tee 21), room B101
Slides from the talk [pdf]
Abstract: Type and effect systems are an established mechanism for tracking actions performed by computations while evaluating. However, there is no established framework for tracking how computations depend on, or use the context in which they evaluate. With the recent rise of execution environments with varying capabilities (such as cloud, mobile phone and web browser), tracking context-dependence in a type system is becoming an important topic.
In this talk, I'll present preliminary work on coeffect systems. Coeffect systems give a unified way of tracking different kinds of context-dependence. Applications include tracking where an expression can be evaluated in a distributed computation, re-binding of values in mobile code, tracking of resource usage and static checking of secure information flows.
As shown by Wadler and Thiemann, effect systems can be modeled using monads with tags (or annotations) that form sets. Dually, coeffect systems can be modeled using tagged comonads. We study the structure of tags beyond sets and find that a more fine-grained structure is important for tracking of detailed information about the context.
(Joint work with Dominic Orchard and Alan Mycroft.)
Tarmo Uustalu
Last update 17.4.2012