Les langages de programmation sont dépendants des applications qu'ils permettent de programmer : les opérations définies dans un langage permettent de réaliser des tâches particulières. Par exemple, le langage Lisp permet d'implémenter une algorithmique fonctionnelle adaptée à l'intelligence artificielle et à la déduction automatique. Le langage C, qui permet de manipuler les adresses mémoire, est couramment utilisé pour implémenter des fonctions du système d'exploitation. Certains langages à objets tels que Java permettent de concevoir des interfaces utilisateurs à un moindre coût et d'utiliser, de façon intégrée, des protocoles réseau de haut niveau. La nature des types de données proposés par chacun de ces langages diffère selon la nature des données traitées : le langage C permet la manipulation de variables de type pointeur, tandis que le langage Java l'interdit. Les structures de données complexes dans le langage Lisp sont toutes construites à base de tuples, tandis que les autre langages proposent des constructions de types plus élaborées (structures, enregistrements).
L'affectation de types aux variables et aux expressions d'un programme permet au programmeur de ne pas avoir le souci de la représentation en mémoire des données manipulées. Lorsqu'il utilise un langage non typé, tel que l'assembleur, le programmeur doit contrôler que le domaine des variables et les paramètres des instructions qu'il écrit sont corrects. De même, il doit gérer la réservation et la libération des espaces mémoire nécessaires pour le stockage de ces variables.
Par contre, Le l-calcul, qui peut également être considéré comme un langage non typé (ce n'est pas un langage de programmation), garantit l'absence d'erreur car toute donnée est une fonction et retourne donc forcément un résultat valide, de même tout opérateur est une fonction et retourne donc un résultat. Cependant les expressions fonctionnelles sont difficiles à comprendre. Cela présente un inconvénient pour la maintenance des programmes écrits dans des langages proches du l-calcul (Lisp, Scheme).
Les types de données apportent un supplément d'information permettant au système de prendre en charge les tâches qui incombent au programmeur dans les langages non typés (réservation de mémoire, contrôle des domaines de valeur), tout en apportant une meilleure lisibilité des programmes [Cardelli 85], ce qui se traduit par :
Nous donnons ici la définition des éléments d'un langage de programmation typé, ainsi que deux approches permettant l'affectation de types aux variables d'un programme.
L'ensemble des types pouvant être exprimés dans un langage, les règles qui permettent de les définir et les règles qui définissent le type d'une expression sont communément appelés système de types du langage.
L'ensemble des types valides d'un langage est composé de types de base représentant les unités d'information atomique pouvant être manipulées par le langage. Par exemple, les types entier, booléen, caractère, chaîne ou réel sont des types de base couramment définis dans les langages de programmation. Ces types de base peuvent être combinés entre eux pour définir des types construits. Deux approches permettent de définir ou d'utiliser les types construits :
Chacune de ces deux approches implique des politiques différentes pour la compilation et l'interprétation des langages qui les utilisent. Les techniques mises en oeuvre pour garantir la correction d'un programme vis-à-vis du système de types du langage sont également différentes.
D'une manière générale nous pouvons dire que les langages explicitement typés permettent une meilleure compréhension des programmes et une économie du temps de compilation et d'exécution. En contrepartie, ils imposent des contraintes sur l'application des traitements à des variables d'un type donné : les variables utilisées dans un calcul doivent être d'un type acceptable pour l'opérande auquel elles sont appliqués.
La plupart des langages explicitement typés permettent de nommer des expressions de type pour les ré-utiliser ultérieurement. Le nommage d'une expression de type est introduit par un mot-clé spécifique (typedef en C, type en Pascal) et définit un nom de type. Si un nom de type est utilisé dans l'expression qui le définit, le type est alors un type récursif.
Le calcul des types des expressions et des variables des programmes écrits dans des langages implicitement typés implique un surcoût de temps à l'exécution du programme. Le type d'une variable ne peut pas toujours être déduit d'une seule expression, et le système doit faire des hypothèses sur le type de la variable qui pourront être confirmées ou infirmées par la suite. Dans l'exemple suivant,
a = 1 + 3;
Le type de a peut être entier ou réel, le système doit conserver tous les types potentiels de la variable a, pour éventuellement choisir ultérieurement. L'expression
a = sin (b/2);
détermine le type réel pour a. Certains types peuvent être incomplets du fait qu'une expression utilise des variables dont le type n'a pas encore été déterminé. Dans ce cas des variables de type doivent être introduites pour paramétrer le type cherché. Une expression est dite entièrement typée lorsque l'ensemble des variables de type utilisées pour définir son type sont valuées (voir section A.4).
Les types de données permettent une plus grande lisibilité des programmes et un temps de développement réduit. L'utilisation de systèmes de types permettent également d'écarter les erreurs à l'exécution. En effet, lors de la compilation ou de l'exécution d'un programme, le système de types est un moyen de contrôler que les paramètres appliqués à un opérateur ou à une fonction sont corrects. Il est ainsi possible de prévoir si une opération pourra aboutir et donnera un résultat (type et domaine des paramètres corrects) ou si elle déclenchera à coup sûr une erreur (paramètres incorrects).
La sécurité des programme à l'exécution n'est pas l'intérêt premier de ce travail, mais cette propriété de sécurité s'appuie d'une part sur le fait qu'un programme est bien typé, d'autre part que le système de type du langage permet d'assurer cette propriété, c'est à dire que les opérations permises par les langages ne produisent que des variables de valeurs correctes par rapport à leur type. Ce n'est pas le cas, par exemple, de l'opération de coercition (ou casting) du langage C qui permet de changer le type d'une valeur sans contrôler sa validité pour le type dans lequel elle est transformée.
Les systèmes de types assurant la propriété de sécurité à l'exécution restreignent en général la souplesse de programmation en interdisant les opérations de changement de type pouvant engendrer des erreurs de type. L'arithmétique de pointeurs est généralement exclue des langages utilisant un système de type conservant la propriété de sécurité.
La conception d'un langage de programmation se heurte donc au défi de proposer un système de type sûr sans restreindre les opérations proposées à l'utilisateur.
Dans cette section nous décrivons un langage permettant de spécifier le système de types d'un langage et de l'exploiter pour décrire les algorithmes de contrôle et d'inférence de types.
Un système de types s'appuie sur la syntaxe du langage pour lequel il est défini, associant aux noeuds de l'arbre syntaxique (construit par l'interpréteur ou le compilateur) une information de type sous la forme d'attributs. Nous donnons ici une représentation permettant de décrire la façon dont ces attributs sont calculés et/ou vérifiés.
Nous appuyons notre description sur un exemple de langage simple que nous
nommerons L. Ce langage permet de décrire des programmes
constitués d'un ensemble de variables typées et d'une expression
unique. Sa grammaire est donnée par la figure 57. Les programmes décrits par le langage
L (P) sont composés d'une partie déclaration
(D) où sont déclarées les variables et les
types (T) auxquelles elles appartiennent et d'une partie
expression (E) combinant des littéraux et des variables
(id) à l'aide des opérateurs d'addition d'entiers
(+), de concaténation de chaînes
(&), d'accès à un tableau, à une
structure et d'application de fonctions.
P ® D ; E
D ® D ; D | id : T
T ® 'entier' ½ 'chaîne' | 'tableau' '[' entier ']' 'de' T |
'structure' '{' D '}' |
'fonction' '(' id ':' T ')' ':' T '{' E '}'
E ® littéral ½ nb ½ id ½ E '+' E ½ E '&' E |
E '[' E ']' | E '.' id | E '(' E ')'
Figure 57 - Grammaire du langage L.
Le langage L est un langage fonctionnel ne contenant pas de structures de contrôle telles que les boucles ou les expressions conditionnelles. Les structures de contrôle ne posant pas de problèmes particulier pour le contrôle de type et nous les avons ignorées pour simplifier la syntaxe du langage.
Un programme est engendré par le non-terminal P de la grammaire. Les déclarations de variables typées (D) sont composées d'un identificateur et d'une expression de type. Voici un exemple de programme écrit avec le langage L qui calcule le double de la variable a :
a : entier;
double : fonction ( c : entier ) : entier
{
c + c
};
double (a)
Les expressions de types de ce programme sont : entier (pour
définir le type de la variable a) et fonction (entier) :
entier (pour définir le type de la variable double).
Le langage L comme tous les langages de programmation définissent deux catégories de types, les types de base et les types construits :
Les expressions de type ne sont pas appropriées au algorithmes de contrôle de type. Il est plus commode de représenter les types sous forme de graphes. La figure 58 montre la représentation sous forme de graphe d'une expression de type. Dans un graphe de types, les noeud terminaux représentent les types de base et les noeuds non terminaux sont étiquetés avec les constructeurs des types qu'ils représentent (en police courrier), les noms de types appartenant à chacun des noeuds étant donnés à titre indicatif (en italique).
[Here is a Drawing]Figure 58 - Un exemple de type construit et son graphe de types
Par la suite nous assimilerons un type et le graphe engendré par l'ensemble des sommets pouvant être atteints depuis le sommet représentant le type. Dans la figure 58, nous avons représenté le type ident en rouge.
Le contrôle de type d'une expression s'appuie sur un ensemble de règles sémantiques donnant le type de cette expression en fonction du type de ses opérandes. Pour les unités syntaxiques représentant les types de base, ces règles sont :
E ® littéral
chaîne
E ® nb
entier
La fonction TypeSymb recherche dans la table des symboles le type d'un identificateur id. Cette fonction est utilisée lorsqu'un identificateur est rencontré dans une expression :
|
E ® id |
TypeSymb (id) |
Le type d'une expression construite dépend du type de ses opérandes :
E ® E1 + E2
si Type (E1) = entier
et Type (E2) = entier
alors entier
sinon erreur de type.
E ® E1 & E2
si Type (E1) = chaîne
et Type (E2) = chaîne
alors chaîne
sinon erreur de type.
La vérification de type lors de l'accès à une cellule de tableau dépend du type des éléments du tableau. Pour désigner ces éléments, on utilise une variable de type t, permettant de faire abstraction du type de données stockés dans le tableau.
E ® E1[ E2]
si Type(E1) = tableau de t
et Type(E2) = entier
alors t
sinon erreur de type.
E ® E1
si Type(E1)= pointeur vers t
alors t
sinon erreur de type.
Lors de l'accès à un champ de structure il faut vérifier que l'identificateur de champ représente réellement un champ de la structure, pour cela, on utilise la fonction champs, retournant l'ensemble des identificateurs des champs d'une structure. La fonction ChercherType recherche le type d'un champ particulier d'une structure.
E ® E1.id
si Type (E1) = structure
et id Ì Champs (E1)
alors ChercherType (E1.id) sinon erreur de type.
E ® E1(E2)
si Type (E1) = fonction (t1) : t2
et Type (E2) = t1
alors t2 sinon erreur de type.
Un algorithme simple de contrôle de type consiste à parcourir l'arbre syntaxique de l'expression en calculant le type de chaque noeud en fonction des types de ses composants. Le type de l'expression est correct si l'algorithme ne retourne pas d'erreur de type.
Les fonctionalités décrites ci-dessus sont proposées par de nombreux langages de programmation et nécessitent la mise en oeuvre de techniques de contrôle de type plus complexes pour déterminer si un programme est bien typé et donc exempt d'erreurs non désirables à l'exécution (propriété de sûreté). Ces techniques avancées que sont l'inférence de type, la surcharge d'opérateur, la coercition, l'équivalence de types ou encore les fonctions polymorphes sont exposées dans la section suivante.
Le langage et l'algorithme de vérification de type présentés ci-dessus sont basiques et ne supportent pas la plupart des caractéristiques de langages de programmation de haut niveau. Les caractéristiques suivantes ne sont pas proposées par le langage L et ne sont pas supportées :
Pour permettre ces fonctionalités dans un langage de programmation, tout en conservant la propriété de sécurité à l'exécution, un contrôleur de types doit intégrer :
L'inférence de type a pour but de calculer, s'il existe, le type d'une expression non typée. Lorsqu'une expression est évaluée, les types de chacune des variables et de ses opérandes doivent être évalués pour savoir s'il sont compatibles avec l'opérateur.
Formellement, le problème de l'inférence de type est exprimé de la façon suivante : étant donnée une expression M, existe-t-il un type A parmi les types pouvant être engendrés par les règles du système de types tel que Type (M) = A ?
L'algorithme d'inférence de type d'une expression exploite la même structure de données que l'algorithme de vérification : Pour typer l'expression M, on parcoure l'arbre syntaxique de l'expression M en assignant à chaque noeud un attribut de type calculé conformément aux règles du système de types associé au langage.
Contrairement à l'algorithme de vérification de type, l'algorithme d'inférence parcourt l'arbre syntaxique d'une expression de bas en haut, en calculant un attribut type pour chacun des noeuds de l'expression (en rouge sur l'exemple de la figure 59) en fonction des attributs des fils du noeud.
Pour calculer le type de la variable e, l'algorithme calcule d'abord le type de ses opérandes. Le premier opérande est de type entier (2), l'autre est le résultat de l'accès au tableau n, si le type du tableau n est connu alors le système peut décider si l'expression à un type valide (tableau d'entier ou de réels) et affecter un type à la variable e.
Dans le cas où le type de n n'est pas connu, alors une nouvelle variable de type n est crée dans l'environnement, et le type tableau de n est affecté à la variable n. Le type de la variable e pourra être effectivement déterminé si l'opérateur + peut être appliqué à un entier et à n.
|
[Here is a Drawing] |
|
Figure 59 - Inférence du type d'une expression
Le problème de l'inférence se généralise à la reconstruction de type en calculant un type pour chacune des variables d'un programme. Pour cela toutes les variables de types non libres (ne pouvant être renommées) introduites lors de l'inférence doivent être valuées par des expressions de type. Il est montré dans [Cardelli 85] que ce problème est décidable pour les systèmes de types n'incluant pas de quantificateurs.
Lors de la reconstruction de types d'un programme il est fréquent de tester l'équivalence de deux expressions de types. Par exemple lorsqu'une variable à laquelle est associé une expression de type est modifiée, il faut comparer le type de la valeur affectée avec l'expression de type. Comme pour l'abstraction de types de données et pour la surcharge des opérateurs, un système de types permettant le typage implicite s'appuie sur l'équivalence des expressions de types.
Les systèmes de types des langages calculant la validité des types lors de l'abstraction de types de données, du nommage des expressions de type ou de la surcharge des opérateurs utilisent la notion d'équivalence de types de données. L'équivalence peut exister à plusieurs niveaux :
Cette notion d'équivalence est très restrictive car elle implique que les types des variables comparées soient nommés. L'équivalence de deux types « égaux », mais de noms différents ne sera pas relevée.
Cette définition permet de mettre en équivalence des types portant des noms différents en se basant sur la correspondance des constructeurs et l'équivalence des composantes du type :
Soient deux types a et b de constructions respectives C(a1,¼,an) et C'(b1,¼,bm), où C et C' sont des constructeurs et ai, bj les types composants respectivement les types a et b. a et b sont structuralement équivalents si et seulement si :
L'équivalence structurale peut être implémentée par un algorithme de parcours de graphes dirigés sans cycles, mais cette implémentation ne permet pas de déterminer l'équivalence de types contenant des variables de types ou des définitions récursives.
L'algorithme d'unification permet de calculer l'équivalence structurale d'expressions contenant des variables de types. En conséquence, la récursion dans la définition des types est prise en compte.
Nous détaillons dans la suite un algorithme d'unification utilisant des classes d'équivalence de types pour prendre en compte la circularité du graphe de type.
L'algorithme d'unification permet de comparer deux types pour trouver une relation d'équivalence. Cet algorithme est une généralisation de l'algorithme d'unification donné dans [Aho 91] aux graphes de types n-aires.
Les types sont définis par des graphes orientés dont les noeuds représentent soit des types soit des variables de types. Le noeuds représentant des types sont étiquetés par le constructeur du type représenté. Les arcs représentent la relation « entre dans le définition de ».
Le principe de l'algorithme repose sur la construction de classes d'équivalence regroupant des noeuds en cours d'unification. Le rôle de ces classes d'équivalence est de ne pas répéter l'unification sur des noeuds participant aux cycles des graphes de types. Chaque classe est représentée de façon unique par un de ses noeuds.
La fonction Fusionner_Classes (n1, n2) permet de créer une nouvelle classe d'équivalence en fusionnant les classes auxquelles appartiennent les noeuds n1 et n2. Si une seule des deux classes est représentée par un noeud qui n'est pas une variable, Fusionner_Classes choisit ce noeud comme représentant de la nouvelle classe. Ainsi, un noeud correspondant à une variable ne peut être représentant d'une classe comprenant des noeuds correspondant à un type construit ou un type de base, ce qui mènerait à unifier à travers cette variable des noeuds non équivalents.
La fonction Trouver_Classe (n) retourne le représentant de la classe d'équivalence à laquelle appartient le noeud n.
Au début de l'unification chaque noeud représente une classe dont il est l'unique élément. Les conditions d'unifications des deux noeuds sont :
Algorithme :
Unifier (m, n : noeud) : booléen;
début
s := Trouver_Classe (m);
t := Trouver_Classe (n);
si s = t alors retourner vrai;
sinon si s et t sont des noeuds représentant le même type de
base
alors retourner vrai;
sinon si
s est un noeud de constructeur a et de fils s1...sp et
t est un noeud de constructeur a et de fils t1...tp
alors
Fusionner_Classes (s, t);
retourner (Unifier (s1, t1) et ... et Unifier (sp, tp));
sinon si s ou t représente une variable alors
Fusionner_Classes (s, t);
retourner vrai;
sinon retourner faux;
finsi
fin
Avec cet algorithme, on détermine si deux types sont équivalents. Si c'est le cas, toute variable d'un des deux types est utilisable à la place d'une variable de l'autre type tout en assurant la conformité de sa valeur, ce qui préserve la propriété de sécurité lors des surcharges d'opérateurs. Les variables relevant d'un type unifié avec un type cible peuvent également être converties dans ce type cible pour permettre une coercition sûre.
L'équivalence de type déterminée par l'algorithme d'unification est également utilisée pour l'inférence de type dans les langages implicitement typés (ML, Lisp).