Abstract:

The polymorphic subtyping relation, which captures the more-general-than relation between polymorphic and monomorphic types, is one of the main ways modern functional programming languages handles parametric polymorphisms (generic types) at higher rank. And with the trend of the rising dependently-typed languages, we explore the theoretical foundation of the combination of polymorphic subtyping and dependent types. In this talk, I will introduce both features and my current work of formal language design that puts them together, and my plan of going forward.