At the heart of every compiler lies a type equivalence algorithm. While this algorithm is relatively straightforward for nominal type systems, where simple checks on type names suffice, it gets more complex in structural type systems, where the structure of types must correspond in a certain sense. For simple types, this algorithm merely descends on their abstract syntax tree: there is, after all, little difference between what is meant by structure and by syntax. But this gap builds up as we introduce features such as polymorphism, equirecursion and type operators. In the presence of these features—system $F^{\mu*}_\omega$—type equivalence can be reduced to equivalence for regular languages.

Why do we need grammars then? Simply because we are dealing with an even more expressive system—$F^{\mu*;}\omega$—obtained by incorporating $F^{\mu*}\omega$ into FreeST, a functional programming language with session types, a type discipline provides safe concurrency by describing and enforcing structured message-passing protocols on heterogeneous and bidirectional channels. Session types in FreeST are context-free, allowing the sequential composition of arbitrary protocols. Sequential composition lifts the restriction to tail recursion, but in turn precludes the use of a least fixed-point construction to decide type equivalence. In this setting, the problem is reduced to the bisimilarity of simple grammars, an amenable subset of context-free grammars. However, functional types and context-free session types cannot be dealt with separately: sessions may carry functions, and functions may act on sessions. As such, we need a type equivalence algorithm that seamlessly deals with both. Reducing type equivalence in $F^{\mu*;}_\omega$ to simple grammar bisimilarity is the way to go.