2014 | OriginalPaper | Buchkapitel
A Core Quantitative Coeffect Calculus
verfasst von : Aloïs Brunel, Marco Gaboardi, Damiano Mazza, Steve Zdancewic
Erschienen in: Programming Languages and Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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 work, we present a language
$\ell \mathcal{R}$
PCF
inspired by a generalized interpretation of the exponential modality. In
$\ell \mathcal{R}$
PCF
the exponential modality carries a label—an element of a semiring
$\mathcal{R}$
—that provides additional information on how a program uses its context. This additional structure is used to express comonadic type analysis.