Intersection Types via Finite-Set declarations

The λ-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 λ-cube only types Strongly Normalising (SN) terms but not all of them. It is well known that even the most powerful system of the λ-cube can only type the same pure untyped λ-terms that are typable by the higher-order polymorphic implicitly typed λ-calculus F _ω, and that there is an untyped λ-term U˙ that is SN but is not typable in F _ω or the λ-cube. Hence, neither system can type all the SN terms it expresses. In this paper, we present the f-cube, an extension of the λ-cube with finite-set declarations (FSDs) like y∈¯{C ₁,⋯,C _n}:B which means that y is of type B and can only be one of C ₁,⋯,C _n. The novelty of our FSDs is that they allow to represent intersection types as Π-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 λ-term M has an intersection type Φ ₁∩⋯∩Φ _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.