单子交集类型：关系视角与有序性考量

《ACM Transactions on Programming Languages and Systems》：Monadic Intersection Types, Relationally and Ordered

我们扩展了带有代数操作符的λ-演算的交类型系统，通过单子交类型将计算效应融入类型系统，并分析其与环境的交互行为。在第二阶段引入子类型，利用预订单monad扩展效应模型以支持非确定性。技术核心在于结合语法分析和抽象关系推理。

　　

摘要

我们将交集类型扩展到一种基于计算\(\lambda\)-演算的系统中，并引入了类似Plotkin和Power方法中的代数运算。我们通过引入单子交集（monadic intersections）来实现这一点——这样一来，计算效应不仅体现在操作语义中，也体现在类型系统中。由于在具有计算效应的系统中，终止性不再是唯一需要关注的属性，我们希望分析带类型程序与环境的交互行为。实际上，我们的类型系统能够描述观察的自然概念，无论是在有限环境中还是在无限环境中。在第二阶段，我们通过引入子类型（subtyping）来扩展系统，利用预序（preorders）而非集合上的单子（monads）来表示更丰富的效应类型，从而能够特别模拟非确定性行为。主要的技术手段是将语法技术与抽象关系推理相结合，这种方法使我们能够将所有必要的概念（如类型化能力和逻辑关系）提升到单子计算环境中。