Séminaire VASCO - Mickaël LAURENT

Résumé :
On classe parfois les langages de programmation en deux grandes catégories : les langages statiques, tels que C, Rust et OCaml, et les langages dynamiques, tels que Python, JavaScript et Elixir. 
Si les langages statiques offrent généralement de meilleures performances et une plus grande sûreté grâce à une phase de typage statique qui précède la compilation (« well-typed programs cannot go wrong »), cela se fait souvent au détriment de la flexibilité, rendant les programmes plus sûrs mais le prototypage plus fastidieux. 
Dans cet exposé, je présente un système de type statique adapté aux langages dynamiques, offrant ainsi un compromis entre sûreté et flexibilité.

Le typage statique de langages dynamiques pose de nombreux défis. En particulier, les fonctions peuvent être surchargées : elles peuvent exhiber des comportements différents selon le type de leurs paramètres. 
La sélection (dispatch) parmi ces différents comportements ne peut pas toujours être faite statiquement, et a géneralement lieu au moment de l'exécution (soit via des tests de type explicites, soit via un mécanisme de dispatch dynamique intégré au langage). En outre, les programmes n'ont généralement pas (ou peu) d'annotations de type. Pour résoudre ces problèmes,je présente un système de types qui combine, de manière contrôlée, du polymorphisme de premier ordre, des types intersection, des types union et du sous-typage, et fournit un algorithme pour déduire automatiquement le type des fonctions (inférence de type). Il en résulte une discipline de type dans laquelle des fonctions non annotées reçoivent des types polymorphes (grâce à Hindley-Milner) qui peuvent capturer le comportement surchargé des fonctions qu'ils typent (grâce aux types intersection) et qui sont déduits en appliquant des techniques avancées de rétrécissement de type (grâce aux types union).