We extend intersection types to a computational $\lambda$-calculus with algebraic operations \`a 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.

翻译：我们将交集类型扩展至含代数运算的$\lambda$-演算（仿Plotkin与Power式），通过引入一元交集实现这一目标——计算效应不仅出现在操作语义中，更渗透至类型系统内部。在效应化场景下，终止性已不再是唯一关注属性，因此我们致力于分析带类型程序与环境的交互行为。本类型系统能刻画有限与无穷域中观测的自然内涵，适用于输出、开销、纯非确定性、概率非确定性及其组合等广泛效应类。核心技术手段是语法分析方法与抽象关系推论的创新融合，这使得可类型化、逻辑关系等所有必备概念能够被提升至一元化框架中。