The lambda-cube is a famous pure type system (PTS) cube of eight powerful explicit type systems that include the simple, polymorphic and dependent type theories. The lambda-cube only types Strongly Normalising (SN) terms but not all of them. It is well known that even the most powerful system of the lambda-cube can only type the same pure untyped lambda-terms that are typable by the higher-order polymorphic implicitly typed lambda-calculus Fomega, and that there is an untyped {\lambda}-term U' that is SN but is not typable in Fomega or the lambda-cube. Hence, neither system can type all the SN terms it expresses. In this paper, we present the f-cube, an extension of the lambda-cube with finite-set declarations (FSDs) like y\in{C1,...,Cn} : B which means that y is of type B and can only be one of C1,..., Cn. The novelty of our FSDs is that they allow to represent intersection types as Pi-types. We show how to translate and type the term U' in the f-cube using an encoding of intersection types based on FSDs. Notably, our translation works without needing anything like the usual troublesome intersection-introduction rule that proves a pure untyped lambda-term M has an intersection of k types using k independent sub-derivations. As such, our approach is useful for language implementers who want the power of intersection types without the pain of the intersection-introduction rule.

翻译：λ-立方体是一个著名的纯类型系统（PTS）立方体，包含八种强大的显式类型系统，涵盖简单类型、多态类型和依赖类型理论。λ-立方体仅能对强规范化（SN）项进行类型化，但无法涵盖所有SN项。众所周知，即使λ-立方体中最强大的系统，也只能为高阶多态隐式类型化λ-演算Fomega所能类型化的相同纯无类型λ-项进行类型化，且存在一个无类型λ-项U'，它是SN项，但无法在Fomega或λ-立方体中被类型化。因此，这两个系统均无法对其表达的所有SN项进行类型化。本文提出了f-立方体，它是扩展了有限集声明（FSD）的λ-立方体，例如y∈{C1,...,Cn}:B表示y属于类型B，且只能取C1,...,Cn中的值。我们FSD的创新之处在于允许将交集类型表示为Π类型。我们展示了如何利用基于FSD的交集类型编码，在f-立方体中翻译并类型化项U'。值得注意的是，我们的翻译无需使用通常棘手的交集引入规则（该规则通过k个独立的子推导证明纯无类型λ-项M具有k种类型的交集）。因此，我们的方法对希望获得交集类型强大能力却避免交集引入规则复杂性的语言实现者具有实用价值。