TY - GEN

T1 - Intersection Types via Finite-Set declarations

AU - Kamareddine, Fairouz Dib

AU - Wells, Joe

PY - 2024/6/8

Y1 - 2024/6/8

N2 - 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 1,⋯,C n}:B which means that y is of type B and can only be one of C 1,⋯,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 Φ 1∩⋯∩Φ 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.

AB - 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 1,⋯,C n}:B which means that y is of type B and can only be one of C 1,⋯,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 Φ 1∩⋯∩Φ 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.

KW - Intersection Types

KW - Typability

KW - Strong Normalisation

UR - http://www.scopus.com/inward/record.url?scp=85196726091&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-62687-6_6

DO - 10.1007/978-3-031-62687-6_6

M3 - Conference contribution

SN - 9783031626869

T3 - Lecture Notes in Computer Science

SP - 80

EP - 92

BT - Logic, Language, Information, and Computation

A2 - Metcalfe, George

A2 - Studer, Thomas

A2 - de Queiroz, Ruy

PB - Springer

ER -