Local Type Inference for Context-Free Session Types

TL;DR

This paper introduces a novel local type inference algorithm for a language with System F and context-free session types, enhancing usability by reducing the need for explicit type annotations.

Contribution

It presents a bidirectional type checking algorithm that supports first-class polymorphism and handles complex type constructs in session-typed languages.

Findings

The algorithm successfully infers types without explicit annotations.

It manages the complexities of sequential composition and type equivalence.

The approach improves language usability and type inference efficiency.

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.