2021/03/28 by Ankush Das, Henry DeYoung, Das, Ankush +5
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Model-Driven Software Engineering Techniques #Programming Languages (cs.PL)
paper · pdf · doi:10.48550/arxiv.2103.15193
openalex publication_date 2021/03/28 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
The importance of subtyping to enable a wider range of well-typed programs is undeniable. However, the interaction between subtyping, recursion, and polymorphism is not completely understood yet. In this work, we explore subtyping in a system of nested, recursive, and polymorphic types with a coinductive interpretation, and we prove that this problem is undecidable. Our results will be broadly applicable, but to keep our study grounded in a concrete setting, we work with an extension of session types with explicit polymorphism, parametric type constructors, and nested types. We prove that subtyping is undecidable even for the fragment with only internal choices and nested unary recursive type constructors. Despite this negative result, we present a subtyping algorithm for our system and prove its soundness. We minimize the impact of the inescapable incompleteness by enabling the programmer to seed the algorithm with subtyping declarations (that are validated by the algorithm). We have implemented the proposed algorithm in Rast and it showed to be efficient in various example programs.