We show how (well-established) type systems based on non-idempotent intersection types can be extended to characterize termination properties of functional programming languages with pattern matching features. To model such programming languages, we use a (weak and closed) $\lambda$-calculus integrating a pattern matching mechanism on algebraic data types (ADTs). Remarkably, we also show that this language not only encodes Plotkin's CBV and CBN $\lambda$-calculus as well as other subsuming frameworks, such as the bang-calculus, but can also be used to interpret the semantics of effectful languages with exceptions. After a thorough study of the untyped language, we introduce a type system based on intersection types, and we show through purely logical methods that the set of terminating terms of the language corresponds exactly to that of well-typed terms. Moreover, by considering non-idempotent intersection types, this characterization turns out to be quantitative, i.e. the size of the type derivation of a term t gives an upper bound for the number of evaluation steps from t to its normal form.

翻译：我们展示了如何将基于非幂等交集类型的（成熟）类型系统扩展至以刻画具有模式匹配特性的函数式编程语言的终止性质。为建模此类编程语言，我们采用一个（弱且封闭的）λ-演算，该演算集成了代数数据类型（ADT）上的模式匹配机制。值得注意的是，我们还证明该语言不仅能编码Plotkin的按值调用（CBV）与按名调用（CBN）λ-演算以及其他包含性框架（如bang演算），还可用于解释具有异常的效果语言的语义。在对无类型语言进行深入研究后，我们引入了一个基于交集类型的类型系统，并通过纯逻辑方法证明了该语言的终止项集合恰好对应于良类型项集合。此外，通过采用非幂等交集类型，该刻画结果具有定量特性，即项t的类型推导规模为从t到其正规形的求值步数提供了上界。