Annexes

A Systèmes de types des langages de programmation

A.1 Langages de programmation et systèmes de types

A.1.1 Langages typés et non typés

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 :

une économie de temps d'exécution
une économie de temps de développement
une économie de compilation
une simplicité d'expression des langages

A.1.2 Systèmes de types

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.

Définitions

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 :

Définition explicite des types de données : une expression de type décrit un type construit, ses opérandes sont des types de base ou d'autres types construits et ses opérateurs sont appelés constructeurs de type.
Définition implicite des types de données : le type d'une expression est calculé lors de son évaluation. Le type des variables utilisées dans un programme est déduit lors de leur utilisation.

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).

A.1.3 Contrôle de type et sécurité à l'exécution

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.

A.2 Un contrôleur de types simple

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 types de base du langage L sont les types entier et chaîne.
Les types construits sont les entités composites décrites par une expression de type. Les constructeurs du langage L sont : tableau, pointeur, structure et fonction.

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.

Vérification du type d'une expression

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.




A.3 Limites et extensions du contrôle de
types simple

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 :


Utilisation de variables de types : les critères
d'égalité entre types ne se fondent que sur
l'égalité des constructeurs. L'algorithme ne permet pas de
déterminer si une variable du programme est compatible avec une
variable de type. Le contrôle de type doit pouvoir déterminer si
une expression du langage appartient à un type contenant des variables
de types dans sa définition.
Types récursifs : l'utilisation des variables de types
permet la définition de types intervenant dans leur propre
définition. Cette propriété introduit des cycles dans le
graphe de représentation des types de données, l'algorithme de
contrôle de types doit prendre en compte la gestion des cycles.
Surcharge des opérateurs : dans le langage L chaque
opérateur agit sur des opérandes dont le type est bien
défini. Dans certains langages, le même opérateur peut
représenter des opérations différentes quand il est
appliqué à des types des données différentes. Un
exemple simple est l'opérateur + qui peut être
indifféremment appliqué à des opérandes entiers ou
réels. La comparaison de types de données ne doit pas simplement
se faire sur l'identification des types, mais sur des critères plus
généraux.
Types implicites : le langage ML [Milner 90] admet l'utilisation d'identificateurs
dont le type n'est pas déclaré. Lors de l'interprétation
de programmes écrits dans ce langage, le système de types doit
calculer le type de ces identificateurs lors de leur utilisation.
Abstraction des types de données : l'implémentation
de fonctions indépendantes du type des objets qu'elles manipulent
permet leur réutilisation  dans des environnement différents.


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
:


une méthode d'inférence de type pour calculer le
type des variables implicitement typées du programme, permettant ainsi
la manipulation de variables implicitement typées ;
une méthode de calcul d'équivalence de types ne se
basant pas seulement sur l'identification des types, mais sur leur
construction structurelle (notion d'équivalence structurelle) et
permettant de prendre en compte les types récursifs ;
une méthode de conversion de données entre types
ayant des structures équivalentes.




A.4 Inférence de 
type

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]






e = 2 + n[3];

  





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.



A.5 Équivalence 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 :


équivalence de noms : deux types sont équivalents si et
seulement si ils portent le même nom. Les compilateurs des langages de
programmation interdisant généralement les définitions
multiples, deux variables appartenant à des types ayant le même
identificateur appartiennent au même type.
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.

équivalence structurale : deux types sont équivalents s'ils
ont le même constructeur et les types qui les définissent sont
équivalents deux à deux.
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 :


C est le même constructeur que C'.
n = m et "i Î [1,n], ai est structuralement équivalent à bi.




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.


A.5.1 Algorithme d'unification

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 :


l'appartenance à la même classe,
la représentation d'un même type de base,
la représentation de deux types de même constructeur,
à la condition de pouvoir unifier les types participant à leur
construction (noeuds fils), 
la représentation par l'un des noeuds d'une variable de type.


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).

Annexes

A Systèmes de types des langages de programmation

A.1 Langages de programmation et systèmes de types

A.1.1 Langages typés et non typés

A.1.2 Systèmes de types

Définitions

A.1.3 Contrôle de type et sécurité à l'exécution

A.2 Un contrôleur de types simple

Vérification du type d'une expression

A.3 Limites et extensions du contrôle de types simple

A.4 Inférence de type

A.5 Équivalence de types

A.5.1 Algorithme d'unification

References

Footnotes