Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Monadic type-and-effect soundness

Francesco Dagnino, Paola Giannini, Elena Zucca

TL;DR

This work develops an abstract framework for monadic type-and-effect soundness by combining monadic small-step operational semantics with a type-and-effect system whose effect types are interpreted via predicate liftings. The core idea is to prove soundness by establishing monadic progress and monadic subject reduction, then deriving finitary and infinitary soundness results from these properties. The framework is instantiated to a lambda-calculus with generic effects, ΛΣ, where effect types capture complex behaviors such as exceptions, nondeterminism, and output constraints, and is further extended to support effect handlers. A key contribution is the parametric proof technique: soundness proofs are modular with respect to the interpretation of effect types and the underlying monad, enabling a range of concrete instances and policy models. The approach thus provides a modular, extensible method for reasoning about a broad class of effectful languages with formal guarantees on their observable behavior.

Abstract

We introduce the abstract notions of "monadic operational semantics", a small-step semantics where computational effects are modularly modeled by a monad, and "type-and-effect system", including "effect types" whose interpretation lifts well-typedness to its monadic version. In this meta-theory, as usually done in the non-monadic case, we can express progress and subject reduction properties and provide a proof, given once and for all, that they imply soundness. The approach is illustrated on a lambda calculus with generic effects. We equip the calculus with an expressive type-and-effect system, and provide proofs of progress and subject reduction which are parametric on the interpretation of effect types. In this way, we obtain as instances many significant examples, such as checking exceptions, preventing/limiting non-determinism, constraining order/fairness of outputs on different locations. We also provide an extension with constructs to raise and handle computational effects, which can be instantiated to model different policies.

Monadic type-and-effect soundness

TL;DR

This work develops an abstract framework for monadic type-and-effect soundness by combining monadic small-step operational semantics with a type-and-effect system whose effect types are interpreted via predicate liftings. The core idea is to prove soundness by establishing monadic progress and monadic subject reduction, then deriving finitary and infinitary soundness results from these properties. The framework is instantiated to a lambda-calculus with generic effects, ΛΣ, where effect types capture complex behaviors such as exceptions, nondeterminism, and output constraints, and is further extended to support effect handlers. A key contribution is the parametric proof technique: soundness proofs are modular with respect to the interpretation of effect types and the underlying monad, enabling a range of concrete instances and policy models. The approach thus provides a modular, extensible method for reasoning about a broad class of effectful languages with formal guarantees on their observable behavior.

Abstract

We introduce the abstract notions of "monadic operational semantics", a small-step semantics where computational effects are modularly modeled by a monad, and "type-and-effect system", including "effect types" whose interpretation lifts well-typedness to its monadic version. In this meta-theory, as usually done in the non-monadic case, we can express progress and subject reduction properties and provide a proof, given once and for all, that they imply soundness. The approach is illustrated on a lambda calculus with generic effects. We equip the calculus with an expressive type-and-effect system, and provide proofs of progress and subject reduction which are parametric on the interpretation of effect types. In this way, we obtain as instances many significant examples, such as checking exceptions, preventing/limiting non-determinism, constraining order/fairness of outputs on different locations. We also provide an extension with constructs to raise and handle computational effects, which can be instantiated to model different policies.

Paper Structure

This paper contains 6 sections, 18 theorems, 3 equations, 6 figures.

Table of Contents

  1. Introduction
  2. Preliminaries on monads
  3. Monadic operational semantics
  4. Example: a lambda calculus with generic effects
  5. Monadic type-and-effect soundness
  6. Example of soundness proof

Key Result

Proposition 8

$c\mathrel{ \stackunder[0pt]{ \xrightarrow{\hbox{$$}} }{ \mathsf{step}\, }}^\star \textsc{c}$ if and only if $\mathsf{step}^{n}(c)=\textsc{c}$ for some $n\in\mathbb{N}$.

Figures (6)

  • Figure 1: Monadic (one-step) reduction on configurations
  • Figure 2: $\Lambda_{\Sigma}$: fine-grain syntax
  • Figure 3: Pure reduction
  • Figure 4: Monadic (one-step) reduction
  • Figure 5: Types and contexts
  • ...and 1 more figures

Theorems & Definitions (46)

  • Example 1: Exceptions
  • Example 2: Classical Non-Determinism
  • Example 3: Probabilistic Non-Determinism
  • Example 4: Output/Writer
  • Example 5: Global State
  • Example 6: Ordered Trees
  • Definition 7
  • Proposition 8
  • Definition 9
  • Proposition 10
  • ...and 36 more