一句话：将交集类型提升到带代数效应的计算演算，并用单子与前序语义刻画程序观察行为。
本文将交集类型扩展到带 Plotkin-Power 代数操作的 computational λ-演算。核心思想是单子交集：计算效应不仅出现在操作语义中，也出现在类型系统里。由于在效应场景中终止不再是唯一关注性质，作者用类型系统刻画程序与环境交互的自然观察，覆盖有限与无限情形。随后引入子类型，并用前序上的单子（而非集合上的单子）容纳更丰富的效应，特别可建模非确定性。技术上是句法技术与抽象关系推理的新结合，可将可类型化、逻辑关系等概念提升到单子场景。
We extend intersection types to a computational \(\lambda\) -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 can characterize the natural notion of observation, both in the finitary and in the infinitary setting. In a second phase, we extend our system with subtyping to incorporate a richer class of effects via monads on preorders instead of sets allowing us to model in particular non-determinism. The main technical tool is a novel combination of syntactic techniques with abstract relational reasoning, which allows us to lift all the required notions, for example, of typability and logical relation, to the monadic setting.
@article{GalalGTV25,
title = {Monadic Intersection Types, Relationally, and Ordered},
author = {Zeinab Galal and Francesco Gavazzo and Riccardo Treglia and Gabriele Vanoni},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {47},
number = {4},
year = {2025},
doi = {10.1145/3777483}
}