This project is proposed in collaboration with Dashbit .

General presentation of the topic:

Type inference for dynamic languages has been a long-standing challenge in programming language research. While ML-style type inference works well for statically-typed functional languages, dynamic languages present unique challenges due to their flexible nature and the presence of dynamic type tests. Recently, a complete type reconstruction system has been developed [1] that combines first-order polymorphism with intersection types, union types, and subtyping based on semantic subtyping [2,3]. This system allows unannotated functions to be given polymorphic types that express overloaded behavior through intersection introduction and advanced type narrowing via union elimination, making it particularly well-suited for dynamic languages. However, two critical aspects require further investigation to make this approach practical and widely applicable. First, the system lacks gradual typing support, which is essential for languages that embrace mixing typed and untyped code. Second, the type reconstruction algorithm has prohibitive computational costs due to the exponential search space of annotation trees, making it impractical for real-world applications. These limitations must be addressed before the system can be integrated into industrial dynamic languages such as Elixir [5].

Objective of the internship:

This internship focuses on extending the polymorphic type inference system described in [1] along two critical dimensions. We propose two distinct subjects of investigation (corresponding to two distinct internships).

Subject 1: Gradual typing integration.
The type inference system in [1] is defined only for fully statically typed code. The first objective is to extend the reconstruction algorithm to support gradual typing [4,5], allowing seamless integration of typed and untyped code. This requires defining how partially annotated programs interact with the inference process, how type precision is maintained across typed/untyped boundaries, and how the MSC-form and annotation trees handle gradual type information. The challenge lies in reconciling the completeness guarantees of the reconstruction algorithm with the flexibility demanded by gradual typing, while preserving the principal typing property. This extension would adapt techniques from gradual typing theory to the context of polymorphic inference with set-theoretic types.

Subject 2: Efficient implementation strategies.
The type reconstruction algorithm in [1] has prohibitive computational costs due to the exponential search space of annotation trees. The second (more practical) objective is to develop strategies to make inference tractable for real-world programs. Two complementary approaches will be explored:

1. Defining application policies that limit inference complexity by restricting where polymorphic inference is applied (e.g., only at function boundaries, or with programmer-controlled annotations that guide the reconstruction).
2. Investigating the use of Large Language Models to bootstrap the inference process by generating initial partial annotations from unannotated code, thereby drastically reducing the search space.

The first approach requires analyzing the trade-offs between inference power and computational cost. The second would transform the problem from complete reconstruction to refinement and verification of LLM-generated annotations, combining modern AI techniques with rigorous type theory.

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 (directeur de recherche CNRS at IRIF), Kim Nguyen (Associate Professor at LMF, Université Paris Saclay), and in collaboration with José Valim (creator and main developer of the Elixir programming language, and CEO of Dashbit). The project will explore both theoretical (gradual typing semantics, inference complexity analysis, completeness and soundness proofs) and practical (implementation strategies, LLM integration, application policies) 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 contribute to the broader effort of bringing advanced type systems to dynamic languages, with a potential application to the Elixir programming language.

Candidate profile
Advanced knowledge of functional languages and good knowledge of type systems. The student must be able to work in English in order to collaborate with José Valim and the Elixir development team. For the second subject (efficient implementation), some familiarity with machine learning or LLM APIs would be beneficial but is not required. Proficiency with dynamic functional programming languages would be an advantage.

The important reference that gives a detailed description of the kind of research that will be developed for this internship is [1] (to be read first). The mandatory readings are [2] and for the gradual typing extension [4].

• [1] Giuseppe Castagna, Mickaël Laurent, and Kim Nguyen: Polymorphic Type Inference for Dynamic Languages. Proc. ACM Program. Lang., vol. 8, n. POPL, January, 2024.
• [2] Giuseppe Castagna: Programming with union, intersection, and negation types. In The French School of Programming, Springer, August, 2023. ISBN 978-3-031-34517-3.
• [3] 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.
• [4] Giuseppe Castagna, Victor Lanvin, Tommaso Petrucciani, and Jeremy G. Siek: Gradual Typing: a New Perspective. Proc. ACM Program. Lang., vol. 3, n. POPL, January, 2019.
• [5] 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.

Giuseppe Castagna : IRIF, Research Institute on the Foundations of Computer Science, Université Paris Cité. Kim Nguyen : LMF, Formal Methods Laboratory, Université Paris Saclay.