A semantic foundation for gradual set-theoretic types

Types graduels ensemblistes Cette thèse porte sur l'étude des interactions entre les types ensemblistes et le typage graduel. Les types ensemblistes sont des types proposant des connecteurs d'union, d'intersection, et de négation, qui permettent de typer des programmes de manière très fine et puissante. Par exemple, l'union permet de spécifier très précisément le type d'une instruction conditionnelle, tandis que l'intersection permet d'encoder la surcharge de fonctions dans le système de types. À l'opposé, le typage graduel permet au programmeur d'outrepasser les vérifications statiques réalisées par le système de types, afin, par exemple, d'accélérer la phase de prototypage. Les types ensemblistes se prêtent naturellement à une approche sémantique, dans laquelle laquelle les types sont interprétés comme des ensembles de valeurs, et le sous-typage est défini comme l'inclusion ensembliste sur ces ensembles. Cette approche, dite du sous-typage sémantique, est adoptée tout au long de cette thèse. À l'inverse, le typage graduel est une notion beaucoup plus syntaxique: c'est à l'aide d'une annotation explicite que le programmeur spécifie au type-checker de ne pas réaliser de vérifications. Dans la plupart des travaux existants, la relation de sous-typage est étendue de manière ad-hoc et syntaxique pour supporter le typage graduel, ce qui la rend très rigide et peu extensible. Dans cette thèse, nous tâchons de réconcilier les deux approches, en proposant des interprétations plus sémantiques du typage graduel. Le manuscrit est composé de deux parties. Dans la première partie, nous proposons une nouvelle approche permettant d'étendre de manière automatique un système de types avec du typage graduel. L'originalité de cette approche vient du fait que le typage graduel est ajouté de manière déclarative au système à l'aide d'une simple règle logique. Ainsi, il n'est pas nécessaire de modifier les règles existantes, comme cela est souvent fait. Nous proposons ensuite des versions algorithmiques, basées sur des algorithmes de résolution de contraintes, pour chaque système déclaratif. Nous illustrons cette approche sur deux systèmes différents. Le premier est un système de types à la Hindley-Milner sans sous-typage. Nous décrivons un langage source graduellement typé, un langage cible comportant des vérifications de type dynamiques (aussi appelées « casts »), ainsi qu'un algorithme de compilation pour passer du premier au second. Nous répétons ensuite cette présentation en étendant ce langage avec des types ensemblistes, ainsi qu'avec une relation de sous-typage sur les types graduels ensemblistes. Dans la deuxième partie du manuscrit, nous abordons la réconciliation des types graduels et des types ensemblistes sous un autre angle. Tandis que la première partie propose une approche logique, la seconde partie tente de fournir une approche plus sémantique de ce problème. Plus particulièrement, dans cette partie nous tentons de réconcilier l'interprétation des types proposées par l'approche du sous-typage sémantique avec l'interprétation des expressions d'un langage, ceci dans l'optique de proposer une sémantique dénotationnelle pour un langage graduellement typé. Nous attaquons ce problème en plusieurs étapes. Tout d'abord, nous proposons une sémantique dénotationnelle pour un lambda-calcul simple, basée directement sur l'approche du sous-typage sémantique. Ceci nous mène à remarquer quelques problèmes, que nous corrigeons en modifiant l'approche considérée. Nous continuons ensuite en fournissant une sémantique dénotationnelle complète pour la partie fonctionnelle du langage CDuce, un langage supportant des types ensemblistes ainsi que diverses constructions complexes (fonctions surchargées, tests de type dynamiques, non-déterminisme). Enfin, nous nous intéressons à un lambda-calcul graduellement typé. Nous proposons une interprétation ensembliste des types graduels qui nous mène à des résultats puissants portant sur la représentation des types graduels.