Ce stage est proposé en collaboration avec Dashbit .

Context

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 PagerDuty, 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 semantics subtyping [3], thanks to which union, intersection, and negation types (a.k.a. set-theoretic types) can be added to existing languages [4]. 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 [5,6,7,8,9]. It currently (and gradually) being integrated in Elixir.

Goals

The current type system does not cover yet Elixir module system. Elixir is a language with first-class modules: modules can be passed to functions and returned as results. The “types” for modules are called behaviors: when you declare a behavior in Elixir, you specify a list of function callbacks, alongside their domain and codomain. A module implements (i.e., it is typed by) a behavior if it defines for each callback in the behavior a function that accepts a superset of the callback domain and returns a subset of the callback codomain. Elixir uses behaviors to implement a naive static typing of modules: if a module adopting a behavior does not implement all the callbacks of the behavior or does not do it according to their specifications, then a warning is emitted. Currently, callbacks’ domains and codomains are specified in TypeSpec [12], but the goal of this project is to integrate behaviors in the Elixir type-system under development. This will require further research. Behaviors may specify the type of callbacks in terms of abstract types, that is, nominal types whose concrete implementation is provided only by each module. In Elixir this corresponds to use term() (Elixir top type) in the TypeSpec specification of a callback. We can already more advantageously replace term() by dynamic() (the dynamic type of our gradual type system), but to fully exploit the information provided by behaviors, we need a type system capable of distinguishing the different roles of each type introduced in a behaviour: the concrete types, shared by all implementations, must be exported transparently; the abstract types, that can be processed and known only by the callback functions, must be exported opaquely; some other types, that are specific to each implementation but must be publicly known, must be instead param- eters of the behaviours. This requires to extend the semantic subtyping framework, for instance to cope with existential types for packaged modules [10,11] or Bounded Existential Types as implemented in Julia [13,14]. A concrete example of this can be found in Appendix C of [2]. At the same time, even the simpler extension where abstract types are simulated by dynamic() will require careful consideration at the language design, especially in regard to backward compatibility.

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 collaboration with José Valim (creator and main developer of the Elixir programming language, at Dashbit). The project will explore both theoretical (e.g., existential types in semantic subtyping) and practical (e.g., languages 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.

• [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 and Alain Frisch: A gentle introduction to semantic subtyping . In Proceedings of PPDP '05, the 7th ACM SIGPLAN International Symposium on Principles and Practice of Declarative Programming, pages 198-208, ACM Press (full version) and ICALP '05, 32nd International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science n. 3580, pages 30-34, Springer (summary), July, 2005. Joint ICALP-PPDP keynote talk.
• [4] 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.
• [5] 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.
• [6] Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, and Jeremy G. Siek: Gradual Typing: a New Perspective . Proc. ACM Program. Lang., vol. 3, Article 16, n. POPL '19: 46th ACM Symposium on Principles of Programming Languages, January, 2019.
• [7] Giuseppe Castagna, Mickaël Laurent, Kim Nguyen, and Matthew Lutze: On Type-Cases, Union Elimination, and Occurrence Typing. Proc. ACM Program. Lang., vol. 6, n. POPL, January, 2022.
• [8] Tommaso Petrucciani. Polymorphic set-theoretic types for functional languages . Joint PhD thesis. Università di Genova; Université Sorbonne Paris Cité – Université Paris Diderot, 2019.
• [9] Giuseppe Castagna: Typing Records, Maps, and Structs. Proc. ACM Program. Lang., vol. 7, n. ICFP, September, 2023.
• [10] Claudio V. Russo. First-class structures for standard ML. In Proceedings of the 9th European Symposium on Programming Languages and Systems, ESOP ’00, page 336–350, Berlin, Heidelberg, 2000. Springer-Verlag.
• [11] Andreas Rossberg. 1ML - Core and modules united. Journal of Functional Programming, 28, 2018.
• [12] Typespecs .
• [13]Francesco Zappa Nardelli, Julia Belyakova, Artem Pelenitsyn, Benjamin Chung, Jeff Bezanson, Jan Vitek: Julia subtyping: a rational reconstruction . Proc. ACM Program. Lang. 2(OOPSLA): 113:1-113:27 (2018)
• [14] Benjamin Chung, Francesco Zappa Nardelli, Jan Vitek: Julia's Efficient Algorithm for Subtyping Unions and Covariant Tuples (Pearl) . ECOOP 2019: 24:1-24:15

[2,3,5,10,11,13] are mandatory reading

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