Nested Polymorphic Session Types

Session types statically describe communication protocols between concurrent message-passing processes. However, parametric polymorphism is not well understood in the context of session types. In this paper, we present the metatheory of session types extended with explicit type quantification and nested datatypes in the presence of recursive types. Remarkably, we prove that type equality is decidable by exhibiting a reduction to trace equivalence of first-order grammars. Moreover, since the theoretical complexity of this problem is very high, we propose a novel type equality algorithm and prove its soundness. We observe that the algorithm is surprisingly efficient and, despite its incompleteness, sufficient for all our examples. We conclude with several examples illustrating the expressivity of our enhanced type system.