Enriching an Effect Calculus with Linear Types

Abstract We define an enriched effect calculus by extending a type theory for computational effects with primitives from linear logic. The new calculus provides a formalism for expressing linear aspects of computational effects; for example, the linear usage of imperative features such as state and/or continuations. Our main syntactic result is the conservativity of the enriched effect calculus over a basic effect calculus without linear primitives (closely related to Moggi’s computational metalanguage, Filinski’s effect PCF and Levy’s call-by-push-value ). The proof of this syntactic theorem makes essential use of a category-theoretic semantics, whose study forms the second half of the paper. Our semantic results include soundness, completeness, the initiality of a syntactic model, and an embedding theorem: every model of the basic effect calculus fully embeds in a model of the enriched calculus. The latter means that our enriched effect calculus is applicable to arbitrary computational effects, answering in the positive a question of Benton and Wadler (LICS 1996).

Authors

• Jeff Egger
• Rasmus Ejlers Møgelberg
• Alex Simpson

Keywords

No keywords are indexed for this paper.