Approche algébrique du typage d'un langage à la ML avec objets, sous-typage et multi-méthodes
Résumé
Object-oriented langages enjoy a particular form of polymorphism by providing "methods" whose execution depends on the dynamic type of its arguments. Generally, this "dynamic dispatch" only takes into account a single argument. However, some langages feature a simultaneous dispatch on every arguments ("multi-methods").
This thesis is about the definition and the typing of a langage derived from ML with multimethods. Multi-methods are introduced as a particular form of pattern matching on objects.The presentation
of the type system uses an algebraic approach. The set of types is not predetermined but the properties necessary for the soundness of the system are axiomatised. This approach allows generic proofs independent of the choice of the algebra. It is shown how automatic type verification can be reduced to the resolution of simple first-order problems (constraints). The resolution of the constraint problems can then reuse all the results available in the litterature. The advantage of this algebraic approach is that it can handle a large class of langages at once, where the type algebra, the constraint langage, and the interpretation model of these constraints vary. This approach also provides an interesting way to study typing in a context where the interpretation world is open, i.e., when typing a module should provide a guarantee for all possible use of this module.
This thesis is about the definition and the typing of a langage derived from ML with multimethods. Multi-methods are introduced as a particular form of pattern matching on objects.The presentation
of the type system uses an algebraic approach. The set of types is not predetermined but the properties necessary for the soundness of the system are axiomatised. This approach allows generic proofs independent of the choice of the algebra. It is shown how automatic type verification can be reduced to the resolution of simple first-order problems (constraints). The resolution of the constraint problems can then reuse all the results available in the litterature. The advantage of this algebraic approach is that it can handle a large class of langages at once, where the type algebra, the constraint langage, and the interpretation model of these constraints vary. This approach also provides an interesting way to study typing in a context where the interpretation world is open, i.e., when typing a module should provide a guarantee for all possible use of this module.
Les langages à objets offrent une forme particulière de polymorphisme en permettant l'écriture de « méthodes » dont l'exécution dépend du type dynamique des arguments. Ce « dispatch dynamique » ne prend généralement en compte qu'un argument unique. Certains langages permettent le dispatch simultané sur tous les arguments et on parle alors de « multi-méthodes ». Cette thèse s'intéresse à la définition et au typage d'un langage dérivant de ML avec multiméthodes. Celles-ci sont introduites comme un cas particulier de filtrage sur les objets. La présentation du système de types utilise une approche algébrique. Plutôt que de figer l'ensemble des types, on en axiomatise les propriétés nécessaires pour la correction du système. Cela permet d'écrire des preuves génériques qui ne dépendent pas du choix de l'algèbre. On montre ainsi comment réduire la vérification automatique du typage à la résolution de problèmes simples du premier ordre (contraintes). La résolution des problèmes de contraintes peut alors réutiliser le corpus de résultats disponibles dans la littérature. L'avantage de cette approche algébrique est qu'elle permet de traiter d'un coup toute une classe de langages possibles se distinguant par la nature de l'algèbre de types, du langage d'expression des contraintes et du modèle d'interprétation de ces contraintes. Elle offre également un outil intéressant pour étudier le typage dans un contexte où le monde d'interprétation est ouvert, c'est-à-dire quand on souhaite que le typage d'un module apporte une garantie pour toutes les utilisations possibles de ce module.
Loading...