Typing OTP design patterns with session types

Abstract

Concurrent and distributed programs are a challenge to write. Part of what makes them so challenging is their error prone runtime, especially in cases where certain constraints are in place, such as order of execution. The OTP library helps with the challenge of writing such programs by providing behaviours which abstract away lower level concurrency details and allow you to focus on the logic instead. However the sequencing issue at runtime is still an issue. The language of focus, Elixir, is also a dynamically typed language, which means it encourages these kinds of errors to happen at runtime. This work proposes to make use of session types implemented as a static checker in order to prevent such runtime errors from occurring. More specifically, within the context of the OTP behaviours. By using an existing static session type checker as a basis for our work, we set out to discover the extent of session types’ usability for OTP behaviours. This involves session typing Elixir modules, applying state to behaviours and formatting session types to be more based around function communication.