Intersection Types via Finite-Set Declarations

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 \(F_\omega \) , and that there is an untyped \(\lambda \) -term \(\dot{U}\) that is SN but is not typable in \(F_\omega \) or the \(\lambda \) -cube. Hence, neither system can type all the SN terms it expresses. In this paper, we present the \(\textsf {f}\) -cube, an extension of the \(\lambda \) -cube with finite-set declarations (FSDs) like \(y \mathord {\overline{\in }}\{C_1,\cdots , C_n\} :B\) which means that y is of type B and can only be one of \(C_1, \cdots , C_n\) . The novelty of our FSDs is that they allow to represent intersection types as \(\varPi \) -types. We show how to translate and type the term \(\dot{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 type \(\varPhi _1\cap \cdots \cap \varPhi _k\) using k independent subderivations. As such, our approach is useful for language implementers who want the power of intersection types without the pain of the intersection-introduction rule.