Disjoint Polymorphism with Intersection and Union Types

HKU PL Group Papers - Index

Metadata

• Title: Disjoint Polymorphism with Intersection and Union Types
• Venue: FTfJP’24
• Area: Intersection and union duality
• Source URL: https://i.cs.hku.hk/~bruno/papers/FTFJP24.pdf
• Downloaded PDF: Disjoint-Polymorphism-with-Intersection-and-Union-Types.pdf
• Extracted assets: _assets/Disjoint-Polymorphism-with-Intersection-and-Union-Types/
• Pages: 7
• Embedded image count reported by PyMuPDF: 2

Why this note exists

This note is part of the HKU PL Group literature knowledge base for work on iso-recursive subtyping, intersection types, union types, disjointness, merge operators, and compositional programming. It is designed for later Coding Agent / Proof Agent use during proof search, design brainstorming, and comparison against prior systems.

Extraction quality note

This is the fast pass generated with pymupdf4llm, not the heavier marker-pdf pass. The original PDF is linked above and kept in _pdfs/. Figures/images detected by PyMuPDF are saved under _assets/. Some mathematical notation may still require checking against the PDF, especially inference rules with complex layouts.

Technical landmarks detected automatically

These are line references into the converted Markdown below. They are meant as a quick navigation layer for rules, lemmas, theorems, proofs, algorithms, examples, and counterexamples.

• line 2:
• line 6:
• line 9: Disjoint Polymorphism with Intersection and Union Types
• line 11: Baber Rehman[∗]
• line 13: Bruno C. d. S. Oliveira
• line 24: |||A<:|||B|||||||||||(Subtyping)|||||
• line 32: |||Γ ⊢e|||:A||||||||||||(Typing)||||
• line 47: Abstract
• line 51: CCS Concepts
• line 53: • Theory of computation → Type theory.
• line 55: Keywords
• line 57: Intersection types, Union types, Disjointness, Polymorphism
• line 59: ACM Reference Format:
• line 63: Figure 1: Syntax and subtyping for 휆푢 with intersection types.
• line 65: 1 Background
• line 67: This section briefly introduces 휆푢 [14] and the limitations in disjointness algorithm for polymorphic 휆푢 . Essence of 휆푢 lies in disjoint switches meaning that branches with overlapping types are not
• line 69: allowed in a type-based switch construct ensuring deterministic semantics. For example, 휆푢 rejects the following program[1] :
• line 81: 1.1 휆푢 Calculus
• line 83: Syntax and subtyping. Figure 1 presents the syntax and subtyping for 휆푢 [14]. Types include top, bottom, integer, function, union, intersection and null types. Expressions consist of variable, integer,
• line 87: > 1Note that we use | in code and ∨ in metatheory for union types. Similarly, we use & in code and ∧ in metatheory for intersection types.
• line 101: Definition 1.1 (∧-Disjointness). A ∗ B � � 퐶[◦] , 퐶[◦] <: A and 퐶[◦] <: B.
• line 106:
• line 109: 1.2 휆푢 with Disjoint Polymorphism
• line 114:
• line 120:
• line 131: 2 Revised Disjointness Algorithm
• line 135: 2.1 Union Ordinary and Union Splittable Types
• line 141: Lemma 2.1 (Exclusivity of union ordinary and union splittable types). ∀ A, A is either union ordinary or union splittable and never both.
• line 143: 2.2 Algorithmic Disjointness
• line 145: The algorithmic disjointness based on union ordinary and union splittable types is shown in Figure 3. Rules ad-bot, ad-intarr,
• line 153: Disjoint Polymorphism with Intersection and Union Types
• line 155: (Operational Semantics)
• line 159: ||e −→e′|||||||(Operational Semantics)||
• line 171: Figure 2: Operational semantics for 휆푢 .
• line 175: ||A⊚|||||||||||||||||||(Union|||Ordinary Types)|||||||
• line 180: ||B⊳A⊲C|||||||||||||||||||(Union Splittable Types)||||||||||
• line 186: ||A∗푎푥B|||||||||||||||||||(Disjointness||||||||Axioms)||
• line 196: ||A∗푎B|||||||||||||||||||||||(Disjointness)||||||
• line 217: Figure 3: Disjointness based on splittable types for 휆푢 .
• line 219: ad-intnull, and ad-nullarr are trivial disjointness axioms. The novelty of the disjointness algorithm lies in the disjointness rules for intersection and union types.
• line 225: - (Int ∨ Bool) ∗푎 String : Int ∨ Bool is disjoint to String by
• line 227: - rule ad-orll.
• line 235: Soundness and completeness of disjointness. We prove that the novel disjointness algorithm is sound and complete with respect to the disjointness specifications (definition 1.1).
• line 237: Lemma 2.2 (Soundness of disjointness algorithm). ∀ A B, A ∗푎 B → A ∗ B.
• line 239: Lemma 2.3 (Completeness of disjointness algorithm). ∀ A B, A ∗ B → A ∗푎 B.
• line 254: Figure 4: Extended Syntax and union ordinary types for polymorphic 휆푢 .
• line 256: 2.3 Metatheory
• line 260: Lemma 2.4 (Subtyping Reflexivity). A <: A
• line 262: Lemma 2.5 (Subtyping Transitivity). If A <: B and B <: C then A <: C
• line 264: Theorem 2.6 (Type Preservation). If Γ ⊢ e : A and e −→ e[′] then Γ ⊢ e[′] : A.
• line 266: Theorem 2.7 (Progress). If Γ ⊢ e : A then either e is a value; or e can take a step to e[′] .
• line 268: Theorem 2.8 (Determinism). If Γ ⊢ e : A and e −→ e1 and e −→ e2 then e1 = e2.
• line 270: 3 Polymorphic Disjointness
• line 278: 3.1 Disjointness
• line 284: ||Δ;Γ|⊢A∗푎푥B||||||||||||(Disjointness||Axioms)|
• line 296: ||Δ;Γ|⊢A∗B|||||||||||||(Disjointness)||
• line 309: Figure 5: Extended disjointness rules with union splittable types for polymorphic 휆푢 .
• line 314:
• line 319: Disjointness for nominal types. The disjointness rule for nominal types (rule adpp-nom) is interesting. It states that two nominal
• line 327: Disjoint Polymorphism with Intersection and Union Types
• line 332:
• line 339: For example, in a context Δ = Person <: ⊤, Student <: Person, GradStudent <: Student, Robot <: ⊤, OptimumPrime <: Robot:
• line 341: - Person is disjoint to Robot as per rule adpp-nom, because the set intersection of the subtypes of Person and Robot is empty i.e Person, Student, GradStudent ∩ Robot, OptimumPrime = .
• line 343: - Whereas, Person is not disjoint to GradStudent, because the set intersection of the subtypes of Person and GradStudent is not empty i.e Person, Student, GradStudent ∩ GradStudent = GradStudent.
• line 347: Lemma 3.1 (Contravariance of disjointness). If Δ; Γ ⊢ A ∗ B and Δ; Γ ⊢ C <: A then Δ; Γ ⊢ C ∗ B.
• line 352:
• line 356:
• line 363: Figure 6: Extended subtyping, typing, and operational semantics for polymorphic 휆푢 .
• line 365: 3.2 Metatheory
• line 369: > 3Alpuim et al. [1] proved covariance for supertypes in the context of intersection types. We call this property contravariance due to subtypes in our context of union types.
• line 383: Figure 6. Similarly, changes for operational semantics are shown in Figure 6. Importantly, we no longer use syntactic category of ground types and the bound of a type variable can be any other type.
• line 385: Type safety and determinism. Polymorphic 휆푢 with updated disjointness preserves standard properties of subtyping, type-safety and determinism.
• line 387: Lemma 3.2 (Subtyping Reflexivity). Δ; Γ ⊢ A <: A
• line 389: Lemma 3.3 (Subtyping Transitivity). If Δ; Γ ⊢ A <: B and Δ; Γ ⊢ B <: C then Δ; Γ ⊢ A <: C
• line 391: Theorem 3.4 (Type Preservation). If Δ; Γ ⊢ e : A and Δ; Γ ⊢ e −→ e[′] then Δ; Γ ⊢ e[′] : A.
• line 393: Theorem 3.5 (Progress). If Δ; · ⊢ e : A then either e is a value; or e can take a step to e[′] .
• line 395: Theorem 3.6 (Determinism). If Δ; Γ ⊢ e : A and Δ; Γ ⊢ e −→ e1 and Δ; Γ ⊢ e −→ e2 then e1 = e2.
• line 399: Lemma 3.7 (Typing Substitution). If Δ; Γ, 훼 ∗ A1 ⊢ e : B and Δ; Γ ⊢ A2 ∗ A1 then Δ; Γ [ 훼 � A2] ⊢ e[ 훼 � A2] : B[ 훼 � A2]
• line 401: Lemma 3.8 (Typing narrowing). If Δ; Γ, 훼 ∗ A1 ⊢ e : B and Δ; Γ ⊢ A1 <: A2 then Δ; Γ, 훼 ∗ A2 ⊢ e : B
• line 403: Lemma 3.9 (Typing weakening). If Δ; Γ1, Γ2 ⊢ e : B and ok Γ1, Γ3, Γ2 then Δ; Γ1, Γ3, Γ2 ⊢ e : B

Full converted paper text

Disjoint Polymorphism with Intersection and Union Types

Baber Rehman[∗]

Bruno C. d. S. Oliveira

The University of Hong Kong Hong Kong SAR, China bruno@cs.hku.hk

Huawei Technologies Hong Kong SAR, China brehman@connect.hku.hk

					A,B,C �				⊤	⊥	Int	A→B	A∨B
								e �	x	i	휆x.e	e1e2	null
					퐴◦,	v � Γ � 퐵◦,퐶◦ �				switche {(푥:A) →e1,(푦: i	휆x.e	null ·	Γ,x :A Int	Null	A→B
		A<:			B											(Subtyping)
				s-top A<:⊤				s-int Int<:Int		s-bot ⊥<:A						s-null Null<:Null
			s-arrow						s-ora							s-orb
			B1 <:A1					A2 <:B2	A<:C B <:C							A<:		B
			A1		→A2			<:B1 →B2	A∨B <:C							A<:B∨C
	s-orc A<:C A<:B∨C							s-anda A<:B A<:C A<:B∧C			s-andb A<:C A∧B <:C					s-andc B <:C A∧B <:C
		Γ ⊢e			:A												(Typing)
					typ-int				typ-null						typ-var
															x :A ∈Γ
					Γ		⊢i:Int		Γ ⊢null:Null							Γ ⊢x :A
					typ-app Γ ⊢e1 :A→B				Γ ⊢e2 :A		typ-sub Γ ⊢e :A					A<:B
								Γ ⊢e1e2 :	B				Γ		⊢e :B
							typ-abs Γ,x :A⊢e :B Γ ⊢휆x.e :A→B				typ-and Γ ⊢e :A Γ ⊢e :		A		Γ ⊢e :B ∧B
								typ-switch Γ ⊢e :A∨B Γ, Γ,y :B⊢e2 :C			x :A⊢e1 :C A∗B
								Γ ⊢switche {(푥:A) →e1,(푦:B) →e2} :C

Abstract

Intersection and union types are advance programming features and are able to encode various classical programming constructs. The significance of intersection and union types is visible by the fact that these types are available in many modern programming languages including Scala, TypeScript and Ceylon. (Un-tagged) Union types are normally eliminated using a type-based switch construct. The branches of the switch construct may overlap thus resulting in an ambiguous semantics. Recently, a disjointness based approach so called 휆푢 has been proposed to deal with ambiguity in (untagged) union elimination. When studied with intersection types and parametric polymorphism, 휆푢 poses an un-intuitive ground type restriction on type variable bounds. This restriction reduces the expressiveness of the calculus. In this paper, we propose a novel disjointness algorithm based on union splittable types. The novel disjointness algorithm does not require ground type restriction on type variable bounds. Therefore, the resulting calculus is more expressive. We prove soundness and completeness of our disjointness algorithm (without parametric polymorphism) w.r.t disjointness specifications for monomorphic 휆푢 . All the metatheory of this paper has been formalized in Coq theorem prover.

CCS Concepts

• Theory of computation → Type theory.

Keywords

Intersection types, Union types, Disjointness, Polymorphism

ACM Reference Format:

Baber Rehman and Bruno C. d. S. Oliveira. 2024. Disjoint Polymorphism with Intersection and Union Types. In Proceedings of the 26th ACM International Workshop on Formal Techniques for Java-like Programs (FTfJP ’24), September 20, 2024, Vienna, Austria. ACM, New York, NY, USA, 7 pages. https://doi. org/10.1145/3678721.3686230

Figure 1: Syntax and subtyping for 휆푢 with intersection types.

1 Background

This section briefly introduces 휆푢 [14] and the limitations in disjointness algorithm for polymorphic 휆푢 . Essence of 휆푢 lies in disjoint switches meaning that branches with overlapping types are not

allowed in a type-based switch construct ensuring deterministic semantics. For example, 휆푢 rejects the following program[1] :

BoolisInteger(x:Int|Bool)=switch(x)

∗Also with The University of Hong Kong.

(x:Int) → true (y:Int|Bool) → false

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org. FTfJP ’24, September 20, 2024, Vienna, Austria

1.1 휆푢 Calculus

Syntax and subtyping. Figure 1 presents the syntax and subtyping for 휆푢 [14]. Types include top, bottom, integer, function, union, intersection and null types. Expressions consist of variable, integer,

© 2024 Copyright held by the owner/author(s). Publication rights licensed to ACM. ACM ISBN 979-8-4007-1111-4/24/09 https://doi.org/10.1145/3678721.3686230

1Note that we use | in code and ∨ in metatheory for union types. Similarly, we use & in code and ∧ in metatheory for intersection types.

23

--- end of page.page_number=1 ---

FTfJP ’24, September 20, 2024, Vienna, Austria

Baber Rehman and Bruno C. d. S. Oliveira

lambda, application, null and a type-based switch expression. Integer, null, and lambda expressions are also values. The context Γ is standard and stores variable bindings. Subtyping is also standard for a calculus with intersection and union types.

Disjointness. Interesting constituent of 휆푢 is the type-based disjointness (A ∗ B) in a switch expression. Disjointness restricts branches with overlapping types. Therefore, the expression under scrutinee falls in a maximum of one branch. Disjointness specifications are shown in Definition 1.1. Essentially, two types are disjoint if they do not share an ordinary common subtype. Ordinary types are shown in Figure 1. Integer, function, and null types are ordinary types. Interested readers may refer to [14] for details about algorithmic disjointness. Nevertheless, disjointness algorithm is sound and complete w.r.t Definition 1.1.

Definition 1.1 (∧-Disjointness). A ∗ B � � 퐶[◦] , 퐶[◦] <: A and 퐶[◦] <: B.

Type system and operational semantics. The type system for 휆푢 is shown at the bottom of Figure 1. Rule typ-switch is an interesting rule. This rule type-checks a switch expression for eliminating union types. The last premise A ∗ B employs disjointness. Rule typswitch type-checks a switch expression only if e has a union type A ∨ B, first branch has type A, second branch has type B, and types A and B are disjoint. Operational semantics for 휆푢 is shown in Figure 2. ⌊v⌋ is the approximate type relation and shown next:

1.2 휆푢 with Disjoint Polymorphism

Rehman et al. [14] study 휆푢 with a variant of parametric polymorphism called disjoint polymorphism [1]. Polymorphic 휆푢 [14] poses a ground type restriction on type variable bounds[2] . Ground types constitute of all the types except type variables. This means that a type variable cannot be declared as a bound to another type variable. While this is a common approach in many polymorphic calculi [5], this approach limits the expressiveness of the calculus. For example, two type variables cannot be declared disjoint in the presence of ground type restriction. This restrains us from writing the following program:

Since the bound of type variable X is another type variable Y, therefore, this program will not type-check with ground type restriction on type variable bound. Any type except the type variable can be a bound of a type variable. The following program will type-check:

2Note that bound in this context corresponds to the disjointness constraint on a type variable. The disjointness constraint restricts the possible instantiation of a type variable. For example, [Γ, 훼 ∗ Int], where 훼 can be instantiated with all the types that are disjoint with Int such as Null.

Notice that the bound of type variable X in the program above is a base type i.e. Int.

Limitation of disjoint polymorphism in 휆푢 . Rehman et al. [14] study a disjointness algorithm based on Least Ordinary Subtypes (LOS) that accounts for intersection and union types. LOS is a function that computes a set of least ordinary subtypes of the input type. The disjointness algorithm simply states that two types are disjoint if set intersection of LOS of two types is an empty set. When extended with parametric polymorphism, the LOS based disjointness algorithm requires an un-intuitive ground type restriction on type variable bounds.

Our contributions. In this paper we study a variant of 휆푢 with disjoint polymorphism [1] and without a ground type restriction on type variable bounds. This makes our calculus expressive than the one discussed in [14]. For example, the program isFirstMatch type-checks in our calculus. All the metatheory has been formalized in Coq theorem prover and is available at: https://github.com/ baberrehman/FTfJP2024-artifact.

2 Revised Disjointness Algorithm

We develop a novel disjointness algorithm for intersection and union types by exploiting union ordinary and union splittable types [9]. We study two variants of 휆푢 with newly developed disjointness, one without polymorphism and another with polymorphism. The first calculus establishes a connection with the calculi without polymorphism. We show that the disjointness in Section 2 is sound and complete with respect to the disjointness specifications (Definition 1.1). The second calculus revisits disjoint polymorphism in Section 3 and proposes a revised disjointness algorithm without ground types. Syntax and subtyping for 휆푢 with intersection types is shown in Figure 1.

2.1 Union Ordinary and Union Splittable Types

Union ordinary and union splittable types [9] play an essential role in the formulation of the novel disjointness algorithm. These types are shown at the top in Figure 3. ⊤, Int, A → B and Null are union ordinary types as shown by rules uo-top, uo-int, uoarrow, and uo-unit respectively. An intersection type is union ordinary only if both of its parts are union ordinary types as shown in rule uo-and. For example, Int ∧⊤ is a union ordinary type. Whereas, (Int ∨ A → B) ∧⊤ is not union ordinary because left part of the intersection is not union ordinary i.e Int ∨ A → B.

Union types are never union ordinary types. On the contrary, union types are union splittable types by rule usp-or. Intersection types are union splittable if either of the component of the intersection is union splittable by rules usp-andl and usp-andr. A type is either union ordinary or union splittable as stated in lemma 2.1.

Lemma 2.1 (Exclusivity of union ordinary and union splittable types). ∀ A, A is either union ordinary or union splittable and never both.

2.2 Algorithmic Disjointness

The algorithmic disjointness based on union ordinary and union splittable types is shown in Figure 3. Rules ad-bot, ad-intarr,

24

--- end of page.page_number=2 ---

FTfJP ’24, September 20, 2024, Vienna, Austria

Disjoint Polymorphism with Intersection and Union Types

(Operational Semantics)

	e −→e′							(Operational Semantics)
step-appl			step-appr			step-switch
	e1 −→e′ 1 e −→e′				step-beta		e −→e′
e1e2 −→e′ 1 e2 v e −→v e′					(휆x.e)v −→e[x �v]	switche {(푥:A) →e1,(푦:B) →e2} −→switche′ {(푥:A) →e1,(푦:B) →e2}
			step-switchl				step-switchr
					⌊v⌋<:A		⌊v⌋<:B
			switchv {(푥:A)	→e1,(푦:B) →e2} −→e1[x		�v]	switchv {(푥:A) →e1,(푦:B) →e2}	−→e2[y �v]

Figure 2: Operational semantics for 휆푢 .

	A⊚																			(Union			Ordinary Types)
																									uo-and
uo-top									uo-int			uo-arrow						uo-unit							A⊚				B⊚
⊤⊚									Int⊚			(A→B)⊚						Null⊚								(A		∧B)⊚
	B⊳A⊲C																			(Union Splittable Types)
										usp-andl									usp-andr
usp-or											A1⊳A⊲A2										B1⊳B⊲B2
A⊳A∨B⊲B										A1∧B⊳A∧B⊲A2∧B									A∧B1			⊳A∧B⊲A∧B2
	A∗푎푥B																			(Disjointness								Axioms)
ad-bot										ad-intarr					ad-intnull							ad-nullarr
⊥∗푎푥A										Int∗푎푥A→B					Int∗푎푥Null							Null			∗푎푥A				→B
														ad-sym
														A∗푎푥B
														B∗푎푥A
	A∗푎B																							(Disjointness)
				ad-orll																	ad-axiom
					A1⊳A⊲A2						A1∗푎B				A2	∗푎B					A∗푎푥B
											A∗푎B											A	∗푎B
			ad-orrr																	ad-andll
			B1⊳B⊲B2								A∗푎B1			A	∗푎B2					A1	∗푎B						B⊚
											A∗푎B									(A1		∧A2)				∗푎B
	ad-andlss											ad-andrr								ad-andrss
		A2		∗푎B						B⊚		A∗푎B1				A⊚				A∗푎B2								A⊚
		(A1∧A2)								∗푎B		A		∗푎(B1∧B2)						A∗푎(B1						∧B2)
										ad-emptyl							ad-emptyr
										A∗푎B								B∗푎C
										(A∧B) ∗푎C							A∗푎(B∧C)

Figure 3: Disjointness based on splittable types for 휆푢 .

ad-intnull, and ad-nullarr are trivial disjointness axioms. The novelty of the disjointness algorithm lies in the disjointness rules for intersection and union types.

Rule ad-orll states that if A is union splittable into A1 and A2 then A is disjoint to B only if A1 and A2 are disjoint to B. Rule adorrr is symmetric to rule ad-orll. Rules ad-andll and ad-andlss state that an intersection type A1 ∧ A2 is disjoint to another type B when B is union ordinary and either A1 or A2 is disjoint to B. Rules ad-andrr and ad-andrss are symmetric to rules ad-andll

and ad-andlss. Rules ad-emptyl and ad-emptyr state that an intersection of two disjoint types is disjoint with any other type. The intersection of two disjoint types forms an empty type or a bottom-like type, which is disjoint with any other type. The following example illustrates our novel disjointness algorithm:

• (Int ∨ Bool) ∗푎 String : Int ∨ Bool is disjoint to String by

• rule ad-orll.

Essence of Union Ordinary Types. Note that the union ordinary premise in rules ad-andll, ad-andlss, ad-andrr, and ad-andrss is optional. This premise only makes the rules less overlapping. It allows the application of rules ad-andll, ad-andlss, ad-andrr, and ad-andrss only if one type is an intersection type and the other type is a union ordinary type. When the other type is not union ordinary type, the disjointness algorithm falls to the union rules. The algorithm then splits the other type until it becomes union ordinary and then applies either of the rules ad-andll, ad-andlss, ad-andrr, and ad-andrss.

Essence of Union Splittable Types. A naive disjointness algorithm without union splittable types may potentially be incomplete. For example, (Int∨Bool∨String)∧(Bool∨String∨Char) and (String∨ Char∨Int)∧(Char∨Int∨Bool) are clearly disjoint types but a naive algorithm that works on the principal of strict smaller reductions may fails to classify them as disjoint types without union splittable types. It does not matter whether we break the left intersection or the right intersection first, we cannot make these two types disjoint. Importantly the two types as a whole are disjoint. But if we drop any component from either of the intersection, the smaller types are no longer disjoint.

Union splittable types come to the rescue in such cases and solve the incompleteness problem of the disjointness algorithm. Note that union ordinary types are optional because union ordinary types just make the rules less overlapping. The disjointness algorithm stays sound and complete without union ordinary types. But union splittable types are essential. The disjointness algorithm will not be complete without union splittable types.

Soundness and completeness of disjointness. We prove that the novel disjointness algorithm is sound and complete with respect to the disjointness specifications (definition 1.1).

Lemma 2.2 (Soundness of disjointness algorithm). ∀ A B, A ∗푎 B → A ∗ B.

Lemma 2.3 (Completeness of disjointness algorithm). ∀ A B, A ∗ B → A ∗푎 B.

25

--- end of page.page_number=3 ---

FTfJP ’24, September 20, 2024, Vienna, Austria

Baber Rehman and Bruno C. d. S. Oliveira

|A⊚|A,B,C
�
… | P | 훼| ∀(훼∗A).B
e
�
… | new P | e A | Λ(훼∗A).e
v
�
… | new P | Λ(훼∗A).e
Γ
�
· | Γ,x :A | Γ, 훼∗A
Δ
�
· | Δ,P<:A
퐴◦, 퐵◦,퐶◦
�
… | ∀(훼∗A).B | P
(Union Ordinary Types)
uo-tvar
훼⊚
uo-all
∀(훼∗A).B⊚
uo-nom
P⊚| |---|---|

Figure 4: Extended Syntax and union ordinary types for polymorphic 휆푢 .

2.3 Metatheory

Typing and operational semantics. Subtyping, typing and operational semantics essentially stay the same and are shown in Figure 2. This calculus preserves the standard properties of subtyping, typesafety and determinism as shown below:

Lemma 2.4 (Subtyping Reflexivity). A <: A

Lemma 2.5 (Subtyping Transitivity). If A <: B and B <: C then A <: C

Theorem 2.6 (Type Preservation). If Γ ⊢ e : A and e −→ e[′] then Γ ⊢ e[′] : A.

Theorem 2.7 (Progress). If Γ ⊢ e : A then either e is a value; or e can take a step to e[′] .

Theorem 2.8 (Determinism). If Γ ⊢ e : A and e −→ e1 and e −→ e2 then e1 = e2.

3 Polymorphic Disjointness

Section 2 presents a novel disjointness algorithm by exploiting union ordinary and union splittable types. We show that the disjointness algorithm is sound and complete with respect to the disjointness specifications. In this section we extend the calculus from Section 2 with disjoint polymorphism. Importantly, we show that the ground type restriction on type variable bounds is no longer needed with the novel disjointness algorithm.

Syntax, union ordinary, and union splittable types. The syntax for polymorphic 휆푢 is shown at the top in Figure 4. Types are extended with the nominal types P, type variables 훼, and disjoint quantifiers ∀(훼 ∗ A).B. The syntactic category of expressions now include a new expression (new P) to construct instances of type P. It also includes type applications e A and type abstractions Λ(훼 ∗ A).e. Expressions new P and Λ(훼 ∗ A).e are also values. Typing context Γ also has entries for type variables Γ, 훼 ∗ A. A new context Δ keeps a list and subtyping bounds of nominal types.

Union ordinary types are shown in Figure 4. Union ordinary types are extended with type variables (rule uo-tvar), disjoint quantifiers (rule uo-all) and nominal types (rule uo-nom). Union splittable types stay the same as in Section 2.

3.1 Disjointness

Note that we use ∗ for algorithmic disjointness in this section for simplicity. Disjointness specifications for disjoint polymorphism is an open problem. The disjointness algorithm with polymorphism is shown in Figure 5. In addition to the disjointness rules from Figure 3, we add axioms for universal types and the nominal types. Universal types are disjoint to all the base types and so are the nominal types. Type variables are disjoint to all the subtypes of its bound as shown in rules adpp-varr and adpp-varl. For example in a context [Γ, 훼 ∗⊤], 훼 is essentially disjoint to all the types because all the types are subtype of ⊤. In another context [Γ, 훼 ∗ Int ∨ Bool], 훼 is disjoint with all the subtypes of Int ∨ Bool including Int and Bool but is not disjoint to String.

	Δ;Γ	⊢A∗푎푥B												(Disjointness		Axioms)
		adpa-intall										adpa-nullall
		Δ;Γ ⊢Int∗푎푥∀(훼∗A).B										Δ;Γ ⊢Null∗푎푥∀(훼∗A).B
		adpa-arrall											adpa-pint
		Δ;Γ ⊢C				→D∗푎푥∀(훼∗A).B							Δ;Γ ⊢P∗푎푥Int
adpa-parr									adpa-pnull				adpa-pall
Δ;Γ		⊢P∗푎푥A→B							Δ;Γ ⊢P∗푎푥Null				Δ;Γ ⊢P∗푎푥∀(훼∗A).B
	Δ;Γ	⊢A∗B													(Disjointness)
	adpp-varr											adpp-varl
	훼∗A ∈Γ					Δ;Γ ⊢B <:A						훼∗A ∈Γ		Δ;Γ	⊢B <:A
		Δ;		Γ ⊢B			∗훼						Δ;Γ ⊢훼∗B
							adpp-nom
								P1 ::Δ(P1) ∩P2 ::Δ(P2) = {}
									Δ;Γ ⊢P1			∗P2

Figure 5: Extended disjointness rules with union splittable types for polymorphic 휆푢 .

Note that we scrap the optional union ordinary premise from rules ad-andll, ad-andlss, ad-andrr, and ad-andrss. This simplifies the metatheory with type variables. We also drop rules ademptyl and ad-emptyr from disjointness algorithm in Figure 5. Dropping rules ad-emptyl and ad-emptyr restricts writing some programs but all the practical programs still type-check. Generally, it does not allow writing empty intersection types in branches. For example, the following program will no longer type-check because of the empty type in the first branch i.e Int ∧ Bool.

Since we cannot construct a value of type Int∧Bool in contemporary system, the first branch in the above program has no practical significance. Therefore not allowing such empty intersections does not affect the programs in practice.

Disjointness for nominal types. The disjointness rule for nominal types (rule adpp-nom) is interesting. It states that two nominal

26

--- end of page.page_number=4 ---

FTfJP ’24, September 20, 2024, Vienna, Austria

Disjoint Polymorphism with Intersection and Union Types

types P1 and P2 are disjoint if the intersection of their subtypes is an empty set. Nominal subtypes (Δ(A)) is a function that finds the subtypes of type A in Δ and returns a list. Note that nominal subtypes is a transitive closure and shown next:

----- Start of picture text -----
Nominal Subtypes Δ(A)
·(A) = {}
{P} ∪ Δ [′] (A) if P <: A ∈ Δ
(Δ [′] , P <: B)(A) =
 Δ [′] (A) otherwise
Is Nominal Subtype A <: B ∈ Δ
A <: B ∈· = FALSE
TRUE if 퐴 푃푎푛푑퐵 퐶
A <: B ∈(Δ [′] , P <: C) = C <: B ∈ Δ [′] if 퐴 == 푃푎푛푑퐵 ≠ 퐶
 A <: B ∈ Δ [′] otherwise

----- End of picture text -----

For example, in a context Δ = {Person <: ⊤, Student <: Person, GradStudent <: Student, Robot <: ⊤, OptimumPrime <: Robot}:

• Person is disjoint to Robot as per rule adpp-nom, because the set intersection of the subtypes of Person and Robot is empty i.e {Person, Student, GradStudent} ∩ {Robot, OptimumPrime} = {}.

• Whereas, Person is not disjoint to GradStudent, because the set intersection of the subtypes of Person and GradStudent is not empty i.e {Person, Student, GradStudent} ∩ {GradStudent} = {GradStudent}.

Contravariance of disjointness. Contravariance[3] of disjointness (lemma 3.1) states that if two types A and B are disjoint, then the subtypes of A are also disjoint with B. In general subtypes of disjoint types are disjoint as well. For example if A → B is disjoint to Int ∨ Null, then A → B is disjoint to both Int and Null among other subtypes of Int ∨ Null. Similarly if a type A is disjoint to ⊤, then A is disjoint with all the types.

Lemma 3.1 (Contravariance of disjointness). If Δ; Γ ⊢ A ∗ B and Δ; Γ ⊢ C <: A then Δ; Γ ⊢ C ∗ B.

Expressiveness of disjointness. Our novel disjointness algorithm allows writing the programs that are not allowed in the polymorphic 휆푢 proposed in [14] due to the ground type restriction. In particular, our calculus allows writing programs by declaring type variables as bounds of other type variables:

----- Start of picture text -----
표푘 Δ (Well-formed Nominal Context)
okp-sub
okp-empty 표푘 Δ Δ; Γ ⊢ P2 P1 ∉ 푑표푚 Δ
표푘 · 표푘 Δ, P1 <: P2
Δ; Γ ⊢ A (Well-formed Types)
wftp-int wftp-tvar wftp-top wftp-bot
훼 ∗ A ∈ Γ
Δ; Γ ⊢ Int Δ; Γ ⊢ 훼 Δ; Γ ⊢⊤ Δ; Γ ⊢⊥
wftp-arrow wftp-all
Δ; Γ ⊢ A Δ; Γ ⊢ B Δ; Γ ⊢ A Δ; Γ, 훼 ∗ A ⊢ B
Δ; Γ ⊢ A → B Δ; Γ ⊢∀(훼 ∗ A).B
wftp-or wftp-and
Δ; Γ ⊢ A Δ; Γ ⊢ B Δ; Γ ⊢ A Δ; Γ ⊢ B
Δ; Γ ⊢ A ∨ B Δ; Γ ⊢ A ∧ B
wftp-prim wftp-null
P ∈ 푑표푚 Δ
Δ; Γ ⊢ P Δ; Γ ⊢ Null
Δ; Γ ⊢ A <: B (Subtyping)
polys-alldisj
polys-tvar Δ; Γ ⊢ A1 <: A2
표푘 Δ Δ; Γ ⊢ 훼 Δ; Γ, 훼 ∗ A2 ⊢ B1 <: B2
Δ; Γ ⊢ 훼 <: 훼 Δ; Γ ⊢∀(훼 ∗ A1 ).B1 <: ∀(훼 ∗ A2 ).B2
polys-prefl polys-pin
표푘 Δ Δ; Γ ⊢ P 표푘 Δ Δ; Γ ⊢ P1 P2 ∈ Δ(P1 )
Δ; Γ ⊢ P <: P Δ; Γ ⊢ P2 <: P1
Δ; Γ ⊢ e : A (Typing)
ptyp-prim ptyp-tapdisj
표푘 Δ Δ; Γ ⊢ P Δ; Γ ⊢ e : ∀(훼 ∗ A).C Δ; Γ ⊢ B ∗ A
Δ; Γ ⊢ new P : P Δ; Γ ⊢ e B : C [ 훼 � B]
ptyp-tabsdisj
Δ; Γ, 훼 ∗ A ⊢ e : B
Δ; Γ ⊢ Λ(훼 ∗ A).e : ∀(훼 ∗ A).B
Δ; Γ ⊢ e −→ e [′] (Operational Semantics)
polystep-tappl
Δ; Γ ⊢ e −→ e [′] polystep-tappdisj
Δ; Γ ⊢ e B −→ e [′] B Δ; Γ ⊢(Λ(훼 ∗ A).e) B −→ e[ 훼 � B]
Approximate Type ⌊v ⌋Δ;Γ
⌊Λ(훼 ∗ A).e⌋Δ;Γ = ∀(훼 ∗⊥).⊥
⌊new P⌋Δ;Γ = P
----- End of picture text -----

Figure 6: Extended subtyping, typing, and operational semantics for polymorphic 휆푢 .

3.2 Metatheory

Subtyping, typing, and operational semantics. Subtyping, typing and operational semantics are altered to lift the ground type restriction on type variable bounds and are shown in Figure 6. Note that subtyping, typing, and operational semantics extend all the rules

3Alpuim et al. [1] proved covariance for supertypes in the context of intersection types. We call this property contravariance due to subtypes in our context of union types.

from Section 2. We also show the well-formedness relation at the top in Figure 6.

Modifications in metatheory. The subtyping changes are reflected by rule polys-alldisj in Figure 6. Note that first premise does not have ground type restriction. A1 and A2 can be any types. Typing changes are shown in rules ptyp-tapdisj and ptyp-tabsdisj in

27

--- end of page.page_number=5 ---

FTfJP ’24, September 20, 2024, Vienna, Austria

Baber Rehman and Bruno C. d. S. Oliveira

Figure 6. Similarly, changes for operational semantics are shown in Figure 6. Importantly, we no longer use syntactic category of ground types and the bound of a type variable can be any other type.

Type safety and determinism. Polymorphic 휆푢 with updated disjointness preserves standard properties of subtyping, type-safety and determinism.

Lemma 3.2 (Subtyping Reflexivity). Δ; Γ ⊢ A <: A

Lemma 3.3 (Subtyping Transitivity). If Δ; Γ ⊢ A <: B and Δ; Γ ⊢ B <: C then Δ; Γ ⊢ A <: C

Theorem 3.4 (Type Preservation). If Δ; Γ ⊢ e : A and Δ; Γ ⊢ e −→ e[′] then Δ; Γ ⊢ e[′] : A.

Theorem 3.5 (Progress). If Δ; · ⊢ e : A then either e is a value; or e can take a step to e[′] .

Theorem 3.6 (Determinism). If Δ; Γ ⊢ e : A and Δ; Γ ⊢ e −→ e1 and Δ; Γ ⊢ e −→ e2 then e1 = e2.

Substitution, narrowing, and weakening lemmas. Type-safety proofs need type substitution (lemma 3.7), type narrowing (lemma 3.8), and type weakening (lemma 3.9) lemmas. Narrowing lemma essentially explains the relation between disjointness and subtyping. It states that it is safe to replace the bound of a type variable with a supertype of its existing bound. Weakening lemma states that if a relation is valid in a smaller context, then it stays valid in an enlarged context given that the enlarged context is well-formed. Note that we do not show corresponding subtyping and disjointness lemmas, such as subtyping substitution and disjointness substitution due to space constraints. All of these lemmas are available in the Coq formalization of this paper.

Lemma 3.7 (Typing Substitution). If Δ; Γ, 훼 ∗ A1 ⊢ e : B and Δ; Γ ⊢ A2 ∗ A1 then Δ; Γ [ 훼 � A2] ⊢ e[ 훼 � A2] : B[ 훼 � A2]

Lemma 3.8 (Typing narrowing). If Δ; Γ, 훼 ∗ A1 ⊢ e : B and Δ; Γ ⊢ A1 <: A2 then Δ; Γ, 훼 ∗ A2 ⊢ e : B

Lemma 3.9 (Typing weakening). If Δ; Γ1, Γ2 ⊢ e : B and ok Γ1, Γ3, Γ2 then Δ; Γ1, Γ3, Γ2 ⊢ e : B

More auxiliary lemmas. We discuss a few more interesting auxiliary lemmas in this paragraph. Lemma 3.10, lemma 3.11 and lemma 3.12 are essential in proving the metatheory. Lemma 3.10 states that if a union ordinary type A[⊚] is a subtype of a union splittable type B (B1 ⊳ B ⊲ B2), then A is subtype of either B1 or B2. Lemma 3.11 states disjointness symmetry. Finally, lemma 3.12 states that if A and B are disjoint types, then this is not the case that a value v checks against both A and B.

Lemma 3.10 (Subtyping inversion of union ordinary and union splittable types). If Δ; Γ ⊢ A <: B and B1 ⊳ B ⊲ B2 and A[⊚] then Δ; Γ ⊢ A <: B1 ∨ Δ; Γ ⊢ A <: B2.

Lemma 3.11 (Disjointness symmetry). If Δ; Γ ⊢ A ∗ B then Δ; Γ ⊢ B ∗ A.

Lemma 3.12 (Exclusivity of Disjoint Types). If Δ; Γ ⊢ A ∗ B then � v such that both Δ; Γ ⊢ v : A and Δ; Γ ⊢ v : B holds.

4 Related Work

Intersection and union types have extensively been studied in the literature. We discuss the work closest to ours in this section.

Intersection types. Coppo et al. [4] and Pottinger [13] initially studied intersection types in programming languages to assign meaningful types to terms. Compagnoni and Pierce [3] studied multiple interface inheritance by exploiting intersection types. Pierce [12] studied a calculus with intersection types, union types and polymorphism. Intersection types have also been studied in the context of refinement types [7]. Refinement types increase the expressiveness of types but not the terms. The merge operator, an introduction form for the intersection types, was first introduced in Forsythe programming language by Reynolds [15]. Dunfield [6] studied merge operator in a calculus with union types.

Disjoint intersection types. Oliveira et al. [11] studied disjoint intersection types to overcome the non-deterministic behaviour of the merge operator. Alpuim et al. [1] studied disjoint intersection types with disjoint polymorphism. Recently, Huang and Oliveira [8] proposed a direct operational semantics for the merge operator. However, this line of work does not count for union types and a type-based switch construct.

Union types. Union types were introduced in programming languages by MacQueen et al. [10]. They proposed an implicit elimination rule for union types. Barbanera et al. [2] solved the type preservation problem of implicit union elimination rule by parallel reduction. Single-branch case construct for union types is proposed by Pierce [12]. Rioux et al. [16] studied merge operator together with intersection and union types. However, their merge operator is restricted to functions. Recently, Rehman et al. [14] studied disjoint switches as a deterministic elimination form for union types. The order of branches of a switch construct does not matter in their calculus due to the disjointness constraint. However, their disjointness algorithm poses an ad-hoc restriction on type variable bounds when studied with disjoint polymorphism.

5 Conclusion and Future Work

We present a type-safe and deterministic calculus with intersection types, union types and disjoint polymorphism. The determinism of the calculus is ensured by employing a notion of disjointness. Disjointness restricts overlapping branches of a switch construct. Thus scrutinee can fall in a maximum of one branch. We present a novel disjointness algorithm which naturally extends for disjoint polymorphism without ad-hoc restrictions on type variable bounds. All the metatheory has been formalized in Coq theorem prover.

There are a few future explorations of the proposed calculus. The first future direction is to study the proposed calculus with the merge operator. Disjointness for union types and the typebased switch expression is essentially dual to the disjointness for intersection types with the merge operator. Another interesting and practical future direction is to study disjoint switches with gradual typing. The challenge of studying disjointness with gradual typing is because of the unknown type.

Acknowledgments

We thank the reviewers for the insightful comments. We also thank Xuejing Huang for technical discussions.

28

--- end of page.page_number=6 ---

FTfJP ’24, September 20, 2024, Vienna, Austria

Disjoint Polymorphism with Intersection and Union Types

References

• [1] João Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi. 2017. Disjoint Polymorphism. In European Symposium on Programming (ESOP).

• [2] Franco Barbanera, Mariangiola Dezaniciancaglini, and Ugo Deliguoro. 1995. Intersection and union types: syntax and semantics. Information and Computation 119, 2 (1995), 202–230.

• [3] Adriana B Compagnoni and Benjamin C Pierce. 1996. Higher-order intersection types and multiple inheritance. Mathematical Structures in Computer Science 6, 5 (1996), 469–501.

• [4] Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. 1981. Functional characters of solvable terms. Mathematical Logic Quarterly 27, 2-6 (1981), 45–58.

• [5] Stephen Dolan and Alan Mycroft. 2017. Polymorphism, subtyping, and type inference in MLsub. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. 60–72.

• [6] Joshua Dunfield. 2014. Elaborating intersection and union types. Journal of Functional Programming 24, 2-3 (2014), 133–165.

• [7] Tim Freeman and Frank Pfenning. 1991. Refinement types for ML. In Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation. 268–277.

• [8] Xuejing Huang and Bruno C. d. S. Oliveira. 2020. A Type-Directed Operational Semantics For a Calculus with a Merge Operator. In 34th European Conference on Object-Oriented Programming (ECOOP 2020) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 166), Robert Hirschfeld and Tobias Pape (Eds.). Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 26:1– 26:32. https://doi.org/10.4230/LIPIcs.ECOOP.2020.26

• [9] Xuejing Huang and Bruno C d S Oliveira. 2021. Distributing intersection and union types with splits and duality (functional pearl). Proceedings of the ACM on Programming Languages 5, ICFP (2021), 1–24.

• [10] David MacQueen, Gordon Plotkin, and Ravi Sethi. 1984. An ideal model for recursive polymorphic types. In Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. 165–174.

• [11] Bruno C. d. S. Oliveira, Zhiyuan Shi, and Joao Alpuim. 2016. Disjoint intersection types. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. 364–377.

• [12] Benjamin C Pierce. 1991. Programming with intersection types, union types. Technical Report. and polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University.

• [13] Garrel Pottinger. 1980. A type assignment for the strongly normalizable 휆-terms. To HB Curry: essays on combinatory logic, lambda calculus and formalism (1980), 561–577.

• [14] Baber Rehman, Xuejing Huang, Ningning Xie, and Bruno C d S Oliveira. 2022. Union Types with Disjoint Switches. In 36th European Conference on ObjectOriented Programming (ECOOP 2022). Schloss-Dagstuhl-Leibniz Zentrum für Informatik.

• [15] John C Reynolds. 1997. Design of the Programming Language F orsythe. In ALGOL-like languages. Springer, 173–233.

• [16] Nick Rioux, Xuejing Huang, Bruno C d S Oliveira, and Steve Zdancewic. 2023. A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F. Proceedings of the ACM on Programming Languages 7, POPL (2023), 515–543.

Received 2024-06-26; accepted 2024-07-24

29

--- end of page.page_number=7 ---