Master project description
TITLE: Set-theoretic types for the Elixir programming language
This project is proposed in collaboration with Dashbit .

Context

Elixir is a dynamic functional programming language that runs on the Erlang Virtual Machine [1]. The language has been gaining adoption over the last years in areas such as web applications, embedded systems, data processing, distributed systems, and more. It is used by companies such as PagerDuty, Discord, and Pinterest. The overall goal of this project is to define the type system for Elixir and work directly with the Elixir team to add the type system to the language. The master internship will focus on the definition of a type system for a functional core of the Elixir language. The starting point for the work will be the theory of semantics subtyping, thanks to which union, intersection, and negation types (a.k.a. set-theoretic types) can be added to existing languages [2]. The research will be carried out at the Research Institute on the Foundations of Computer Science (IRIF) in Paris under the joint supervision of Giuseppe Castagna (principal investigator of semantic subtyping, directeur de recherche CNRS at IRIF) and José Valim (creator and main developer of the Elixir language, at Dashbit). The perspective of this proposal is that the results of the master internship will be pursued (by the master candidate) in a PhD thesis aiming at defining and implementing a full-fledged state-of-the-art type system for the complete Elixir language, thesis that may be funded by a CIFRE PhD program.

Goals

There are many aspects that make semantic subtyping ad set-theoretic types the right candidates for a type system for Elixir and that are of interest both for developers and researchers:
  • Union and intersections types that characterize semantic subtyping are the right tools for typing key aspects of the Elixir language: intersection types are needed for a fine-grained typing of overloaded functions, while pattern-matching and guards require union and negation types.[3] [1]
  • To capture some programming patterns used in Elixir programming one needs to resort to the techniques of gradual typing, parametric polymorphism, and occurrence typing, three tools whose theoretical aspects have been already studied for semantic subtyping [4,5,6]
  • The Elixir team wants to go beyond type annotations and make type signatures a direct part of the language in a way to add new idioms and expressive power to the engineering teams that opt-in. This should open new perspectives in the theory of typing and the application of bi-directional typing.
  • The language and runtime of Elixir have a distinct focus on fault-tolerance, concurrency, and distribution, which can lead to interesting typing considerations and modelling
  • As work progresses, the Elixir team will collect feedback from the community, which will point paths for improvements and help developers see real-world usage from their efforts. The master thesis and the subsequent thesis will be characterized by a constant and mutual feedback and dependency between theory and practice.
  • Finally, a long term interesting area of exploration is the interface between typing and meta-programming and how that can lead to an extensible type system
References
[1] As an example, the overloaded sum function has type (Int×Int → Int)∩(Real×Real → Real)∩ ...(read the intersection ∩ as “and"); in pattern matching, a variable that captures the expression matched by some pattern does not have the type captured by previous patterns (i.e. it has a negation type) and the whole matching expression has the union of the types of all branches of the pattern matching.