This project is proposed in collaboration with 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). Elixir features a powerful module system with first class modules, whose typing is under development. This is the subject of this project.

Objective of the internship:

Elixir's module system is currently being extended with a type system based on the approach described in Andreas Rossberg's "1ML - Core and modules united" [5]. This work follows from a previous internship that established the foundation for typing Elixir's modules using 1ML's unified approach, where modules and values are treated uniformly within a single type-theoretic framework. However, two critical aspects remain to be addressed:

• Gradual typing integration: The current module type system is defined only for statically typed code, but Elixir's philosophy embraces gradual typing [2], allowing seamless mixing of typed and untyped code. The module system must support this graduality.
• Semantic subtyping foundations: Elixir's core type system is based on semantic subtyping [3,4], which provides elegant handling of union, intersection, and negation types. However, the module type system introduces features that are usually captured by using existential types (used to encode abstract data types and information hiding), which have not yet been integrated into the semantic subtyping framework. Understanding the relationship between these two subtyping disciplines is crucial for a coherent type system.

We thus propose two distinct subjects of investigation (corresponding to two distinct internships).

Subject 1: Gradual typing integration for Elixir's module system.
The first subject aims to extend the module type system to support gradual typing, adapting the techniques from [2] to the module context, thereby enabling seamless integration of typed and untyped modules consistent with Elixir's gradual typing philosophy. This will allow developers to gradually add types to their modules while maintaining compatibility with untyped code, following Elixir's philosophy of progressive type adoption.

Subject 2: Semantic subtyping foundations for existential types.
The second subject (much more difficult) is to study how to integrate existential types—which encode abstract data types and information hiding in the module system—into the semantic subtyping framework [3,4]. This would require proving that the subtyping relation induced by the module system (based on 1ML) coincides with the subtyping relation derived from the semantic interpretation of existential types, thus reconciling these two approaches and ensuring that the module type system aligns with Elixir's core type system at a foundational level.

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, CEO of Dashbit). The project will explore both theoretical (theory of gradual typing, extension of semantic subtyping) and practical (e.g., language and module typing system 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.
• [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] Andreas Rossberg: 1ML - Core and modules united. Journal of Functional Programming, 28, 2018.

Giuseppe Castagna : IRIF, Research Institute on the Foundations of Computer Science, Université Paris Cité.