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.