Ce stage est proposé en collaboration avec Dashbit .

General presentation of the topic:

Elixir is an open-source dynamic functional programming language that runs on the Erlang Virtual Machine [1], designed for building scalable and maintainable applications. Its characteristics have earned it a surging adoption by hundreds of industrial actors and tens of thousands of developers. It is used by companies such as Discord, PepsiCo, and Pinterest. Static typing seems nowadays to be the most important request coming from the Elixir community. IRIF has an ongoing collaboration with the Elixir development team to define and implement static type-checking for Elixir. The current type system we are implementing for Elixir is described in [2]. It is a type system based on the theory of semantic subtyping [3,4], thanks to which union, intersection, and negation types (a.k.a. set-theoretic types) can be added to existing languages. It features cutting edge typing techniques: parametric polymorphism with local type inference, overloading, occurrence typing, gradual typing, and a sophisticated type analysis of patterns and guards. In the last two years this system has been gradually integrated into Elixir since version 1.17 (current version is 1.19.2). One important aspect of the type system is an accurate typing of maps (also known as "records"), which has been developed in [5] and [6] (and being implemented in Elixir). Maps are a fundamental data structure in Elixir; this is the subject of this project.

Objective of the internship:

The work in [6] extends Elixir's typing of maps with \emph{row polymorphism} as can be found in OCaml. This allows to type functions in the Elixir's Map library with greater precision. The typing of maps [5] focuses on two record forms: structs and dictionaries. Structs associate different keys with different types, requiring nominal keys for access, whereas dictionaries link all keys to a single type, with non-existent keys returning a default value. Our type theory accommodates both these structures, enabling Elixir maps to adapt to either struct-like or dictionary-like usage seamlessly. Elixir maps can therefore have several domain key types which are not all necessarily present (e.g. integers are sent to atom types, and atoms are sent to tuples). Importantly, domains are non-overlapping; this is a key limitation that comes both from design consideration and from the fact that the theory of semantic subtyping, used to compute subtyping between types, disregards the order of the fields. The solutions presented in [5] and [6] greatly improve the typing of functions of on maps in Elixir (in particular the module Map), but there is still room for improvement. We propose three different subject of internship, all related to the typing of maps in Elixir.

Subject 1: Fine-grained key types for maps in Elixir.
The type system for maps presented at a recent ICFP conference [5] proposes a solution where domains are pre-defined, and represent simple base types such as integer, atom, tuple, list, or the super-type of all types, noted term. However, in practice, some more fine-grained key types could be useful, for instance types {term, term} and {term, term, term}, which respectively represent tuples of size 2 and 3, but are subtypes of the type tuple. The project aims to explore the challenges of integrating more fine-grained key types into the type-checker for maps in Elixir. The objectives include:

1. Developing a method to represent a disjoint partition of the complete set of types, where the list of possible domains for map keys must be comprehensive yet distinct.
2. Creating a mechanism to reconcile differences in type partitions across different programs, enabling comparison and compatibility.
3. Designing a system where these partitions can be precisely defined and adapted fluidly, enhancing the typing system's accuracy and flexibility.

Subject 2: Polymorphic key types for maps in Elixir.
The goal of this internship is to investigate the integration of polymorphic key types in Elixir maps. Polymorphic key types allow for type variables to range over map keys, and would allow for more flexible and reusable code by enabling functions to accept maps with varying key types while maintaining type safety. This would allow to precisely type functions of the Map module that currently cannot be precisely typed like intersect (intersects two maps, returning a map with the common keys), merge (merges two maps, returning a map with all the keys giving priority to the second map for their definition), and take (which returns a map with only the keys specified in a list). In particular, this kind of polymorphism has been studied in [7] for Erlang, and the goal of this internship is to adapt these ideas to the typing of map defined in [5].

Subject 3: Gradual typing for maps in Elixir.
The works in [5] and [6] provide a solid foundation for the static typing of maps in Elixir. However, the system being implemented for Elixir is gradual, meaning that it allows to mix statically typed code with dynamically typed code. In practice this means to add to types a dynamic() annotation, which indicates that a value can be of any type and use relaxed typing rules. Therefore a different internship subject consists in studying how to extend the gradual typing framework of Elixir presented in [2] to the typing system of maps presented in [5] and [6].

The research will be carried out at the Research Institute on the Foundations of Computer Science (IRIF) in Paris under the supervision of Giuseppe Castagna (principal investigator for the Elixir Type System, directeur de recherche CNRS at IRIF) and in collaboration with José Valim (creator and main developer of the Elixir programming language, at Dashbit). The project will explore both theoretical (reflection on the structure of map types, design of the typing rules) and practical (e.g., language design and implementation) aspects, in a proportion that will depend on the profile of the candidate. The perspective of this proposal is that the results of this project will be integrated in the compiler of Elixir.

Candidate profile
Advanced knowledge of functional languages and basic knowledge of type systems. The student must be able to work in English in order to collaborate with José Valim and the development team of Elixir. Proficiency with Elixir or Erlang programming languages is not necessary but would be a clear advantage.

The important reference that gives a detailed description of the kind of research that will be developed for this internship is [2] (to be read first). The mandatory readings are [3,5].

• [1] The Elixir Programming Language
• [2] Giuseppe Castagna, Guillaume Duboc, and José Valim: The Design Principles of the Elixir Type System , The Art, Science, and Engineering of Programming, vol. 8, n. 2, March 2024. To appear.
• [3] Giuseppe Castagna: Programming with union, intersection, and negation types. In The French School of Programming, Springer, August, 2023. ISBN 978-3-031-34517-3. Preprint at arXiv:2111.03354.
• [4] G. Castagna: Covariance and Contravariance: a fresh look at an old issue (a primer in advanced type systems for learning functional programmers) . Logical Methods in Computer Science, n. 16, pag. 15:1―15:58, 2020.
• [5] Giuseppe Castagna: Typing Records, Maps, and Structs. Proc. ACM Program. Lang., vol. 7, n. ICFP, September, 2023.
• [6] Giuseppe Castagna and Loïc Peyrot: Polymorphic Records for Dynamic Languages. Proc. ACM Program. Lang., vol. 9, n. OOPSLA1, 4, 2025.
• [7] Erdem Yildirim, Albert Schimpf, Stefan Wehr, Annette Bieniusa. Semantic Subtyping for Maps in Erlang. 2025.

[3,5] are mandatory reading

Giuseppe Castagna : IRIF, institut de recherche en informatique fondamentale, Université Paris Cité.