Ce stage est proposé en collaboration avec le LRI .

Le but de ce stage est de dépasser plusieurs limitations dues à l'utilisation des variants polymorphes en OCaml et de jeter des bases théoriques pour l'étude de l'utilisation du sous-typage sémantique en OCaml. En particulier, lors de ce stage on étudiera l'intégration des types intersections dans OCaml. Ceci aussi bien pour spécifier de manière plus précise le comportement des fonctions que pour mettre en œuvre une version bornée de polymorphisme. Il s'agit donc d'un stage qui devra établir des bases théoriques rigoureuses pour ensuite les implémenter en les intégrer dans une version modifiée du compilateur OCaml
Pour plus de détails, considérons cette simple définition de fonction en OCaml pour laquelle OCaml renvoie le message Ce message signale que la fonction accepte tout argument ayant les variants `One et `Two et renvoie un résultat ayant au moins les variants `One et `Two Un premier problème est que si l'on force le type de foo à [< `One ] -> [> `One ]: OCaml repond: Donc OCaml se rend compte que le deuxième cas du match n'est pas utilisé lorsque l'argument est de type [< `One ]. Cependant le cas est pris en compte pour déterminer le type de retour, car le type déduit pour foo est [< `One ] -> [> `One | `Two ]. Mis à part le fait que la déclaration de type foo : [< `One ] -> [> `One ] quoique correcte n'est pas directement compatible avec une telle déduction car [< `One ] -> [> `One ] n'est pas un super-type de [< `One ] -> [> `One | `Two ] (ceci est du à l'instanciation d'une variable de type cachée), le problème principal est qu'une telle déduction ne permet pas d'utiliser foo lorsqu'une fonction de type [< `One ] -> [> `One ] est attendue. Il existe des cas où l'on aimerait pouvoir utiliser foo avec un tel type, car cela serait "safe". Pour éviter une duplication de code l'idée proposée par ce stage est d'utiliser un type intersection (dénoté dans la suite par le symbole &) qui déclare (et demande au type-checker de contrôler) que foo a aussi bien le type [< `One ] -> [> `One ] que le type [< `One | `Two ] -> [> `One | `Two ], et que donc elle peut être utilisée où ces types sont attendus. Il faut noter qu'ici nous visons un définition des types intersections biens plus générale que la version actuelle présente dans OCaml où l'intersection d'une utilisation très limitée.

L'utilisation des variants polymorphes fait perdre le polymorphisme à la fonction foo. Cette dernière étant la fonction d'identité on aimerait pouvoir la typer par le type suivant:

selon lequel foo a tout type obtenu en instanciant 'a par un sous-type de [`One | `Two ]. Il s'agit d'une quantification bornée car la variable quantifiée ne peut être instanciée que par les sous-types d'un certain type. Une fois de plus un tel comportement peut être obtenu par des types intersection car la quantification bornée ci dessus peut être considérée comme du sucre syntaxique pour Donc l'inclusion de types intersection permet de capturer deux mécanismes (le raffinage du typage d'une fonction définie par filtrage et la perte de polymorphisme due à l'utilisation de variantes polymorphes) apparemment très éloignés, et ceci par le système de types lui même (donc pas à un niveau meta-linguistique tel la quantification bornée définie par François Pottier dans sa thèse). En conclusion il s'agit dans ce stage d'étudier l'intégration des types intersection dans OCaml et éventuellement d'en effectuer l'implémentation. Le travail devra jeter les bases d'un travail à plus long terme visant à étudier l'intégration du sous-typage sémantique (y compris les types union) avec les langages de la famille ML.

Optionnel: Selon l'état d'avancement du stage on explorera aussi l'utilisation des types intersections pour la généralisation des variables de rangée pour les types enregistrements (record types). Une fois de plus les types interesections permettent d'enrichir l'inference de types de ML en particulier pour le types enregistrements. On demandera donc d'étudier la meilleure maniere de combiner les deux types de polymorphisme.

Une tres bonne conaissance de OCaml est attendue ainsi qu'une certaine familiarité avec la théorie des types. Rétribution possible.

Giuseppe Castagna : Laboratoire PPS, Université Paris 7.
Kim Nguyễn : LRI .