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 (un-tagged) 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.

Type systems provide specifications and enable reasoning about the programs. Among other benefits, type systems provide guarantees of the absence of certain (ill-typed) program behaviors. Refinement types further enrich the expressiveness of type systems by allowing a predicate alongside the type. The crucial divide by zero and null pointer errors are safely eliminated with refinement types. Interestingly, Correctness-by-Construction (CbC) also provides a way to set specifications for the programs. The specifications are provided for the smaller modules. Larger programs are built by composing the functionally correct smaller modules. Therefore, CbC naturally results in verified and correct programs following the program specifications. In this short paper, we highlight that CbC meets refinement types in a sense that both approaches provide specifications for program correctness and larger programs are built by composing the functionally correct smaller modules.

Subtyping is a concept frequently encountered in many programming languages and calculi. Various forms of subtyping exist for different type system features, including intersection types, union types or bounded quantification. Normally these features are designed independently of each other, without exploiting obvious similarities (or dualities) between features. This paper proposes a novel methodology for designing subtyping relations that exploits duality between features. At the core of our methodology is a generalization of subtyping relations, which we call Duotyping. Duotyping is parameterized by the mode of the relation. One of these modes is the usual subtyping, while another mode is supertyping (the dual of subtyping). Using the mode it is possible to generalize the usual rules of subtyping to account not only for the intended behaviour of one particular language construct, but also of its dual. Duotyping brings multiple benefits, including: shorter specifications and implementations, dual features that come essentially for free, as well as new proof techniques for various properties of subtyping. To evaluate a design based on Duotyping against traditional designs, we formalized various calculi with common OOP features (including union types, intersection types and bounded quantification) in Coq in both styles. Our results show that the metatheory when using Duotyping does not come at a significant cost: the metatheory with Duotyping has similar complexity and size compared to the metatheory for traditional designs. However, we discover new features as duals to well-known features. Furthermore, we also show that Duotyping can significantly simplify transitivity proofs for many of the calculi studied by us.