Modular session types for objects

TL;DR

This paper introduces a modular approach to session types in distributed object-oriented programming, enabling type-safe communication protocols and dynamic object behavior through class and channel session types.

Contribution

It extends session types to classes and channels, allowing modular protocol specifications and unifying communication channels with object session types in an object-oriented setting.

Findings

Type safety for message sequences and method calls.

Modular session types for classes and channels.

Integration of session types with object-oriented features.

Abstract

Session types allow communication protocols to be specified type-theoretically so that protocol implementations can be verified by static type checking. We extend previous work on session types for distributed object-oriented languages in three ways. (1) We attach a session type to a class definition, to specify the possible sequences of method calls. (2) We allow a session type (protocol) implementation to be modularized, i.e. partitioned into separately-callable methods. (3) We treat session-typed communication channels as objects, integrating their session types with the session types of classes. The result is an elegant unification of communication channels and their session types, distributed object-oriented programming, and a form of typestate supporting non-uniform objects, i.e. objects that dynamically change the set of available methods. We define syntax, operational se-mantics, a sound type system, and a sound and complete type checking algorithm for a small distributed class-based object-oriented language with structural subtyping. Static typing guarantees that both sequences of messages on channels, and sequences of method calls on objects, conform to type-theoretic specifications, thus ensuring type-safety. The language includes expected features of session types, such as delegation, and expected features of object-oriented programming, such as encapsulation of local state.