A practical type system for generalized recursion
Résumé
The ML language is equipped with a sophisticated module system, especially thanks to its notions of functor (higher-order functions on modules) and of controlled type abstraction (opaque or transparent types). Nevertheless, an important weakness of this system hinders modularization: the impossibility to define mutually recursive modules. In particular, mutually recursive functions must all reside in the same module. Recently, Leroy extended the OCaml language, a dialect of ML, with an unsafe notion of recursive modules. In this extension, one can define recursive modules, but the system does not check that they are well-founded. If not, the system throws an exception at runtime, which is annoying given the strong typing of ML. Powerful type systems have been proposed to tackle this issue, but they require rather deep modifications to the ML type system. This report presents a system requiring only local modifications to the ML type system. We prove its soundness by injection into one of the evoked more general formalisms.
Le langage ML est doté d'un système de modules sophistiqué, notamment grâce aux foncteurs (fonctions d'ordre supérieur sur les modules) et à son mécanisme d'abstraction de types contrôlée (types manifestes ou abstraits). Cependant, une faiblesse importante de ce système gêne la modularisation des programmes : l'impossibilité de définir des modules de façon mutuellement récursive. Notamment, les définitions de fonctions mutuellement récursives doivent toutes résider dans le même module. Récemment, Leroy a étendu le langage OCaml, un dialecte de ML, avec une notion non sûre de modules récursifs. Avec cette extension, on peut définir des modules récursifs, mais le système ne vérifie pas que ces définitions sont bien fondées. Lorsqu'elles ne le sont pas, le système lance une exception à l'exécution, ce qui cadre mal avec le typage fort de ML. Des systèmes de types assez généraux ont été proposés récemment pour gérer ce problème, mais leur mise en oeuvre demande une modification en profondeur du typage de ML. Ce rapport propose un système ne nécessitant que des modifications locales au typage de ML. Nous prouvons sa sûreté par injection dans l'un des formalismes plus généraux évoqués ci-dessus.
Origine : Fichiers produits par l'(les) auteur(s)