Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Monadic Intersection Types, Relationally (Extended Version)

Francesco Gavazzo, Riccardo Treglia, Gabriele Vanoni

TL;DR

This work extends intersection types to effectful λ-calculi by introducing monadic intersections, parametric in the underlying monad $T$, and embedding both terms and types into the monadic framework. It leverages abstract relational reasoning and Barr extensions to establish soundness and completeness (including infinitary semantics) for finitary and infinitary observation of program behavior under a wide range of effects (e.g., output, cost, probabilistic nondeterminism, and their combinations). The approach delineates intrinsic limits via weakly cartesian monads and non-erasing operation constraints in the finitary setting, which can be overcome in infinitary semantics, yielding a modular, robust theory of observable behavior via typability. The results provide a foundational bridge between monadic operational semantics, algebraic effects, and intersection-type systems, with potential implications for model checking, complexity analysis, and reasoning about higher-order effectful programs.

Abstract

We extend intersection types to a computational $λ$-calculus with algebraic operations à la Plotkin and Power. We achieve this by considering monadic intersections, whereby computational effects appear not only in the operational semantics, but also in the type system. Since in the effectful setting termination is not anymore the only property of interest, we want to analyze the interactive behavior of typed programs with the environment. Indeed, our type system is able to characterize the natural notion of observation, both in the finite and in the infinitary setting, and for a wide class of effects, such as output, cost, pure and probabilistic nondeterminism, and combinations thereof. The main technical tool is a novel combination of syntactic techniques with abstract relational reasoning, which allows us to lift all the required notions, e.g. of typability and logical relation, to the monadic setting.

Monadic Intersection Types, Relationally (Extended Version)

TL;DR

This work extends intersection types to effectful λ-calculi by introducing monadic intersections, parametric in the underlying monad , and embedding both terms and types into the monadic framework. It leverages abstract relational reasoning and Barr extensions to establish soundness and completeness (including infinitary semantics) for finitary and infinitary observation of program behavior under a wide range of effects (e.g., output, cost, probabilistic nondeterminism, and their combinations). The approach delineates intrinsic limits via weakly cartesian monads and non-erasing operation constraints in the finitary setting, which can be overcome in infinitary semantics, yielding a modular, robust theory of observable behavior via typability. The results provide a foundational bridge between monadic operational semantics, algebraic effects, and intersection-type systems, with potential implications for model checking, complexity analysis, and reasoning about higher-order effectful programs.

Abstract

We extend intersection types to a computational -calculus with algebraic operations à la Plotkin and Power. We achieve this by considering monadic intersections, whereby computational effects appear not only in the operational semantics, but also in the type system. Since in the effectful setting termination is not anymore the only property of interest, we want to analyze the interactive behavior of typed programs with the environment. Indeed, our type system is able to characterize the natural notion of observation, both in the finite and in the infinitary setting, and for a wide class of effects, such as output, cost, pure and probabilistic nondeterminism, and combinations thereof. The main technical tool is a novel combination of syntactic techniques with abstract relational reasoning, which allows us to lift all the required notions, e.g. of typability and logical relation, to the monadic setting.
Paper Structure (2 sections, 2 equations, 1 figure)

This paper contains 2 sections, 2 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Intersection Types and the CbV $\lambda$-Calculus

Figures (1)

  • Figure 1: The intersection type system for closed call-by-value.

Theorems & Definitions (1)

  • remark thmcounterremark