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.

翻译：届会类型 静态描述同时传递信息过程之间的通信协议。 但是, 参数多元形态在会话类型中并不太清楚。 在本文中, 我们展示了会话类型的元理论, 以明确的类型量化和嵌套数据类型扩展, 并存在递归类型 。 值得注意的是, 我们证明, 类型的平等可以通过减少对一阶语法等值的追踪来改变。 此外, 由于这个问题的理论复杂性非常高, 我们建议采用新型的平等算法, 并证明它健全。 我们观察到, 算法非常有效, 尽管不完全, 也足够我们所有的例子。 我们最后举了几个例子, 说明我们增强型法的清晰度。