Abstract

In this seminar talk I will revisit the ICFP 2016 paper “Disjoint Intersection Types” and present a similar calculus where the restriction of disjointness in the well-formedness of types is lifted, and show that the most important property, that is, coherence is not compromised.

The direct consequence of this change is that the original syntactic approach of proving coherence does not apply any more. Instead, a more powerful proof method, i.e., logical relations is used to prove coherence. I will walk you through the high level overview of the proofs and show that it also simplifies the calculus a bit in several aspects.

One advantage of using logical relations is that it is robust to language extensions, and the coherence proof rarely changes. I will demonstrate that by adding one subtyping rule that adds significant expressiveness power to the calculus.