TITRE: Étude du polymorphisme pour des types enregistrement dans des langages dynamiques
Références
Contacts
Proposition de Post-doc
TITRE: Étude du polymorphisme pour des types enregistrement dans des langages dynamiques
Ce post-dec est proposé en collaboration avec Dashbit .
Durée: 14 mois ou plus
Context
Elixir is a dynamic functional programming language that runs on the Erlang Virtual Machine [1]. 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 [2], occurrence typing [3], and gradual typing [4]. Record types play an important role in Elixir and, more generally, in dynamic languages. The goal of this post-doc position is to develop the polymorphic typing of Elixir records and possibly contribute to its implementation in the Elixir type checker.
Goals
The type system for the functional core of Elixir is being studied and developed in a PhD thesis jointly supervised by Giuseppe Castagna (IRIF) and José Valim (Dashbit) based on semantic subtyping and set-theoretic types [5]:
Union and intersections types that characterize semantic subtyping are the right tools for typing key aspects of the Elixir language: intersection types are needed for a fine-grained typing of overloaded functions, while pattern-matching and guards require union and negation types [6].[1]
To capture some programming patterns used in Elixir, one needs to resort to the techniques of gradual typing, parametric polymorphism, and occurrence typing, three tools whose theoretical aspects have already been studied for semantic subtyping [3,7,4]
The (monomorphic) 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 [8] (for a quick overview you can consult appendix C2 of [3]). The post-doctoral research proposed here will graft this theory on the one being defined for Elixir and extend it to allow polymorphic typing of records. For that, we will introduce row variables [9,10] 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 [11]) 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 [3].
Depending on the progress of the research and the results obtained, we will implement it in the type-checker under development for Elixir and/or study whether it is possible to use the said theory to type records with calculated labels (and, if so, we will apply this to the typing of "maps" of the Elixir language).
[4] 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.
[5] G. Castagna and A. 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.
[1] As an example, the overloaded sum function has type (Int×Int → Int)∩(Real×Real → Real)∩ ...(read the intersection ∩ as “and"); in pattern matching, a variable that captures the expression matched by some pattern does not have the type captured by previous patterns (i.e. it has a negation type) and the whole matching expression has the union of the types of all branches of the pattern matching.