Le typage statique avec types polymorphes, comme dans le langage ML, s'adapte parfaitement aux langages purement applicatifs, leur apportant souplesse et expressivité. Mais il ne s'étend pas naturellement au trait principal des langages algorithmiques: la modification en place des structures de données. Des difficultés de typage similaires apparaissent avec d'autres extensions des langages applicatifs: les variables logiques, la communication inter-processus à travers des canaux, et la manipulation de continuations en tant que valeurs. Ce travail étudie, dans le cadre de la sémantique relationnelle, deux nouvelles approches du typage polymorphe de ces constructions non-applicatives. La première repose sur une restriction de l'opération de généralisation des types (la notion de variables dangereuses), et sur un typage plus fin des valeurs fonctionnelles (le typage des fermetures). Le système de types obtenu reste compatible avec le noyau applicatif de ML, et se révèle être le plus expressif parmi les systèmes de types pour ML plus traits impératifs proposés jusqu'ici. La seconde approche repose sur l'adoption d'une sémantique “par nom” pour les constructions du polymorphisme, au lieu de la sémantique “par valeur” usuelle. Le langage obtenu s'écarte de ML, mais se type très simplement avec du polymorphisme. Les deux approches rendent possible l'interaction sans heurts entre les traits non-applicatifs et le typage polymorphe. (See [100] for an English translation.)
[ bib | Local copy ] Back
This file was generated by bibtex2html 1.99.