Contexte

Le langage CDuce [1,2] est un langage de programmation qui est basé et utilise des types ensemblistes (types union, intersection et négation). La version polymorphede CDuce [3,4] est disponible sur le repository git du langage, mais elle n'est pas encore distribuée. Si la gestion des fonctions polymorphes est assez aboutie (voir [5] pour un panorama des possibilités offertes par les types ensemblistes polymorphes), il reste encore une importante lacune à combler avant d'avoir un langage possedant un degré de polymorphisme satisfaisant : les enregistrements (records) sont encore typés de manière monomorphe.

Elixir est un langage fonctionnel dynamique exécuté sur la machine virtuelle d'Erlang. Le langage est très populaire dans les domaines, parmi d'autres, des applications web, des systèmes embarqués, des systèmes distribués. Il est utilisé par des entreprises telles PagerDuty, Discord et Pinterest.
L'IRIF a démarré une collaboration avec Dashbit et José Valim, l'auteur de Elixir, pour définir et implémenter un système de types pour le langage. Le système comprend les types unions and intersection, l'occurrence typing et le typage graduel. Les types enregistrement jouent un rôle important dans Elixir et, plus en général, dans les langages dynamiques. Le but ultime de ce stage est de développer le typage polymorphe des enregistrements pour Elixir et de participer à leur implémentation.


Objectifs

Le typage des records avec types ensemblistes est basé sur une élégante théorie de fonctions quasi-finies qui a été définie et décrite dans le détail dans le Chapitre 9 de [6] (pour un aperçu rapide on pourra consulter l'appendice C2 de [7]).
Le but de ce stage est d'étendre cette théorie pour permettre un typage polymorphe des enregistrements. Pour cela on introduira des variables de rangée [8,13] pour capturer et décrire la partie infinie des fonctions quasi-finies représentant les types enregistrement. Il faudra développer la théorie, en prouver la correction et éventuellement étudier des extensions possibles. Parmi ces dernières on pourra étudier (1) la compatibilité avec la reconstruction des types (voir thèse de Petrucciani [9]) et/ou (2) la compatibilité avec le occurrence typing et la reconstruction d'intersections de flèches pour les fonctions, tels qui ont été décrits dans l'article [7] déjà cité. Il faudra ensuite utiliser les résultats obtenus pour implémenter le typage polymorphe des enregistrements dans la version polymorphe de CDuce.
Selon l'avancement du stage et les résultats obtenus, on pourra aussi étudier s'il est possible adapter la théorie en question pour qu'elle puisse être appliquée au typage des langages dynamiques, autrement dit, on vérifiera s'il est possible d'utiliser la dite théorie pour typer les objets JavaScript et/ou on essayera de développer des techniques qui permettent de typer des enregistrements avec des étiquettes calculées (le cas échéant on appliquera cela au typage des "maps" du langage Elixir [10]).

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