Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

An effectful object calculus

Francesco Dagnino, Paola Giannini, Elena Zucca

TL;DR

The paper addresses integrating effects into object-oriented languages using a monadic semantics approach to ensure soundness. It extends a Featherweight Java-style core with magic methods for effect raising and catch-style handlers, and a type-and-effect system that tracks call-effects of shape $T.m[barT]!E$. Soundness is established by a novel technique that reduces expressions to monadic computations and proves progress and subject reduction on the monadic one-step reduction. The approach is demonstrated through examples (e.g., exceptions and nondeterminism) and supports simple form of effect polymorphism and scalable handling strategies.

Abstract

We show how to smoothly incorporate in the object-oriented paradigm constructs to raise, compose, and handle effects in an arbitrary monad. The underlying pure calculus is meant to be a representative of the last generation of OO languages, and the effectful extension is manageable enough for ordinary programmers; notably, constructs to raise effects are just special methods. We equip the calculus with an expressive type-and-effect system, which, again by relying on standard features such as inheritance and generic types, allows a simple form of effect polymorphism. The soundness of the type-and-effect system is expressed and proved by a recently introduced technique, where the semantics is formalized by a one-step reduction relation from language expressions into monadic ones, so that it is enough to prove progress and subject reduction properties on this relation.

An effectful object calculus

TL;DR

The paper addresses integrating effects into object-oriented languages using a monadic semantics approach to ensure soundness. It extends a Featherweight Java-style core with magic methods for effect raising and catch-style handlers, and a type-and-effect system that tracks call-effects of shape . Soundness is established by a novel technique that reduces expressions to monadic computations and proves progress and subject reduction on the monadic one-step reduction. The approach is demonstrated through examples (e.g., exceptions and nondeterminism) and supports simple form of effect polymorphism and scalable handling strategies.

Abstract

We show how to smoothly incorporate in the object-oriented paradigm constructs to raise, compose, and handle effects in an arbitrary monad. The underlying pure calculus is meant to be a representative of the last generation of OO languages, and the effectful extension is manageable enough for ordinary programmers; notably, constructs to raise effects are just special methods. We equip the calculus with an expressive type-and-effect system, which, again by relying on standard features such as inheritance and generic types, allows a simple form of effect polymorphism. The soundness of the type-and-effect system is expressed and proved by a recently introduced technique, where the semantics is formalized by a one-step reduction relation from language expressions into monadic ones, so that it is enough to prove progress and subject reduction properties on this relation.

Paper Structure

This paper contains 3 sections, 1 theorem, 4 equations, 6 figures.

Table of Contents

  1. Introduction
  2. Language
  3. Monadic Operational Semantics

Key Result

Proposition 3

If $\mathit{e}\to \textsc{e}_1$ and $\mathit{e}\to\textsc{e}_2$ then $\textsc{e}_1 = \textsc{e}_2$.

Figures (6)

  • Figure 1: Effect-free syntax and types
  • Figure 2: Fine-grain syntax for the effectful language
  • Figure 3: Pure reduction
  • Figure 4: Method look-up and matching
  • Figure 5: Monadic (one-step) reduction
  • ...and 1 more figures

Theorems & Definitions (6)

  • Remark 1
  • Example 2
  • Proposition 3: Determinism
  • Example 4: Exceptions
  • Example 5: Failure
  • Example 6: Non-determinism