Type statique

Typage statique

Définition

Le typage statique est une technique utilisée dans certains langages de programmation impératifs (C++, Java, Pascal, par exemple) pour associer à un symbole dénotant une variable le type de la valeur dénotée par la variable ; et dans certains langages de programmation fonctionnels (ML, Objective Caml, Haskell, etc.) pour associer à une fonction (un calcul) le type de son paramètre et le type de la valeur calculée.

Une telle association présente les bénéfices potentiels suivants :

• un compilateur de langage à typage statique détecte les erreurs de types avant que le programme ne soit exécuté (on obtient ainsi la sûreté du typage),
• le même compilateur peut tirer parti de l'information sur les types pour réaliser certaines optimisations du code objet,
• enfin, puisque les types des objets manipulés sont connus, le compilateur peut éliminer cette information du code objet produit, avec pour principal avantage un gain de mémoire par rapport aux systèmes à typage dynamique.

Langages à objets et typage statique

(déplacer vers nouvel article : le problème de la covariance/contravariance)

Les langages à objets en particulier peuvent tirer parti du typage statique, afin de détecter avant l'exécution des erreurs de types (comme par exemple la tentative d'additionner un entier avec une chaîne de caractères). Toutefois, la sûreté du typage et la programmation orientée objet sont parfois en contradiction, parce que le typage sûr va à l'encontre de la modélisation « naturelle » du problème à résoudre avec l'approche objet (redéfinition contravariante du type des paramètres des méthodes pour la sûreté du typage vs. redéfinition covariante dans l'approche objet).

Pour éclaircir la dernière phrase, nous travaillons sur un exemple. Considérons en Java l'extrait de code suivant :

  Graphe mon_graphe = new Graphe ();
 
  Nœud n1, n2;
  n1 = new Nœud ();
  n2 = new Nœud ();
 
  Arête a = new Arête (n1, n2);
 
  mon_graphe.ajout_nœud (n1);
  mon_graphe.ajout_nœud (n2);
  mon_graphe.ajout_arête (a);

Quatre objets sont déclarés et instanciés, précédés de leur type (respectivement Graphe, Nœud, Arête). Si le programmeur essaye d'instancier mon_graphe avec le type Nœud, le compilateur le lui interdit car mon_graphe a été déclaré comme étant de type Graphe (contrôle sur le type de retour).

De même, si la méthode ajout_nœud () de la classe Graphe a été définie comme ceci :

 boolean ajout_nœud (Nœud n) { ... }

c'est-à-dire en spécifiant le type du paramètre reçu, le compilateur saura détecter une erreur d'appel (par exemple 'mon_graphe.ajout_nœud (a)') - (contrôle sur le type des paramètres).

Problèmes

C'est ce dernier point qui est le plus délicat. Supposons une dérivation de Graphe : la classe Réseau spécialise Graphe, Routeur spécialise Nœud et Lien spécialise Arête.

En particulier, la méthode ajout_nœud est redéfinie dans Réseau :

 boolean ajout_nœud (Routeur r) { ... } //modélisation covariante conforme à l'intuition

Considérons alors le code suivant :

 Réseau res = new Réseau;
 Nœud n = new Nœud;
 res.ajout_nœud (n); //Boum ! Le compilateur refuse ceci.

En fait, pour garantir la sûreté du typage, il faut que le type des paramètres de la méthode ajout_nœud de Réseau soit un super-type du paramètre de la méthode ajout_nœud de Graphe.

De façon schématique :

Soient des classes A et B telles que B < A (« B spécialise A ») et B <: A (« B est un sous-type de A »); une méthode m(A) de type fonctionnel u→t définie sur A. Si B redéfinit m, alors le type de m(B) est u'→t' tels que u' <: u et t <: t', ce qui implique que u' < u et t < t'.

En d'autres termes, la redéfinition de méthode a pour corollaire la *covariance* du type de retour (ce type varie dans le même sens que B < A) et la *contravariance* du type des paramètres.

Résolution, autres difficultés

Des langages comme Java et C++ ont tranché en faveur de l'invariance des types de retour et des paramètres de méthodes bien que dans ces deux langages, les types de retour puissent être covariants.

Les besoins de la modélisation (covariance du type des paramètres) entraînent des astuces plus ou moins contestables pour la simuler dans ces langages : il faut combiner des opérateurs de *coercition descendante* (downcast) et la *surcharge statique* de méthodes pour y arriver.

Le langage de programmation Eiffel est le seul à admettre la redéfinition covariante du type des paramètres.

Dans *tous* les cas, le programmeur doit anticiper des erreurs de type à l'exécution, comme dans les langages à typage dynamique. En résumé, il faut admettre que « les erreurs de type sont dans la nature ». Par exemple, considérons :

• classe Animal, méthode Mange (nourriture)
• classe Vache, méthode Mange (de l'herbe)

Ce typage est (a priori) incorrect, et le compilateur refusera le programme car manifestement herbe <: nourriture (<: « est un sous-type de »). En pratique rien n'empêche qu'une instance de « Pâté d'alouettes » ne soit donné en paramètre à une instance de Vache. Corrigeons :

• classe Vache, méthode Mange (de tout)

Le typage est donc « sûr », car nourriture <: tout. Donc à l'exécution, la vache peut recevoir des farines animales. La maladie de la vache folle est une erreur de type, garantie par la sûreté du typage...

Inférence des types

Des langages à typage statique comme ML évitent en partie ces chausse-trappes en proposant un puissant mécanisme d'inférence de type : le compilateur devine le type des variables d'après les opérateurs utilisés par le programmeur.

Par exemple, si l'opérateur '+' est utilisé pour l'addition entière, le compilateur en déduira le type de ses arguments. Plus généralement, le moteur d'inférence de type essaie de déduire le type le plus général qui est un type valide pour le programme. Par exemple, le programme suivant ne fait aucune hypothèse sur le type de son argument :

 let identity x = x

ML lui affectera le type : 'a -> 'a qui signifie qu'on peut utiliser la fonction identity avec un argument d'un type quelconque. Ainsi, les expressions "identity 0" et "identity 'a'" sont donc valides. On nomme polymorphisme ce typage général des programmes.

Il existe de nombreuses variantes du polymorphisme. Concilier inférence de types et polymorphisme avancé est une tâche complexe dans laquelle les langages Ocaml et Haskell brillent particulièrement. En Ocaml ou Haskell, l'inférence de type est capable d'inférer que le programme suivant :

 let double x = x + x

ne peut être appliqué qu'à des arguments dont les valeurs sont compatibles avec l'opérateur +. Le type de double est alors en Ocaml int -> int et respectivement en Haskell Num a => a => a.

Si les contraintes de typage ne sont pas satisfiables alors le programmeur a fait une erreur de type.

Ce document provient de « Typage statique ».