A dynamically typed programming language, such as Elixir, allows type checking and evaluation to occur during run-time (i.e., program execution). This, in turn, makes it possible to detect and report any related errors while the program would be running.
The above could also be said for the behaviour of Elixir applications, where a certain overall pattern of behaviour is expected to be adhered to, yet never statically enforced or verified. Statically, here, refers to the compile-time instance of the program, i.e., when the program is being translated into an executable. Verifying this information statically would allow the detection of relevant errors during compile time; this would prevent them from occurring at run-time, thus leading to a more stable run-time instance of the program.
An instance of this problem is prevalent in design patterns, also known as behaviours, which are provided by the OTP (Open Telecom Platform) framework. These behaviours abstract away the concurrency aspect of systems and allow the programmer to implement their higher-level logic. They are typically split into two components: a set of public functions to interact with the behaviour itself, and a set of callbacks to define a specific logic within the behaviour. The functions would trigger the callbacks and pass along parameters; the callbacks, in turn, would process these parameters and provide return values for the functions.
In order to be able to type these behaviours., one can employ the use of session types. This would allow defining a session, or instance, between two communicating parties and hence define the expected protocol (or communication pattern) that these two parties would be expected to abide by. Since Elixir is a concurrent, actor-based language, it makes use of message-passing between processes. The protocol defined by a session type specifies the type of these messages, (integers, strings, etc.) and also the order in which they are sent and received.
On the basis of the above, the aim of this work was to establish to what extent session types could be used to statically type the behaviour of OTP design patterns and capture errors relating to them. The project has explored the possibility of achieving this objective by extending a static type-checking tool for Elixir that would employ session types. The selected tool was ElixirST.
The approach involved redefining a session type to correspond to a whole module and be oriented around the function calls made to the behaviour, as well as what the behaviour would then return. This could be accomplished through the above-mentioned callbacks. It was also necessary to introduce the notion of state to the session types, as well as the behaviours themselves within the callbacks. By using state, which could also serve as a unique identifier, it was possible to create a sequence of expected function calls and returns, with each state representing a call and a return in succession. In order to further support this, an intermediary function was also required to handle the addition of state, in order to provide a runtime guarantee that the session type would be adhered to.
Figure 1. An overview of how a behaviour has been modified to be able to cater to a session type
Student: Adrian Farrugia
Supervisor : Prof. Adrian Francalanza