Calculi with disjointness received significant research interest recently. The disjointness restricts potential problematic programs. An example is the disjoint intersection types proposed for deterministic merge operator. A variant of disjointness is also implemented in the type-based switch construct in Ceylon programming language. Such a type-based switch construct provides deterministic elimination of the union types. Another variant of disjointness has recently been implemented in Scala match types. The disjointness plays an integral role in maintaining the determinism in these calculi. We propose a novel disjointness algorithm for a calculus with intersection and union types. Our disjointness algorithm naturally extends for disjoint polymorphism without any ad-hoc restrictions. Importantly, we explore the integration of merge operator and type-based switch expression in a deterministic manner based on disjointness and unambiguous upcasts.
Program Display Configuration
Tue 18 Jul
Displayed time zone: Pacific Time (US & Canada)change