Local Type Inference for Context-Free Session Types
Bernardo Almeida, Andreia Mordido, Vasco T. Vasconcelos
TL;DR
This work tackles local type inference for FreeST, a System F–based language with context-free session types, where impredicative polymorphism and a sequential composition operator complicate type checking. It introduces a bidirectional typing framework augmented with a novel type matching algorithm that uses type reduction and explicit tracking of mu-redexes to handle the monoidal laws and left-absorbing elements of context-free session types. The authors provide a complete algorithm, a prototype integrated into the FreeST compiler, and an evaluation showing successful reconstruction of type information without most type annotations on a large codebase. The results demonstrate improved usability by eliminating many type annotations and lay groundwork for formal termination and correctness proofs, with future extensions toward deadlock-freedom via priority annotations. This work advances practical type inference for expressive session-typed languages built on System F.
Abstract
We address the problem of local type inference for a language based on System F with context-free session types. We present an algorithm that leverages the bidirectional type checking approach to propagate type information, enabling first class polymorphism while addressing the intricacies brought about by the sequential composition operator and type equivalence. The algorithm improves the language's usability by eliminating the need for type annotations at type application sites.