Abstract

Linear logic is well known for its resource-awareness, which has inspired the design of several resource management mechanisms in programming language design. Its resource-awareness arises from the distinction between linear, single-use data and non-linear, reusable data. The latter is marked by the so-called exponential modality, which, from the categorical viewpoint, is a (monoidal) comonad.

Monadic notions of computation are well-established mechanisms used to express effects in pure functional languages. Less well-established is the notion of comonadic computation. However, recent works have shown the usefulness of comonads to structure context dependent computations. In this talk, I will present a language inspired by a generalized interpretation of the exponential modality. In this language the exponential modality carries a label—an element of a semiring—that provides additional information on how a program uses its context. This additional structure is used to express comonadic type analysis

I will conclude my talk by discussing an ongoing work about a quantitative calculus combining comonadic coeffects with monadic effects. I will show how a dependency between coeffects and effects corresponds to a distributivity law of (labeled) monads over (labeled) comonads.