Disjoint Intersection Types and Disjoint Quantification
George
Abstract
Intersection types can be the foundation of languages embracing extensibility. Yet many type systems with intersection types are known to suffer the incoherence problem, which means a program can have multiple meanings. The lack of coherence leads to unexpected program behaviours and is not desirable in practice. In this talk, I will show a simple type system with intersection types, parametric polymorphism, and subtyping, which is coherent. The current system is inspired by systems with bounded quantification; the latter supports both subtyping and parametric polymorphism.