Gradual Session Types

TL;DR

Gradual session types enable seamless integration of static and dynamic typing in session-based communication systems, enhancing safety and flexibility in multi-language web and microservice applications.

Contribution

We introduce Gradual GV, a gradually typed extension of the GV session type system, with formal semantics and safety guarantees for mixed static and dynamic typing.

Findings

Type and communication safety are maintained.

Blame safety is achieved in the extended system.

A novel approach handles linearity with dynamic types.

Abstract

Session types are a rich type discipline, based on linear types, that lifts the sort of safety claims that come with type systems to communications. However, web-based applications and microservices are often written in a mix of languages, with type disciplines in a spectrum between static and dynamic typing. Gradual session types address this mixed setting by providing a framework which grants seamless transition between statically typed handling of sessions and any required degree of dynamic typing. We propose Gradual GV as a gradually typed extension of the functional session type system GV. Following a standard framework of gradual typing, Gradual GV consists of an external language, which relaxes the type system of GV using dynamic types, and an internal language with casts, for which operational semantics is given, and a cast-insertion translation from the former to the latter. We demonstrate type and communication safety as well as blame safety, thus extending previous results to functional languages with session-based communication. The interplay of linearity and dynamic types requires a novel approach to specifying the dynamics of the language.