This project is proposed in collaboration with and partially financed by Dashbit .
Duration: 14 months or more

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 Research Institute on the Foundations of Computer Science (IRIF) in Paris has started a collaboration with Dashbit and José Valim, the author of Elixir, to define and implement a type system for the language. The system we are devising is a polymorphic type system featuring union and intersection types [2], occurrence typing [3], and gradual typing [4]. Record types play an important role in Elixir and, more generally, in dynamic languages. The goal of this post-doc position is to develop the polymorphic typing of Elixir records and possibly contribute to its implementation in the Elixir type checker.

Goals

The type system for the functional core of Elixir is being studied and developed in a PhD thesis jointly supervised by Giuseppe Castagna (IRIF) and José Valim (Dashbit) based on semantic subtyping and set-theoretic types [5]:

• 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 [6]. ^[1]
• To capture some programming patterns used in Elixir, one needs to resort to the techniques of gradual typing, parametric polymorphism, and occurrence typing, three tools whose theoretical aspects have already been studied for semantic subtyping [3,7,4]

The (monomorphic) typing of records with set-theoretic types is based on an elegant theory of quasi-finite functions which has been defined and described in detail in Chapter 9 of [8] (for a quick overview you can consult appendix C2 of [3]). The post-doctoral research proposed here will graft this theory on the one being defined for Elixir and extend it to allow polymorphic typing of records. For that, we will introduce row variables [9,10] to capture and describe the infinite part of the quasi-finite functions representing record types. It will be necessary to develop the theory, to prove its soundness and to study possible extensions. Among the latter there are the study (1) of the compatibility with type reconstruction (see thesis of Petrucciani [11]) and/or (2) of the compatibility with occurrence typing and the reconstruction of intersections of arrows for functions, such as they have been described in the article [3]. Depending on the progress of the research and the results obtained, we will implement it in the type-checker under development for Elixir and/or study whether it is possible to use the said theory to type records with calculated labels (and, if so, we will apply this to the typing of "maps" of the Elixir language).