A blend of intersection types and union types

Abstract

Languages define the constructs and protocols of communication. Programming languages, in particular, define the constructs that assist in communicating with machines. With the growing complexity and need of software applications, it has become a challenge to design an expressive, yet simple programming language. The complexity in a language design mostly occurs due to the interaction of disparate features. This thesis is an effort in simplifying and formally studying the design of intersection and union types in programming languages.

Intersection and union types are advance and powerful features available in many modern programming languages. Intersection types provide an interface to introduce an expression of multiple types. Union types, on the other hand, provide an interface to express an expression of variant types. Interaction of intersection and union types is known to be non-trivial in theory. This thesis examines the interaction of intersection and union types. Our study starts with a deterministic type-based switch expression for the elimination of union types. Disjointness plays an integral role in keeping the calculus deterministic, which ensures that no two branches of a type-based switch expression overlap. Thus the scrutinee falls in a maximum of one branch. The resulting calculus is called λu . We further extend λu with powerful and advance features of intersection types, subtyping distributivity, nominal types, and polymorphism. Moreover, we study λu with the merge operator. An extension with the merge operator poses novel challenges in determinism.

Intersection and union types are well-known dual features. We also examine the duality of intersection and union types formally in this thesis. The duality unifies some of the subtyping rules and reduces the theoretical complexity of a system with dual features. The benefits include the reduction in number of subtyping rules and simplified proofs for certain theorems such as subtyping transitivity. All of the metatheory of this thesis has been formalized in the Coq theorem prover.