On peut distinguer deux types d'approches pour définir une relation de
sous-typage sur une algèbre de types. L'approche syntaxique consiste à
axiomatiser la relation avec un système de règles inductives ou
coinductives. L'approche sémantique utilise une interpretation des types
dans un modèle pour définir le sous-typage, par exemple comme l'inclusion
dans le cas d'une interpretation ensembliste.
Je vais montrer comment appliquer cette approche sémantique au cas d'une
algèbre de types plutôt riche, avec les constructeurs classiques (types de
base, produit, flèche), les combinaisons booléennes arbitraires finies
(types intersection, union, complémentaire), et les types récursifs.
Cependant, étant donné les caractéristiques du langage, on ne peut pas
définir de modèle du langage avant de disposer du système de type, et donc
de la relation de sous-typage. Il s'agit de rompre le cycle de dépendance
pour appliquer tout de même l'approche sémantique.
Ce travail constitue la base du système de types de CDuce. CDuce reprend
les caractéristiques du langage XDuce spécialisé dans la manipulation de
documents XML, les replace dans un cadre moins spécifique, et ajoute
l'ordre supérieur (les fonctions sont de plus surchargées, et l'opération
de dispatch dynamique est unifiée avec le filtrage).
Ref:
* Semantic Subtyping. A. Frisch, G. Castagna, V. Benzaken. In LICS 2002,
to appear. ftp://ftp.ens.fr/pub/di/users/castagna/lics02.ps.gz
* Le langage CDuce: http://www.cduce.org/