Subtyping on Nested Polymorphic Session Types

TL;DR

This paper investigates subtyping in nested, recursive, and polymorphic session types, proving undecidability in general, but also providing a sound algorithm that is practically effective for a specific type system extension.

Contribution

It introduces a formal study of subtyping in complex session types, proves undecidability, and offers a practical, sound subtyping algorithm with implementation insights.

Findings

Subtyping is undecidable for the studied system.

A sound subtyping algorithm was developed and implemented.

The algorithm performs efficiently on example programs.

Abstract

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.