Context

CDuce [1,2] is a programming language which is based on and uses set-theoretic types (union, intersection and negation types). The polymorphic version of CDuce [3,4] is available on the language's git repository, but it is not yet distributed. If the treatment of polymorphic functions is quite successful (see [5] for an overview of the possibilities offered by polymorphic set-theoretic types), there is still an important gap to be filled before having a language possessing a satisfactory degree of polymorphism: records are still monomorphically typed.

Elixir is a dynamic functional programming language that runs on the Erlang Virtual Machine. 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, occurrence typing, and gradual typing. Record types play an important role in Elixir and, more generally, in dynamic languages. The long term goal of this internship is to develop the polymorphic typing of Elixir records and possibly contribute to its implementation in the Elixir type checker.


Goals

The 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 [6] (for a quick overview you can consult appendix C2 of [7]).
The goal of this internship is to extend this theory to allow polymorphic typing of records. For that we will introduce row variables [8,13] 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 [9]) 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 [7] already cited. It will then be necessary to use the results obtained to implement the polymorphic typing of the records for the polymorphic version of CDuce.
Depending on the progress of the internship and the results obtained, we may also study whether it is possible to adapt the theory in question so that it can be applied to the typing of dynamic languages, in other words, we will check whether it is possible to use the said theory to type JavaScript objects and/or we will try to develop techniques which allow to type records with calculated labels (and, if so, we will apply this to the typing of "maps" of the Elixir language [10]).

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