Intersection Types via Finite-Set Declarations

TL;DR

This paper introduces the f-cube, an extension of the lambda-cube with finite-set declarations that enable representing intersection types as Pi-types, allowing typing of certain untypable terms without complex intersection rules.

Contribution

The paper presents the f-cube, a novel extension of the lambda-cube, that encodes intersection types via finite-set declarations, simplifying intersection type typing.

Findings

Successfully encodes intersection types as Pi-types using FSDs

Enables typing of the untypable term U' without intersection-introduction rules

Provides a practical approach for language implementers to incorporate intersection types

Abstract

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.